An Expressive Coalgebraic Modal Logic for Cellular Automata

arXiv (Cornell University)

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.

Authors 3

1. Henning Basold Aachen

   Leiden University · University of Applied Sciences Leiden

   Affiliation as printed

   LIACS , Leiden University ,

2. Chase Ford Aachen

   Leiden University · University of Applied Sciences Leiden

   Affiliation as printed

   LIACS , Leiden University ,

3. Lulof Pirée

   Tallinn University of Technology

   Affiliation as printed

   Tallinn University of Technology ,