zbMATH — the first resource for mathematics

Analysis of synchronous and asynchronous cellular automata using abstraction by temporal logic. (English) Zbl 1122.68473
Kameyama, Yukiyoshi (ed.) et al., Functional and logic programming. 7th international symposium, FLOPS 2004, Nara, Japan, April 7–9, 2004. Proceedings. Berlin: Springer (ISBN 3-540-21402-X/pbk). Lecture Notes in Computer Science 2998, 7-21 (2004).
Summary: We have been studying abstractions of linked structures, in which cells are connected by pointers, using temporal logic. This paper presents some our results for these abstractions. The system to be verified is a transition system on a graph. The shape of the graph does not change as a result of the transition, but the label assigned to each cell (node) changes according to rewrite rules. The labels of cells are changed synchronously or asynchronously. We abstract such systems using abstract cells and abstract graphs. Abstract cells are characterized by a set of temporal formulas, and different abstractions can be tried by changing the set of formulas. Some examples of analysis are also described.
For the entire collection see [Zbl 1048.68005].
68Q80 Cellular automata (computational aspects)
03B44 Temporal logic
Full Text: DOI