An Expressive Coalgebraic Modal Logic for Cellular Automata

TL;DR

The paper develops a coalgebraic framework for cellular automata that permits non-uniform neighbourhoods and update rules. It models cells as carriers in EM coalgebras for the cowriter comonad $M_{*}$, enabling a robust notion of cellular morphisms and bisimulations that preserve global behaviour. A two-tier modal logic is introduced with spatial modalities indexed by the monoid $M$ and an update modality to reason about configurations after applying the global rule, culminating in a Hennessy–Milner style theorem linking logical equivalence to cellular behavioural equivalence. The work lays a foundation for analyzing and comparing non-uniform CA via modal reasoning, with future directions toward quantitative extensions and fixed-point logics. This approach offers a uniform, expressive means to capture and verify complex CA dynamics like periodicity and nilpotency across diverse CA architectures.

Abstract

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.

Figures (1)

• Figure 1: Cellular automaton, where the spatial connectivity is given by the natural action $\gamma_{1}$ of $\mathbb{Z}$ on $\mathbb{Z}_{6}$ and local rules $\gamma_{2}$ for cells $k \in \mathbb{Z}_{6}$ by modular arithmetic.

Theorems & Definitions (1)

• definition thmcounterdefinition