An Expressive Coalgebraic Modal Logic for Cellular Automata

Cellular automata provide models of parallel computation based on cells, whose connectivity is given by an action of a monoid on the cells. At each step in the computation, every cell is decorated with a state that evolves in discrete steps according to a local update rule, which determines the next state of a cell based on its neighbour's states. In this paper, we consider a coalgebraic view on cellular automata, which does not require typical restrictions, such as uniform neighbourhood connectivity and uniform local rules. Using the coalgebraic view, we devise a behavioural equivalence for cellular automata and a modal logic to reason about their behaviour. We then prove a Hennessy-Milner style theorem, which states that pairs of cells satisfy the same modal formulas exactly if they are identified under cellular behavioural equivalence.