Event locality is a class of theory that can clearly minimizes the memory and time required to store the state space. We present the multi-way decision diagrams to encode the next-state functions based on event locality and CSP’s stable failure. Instead of studying symbolic overall model, we apply the above thinking to the set of sub-models. Furthermore, we focus on saturation algorithms for CSP theory. And the algorithms consist of two phases, the universal process’s saturation checking and the single CSP symbol’s saturation checking. In the former case, the algorithms discuss better iteration strategy and recursive local fifix-point computations. In the latter case, the the single CSP symbol’s saturation checking calls the former algorithms, being combined preformed events and refusal events. Finally, we discuss bacterial chemotaxis modeled in CSP’s framework and saturation checking used to check the predefifined properties. The all algorithms are implemented in CSP tool FDR, the running results show that our algorithms often perform signifificantly faster than other conventional algorithms.