An Expressive Coalgebraic Modal Logic for Cellular Automata

Fuente: arXiv
Enregistré dans:
Détails bibliographiques
Auteurs principaux: Basold, Henning, Ford, Chase, Pirée, Lulof
Format: Preprint
Publié: 2025
Sujets:
Accès en ligne:
Tags: Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
_version_ 1866912766181244928
author Basold, Henning
Ford, Chase
Pirée, Lulof
author_facet Basold, Henning
Ford, Chase
Pirée, Lulof
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2504_16735
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle An Expressive Coalgebraic Modal Logic for Cellular Automata
Basold, Henning
Ford, Chase
Pirée, Lulof
Logic in Computer Science
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.
title An Expressive Coalgebraic Modal Logic for Cellular Automata
topic Logic in Computer Science
url https://arxiv.org/abs/2504.16735