Research on Model Checking Cellular Automata
Cellular Automata (CA) is a model for describing state evolution system with local communication. It can be used to model artificial life and traffic flow, etc. The expression ability of the Cellular Automata is powerful. But the property analysis of it is in general a hard problem. In this paper, the model checker NuSMV is used to verify the reachability and safety of the Cellular Automata. The algorithm for translating the Cellular Automata into Global State Transition Diagram is provided, and the algorithm for model checking correctness of the property of the Global State Transition Diagram is also given. In the last, an example is taken to explain the method.