On the Logic of Cellular Reactive Systems

In multi-agent systems where the available actions of each agent are determined by its state change history, a small change in the states of any subset of the agents, caused by an external force, may induce an infinite chain of events which force the system to undergo a complex evolvement process, even when the interconnections between the agents are partial. This scenario is common in modeling the interactions in complex systems and can be manifested vividly by the well-known ``butterfly effect". Motivated by the idea of cellular automata, cellular reactive system is defined to capture the dynamics of such multi-agent systems. Then, the logic CRL is proposed to reason about the temporal effects of external forces in a cellular reactive system. Finally, the relation between CRL and ATL* is established formally and based on which the model checking problem of CRL is discussed.