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. © Springer-Verlag 2004.
CITATION STYLE
Hagiya, M., Takahashi, K., Yamamoto, M., & Sato, T. (2004). Analysis of synchronous and asynchronous cellular automata using abstraction by temporal logic. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2998, 7–21. https://doi.org/10.1007/978-3-540-24754-8_2
Mendeley helps you to discover research relevant for your work.