Model-checking CTL* over flat Presburger counter systems

Journal of Applied Non-Classical Logics 20 (4):313-344 (2010)
  Copy   BIBTEX


This paper concerns model-checking of fragments and extensions of CTL* on infinite-state Presburger counter systems, where the states are vectors of integers and the transitions are determined by means of relations definable within Presburger arithmetic. In general, reachability properties of counter systems are undecidable, but we have identified a natural class of admissible counter systems (ACS) for which we show that the quantification over paths in CTL* can be simulated by quantification over tuples of natural numbers, eventually allowing translation of the whole Presburger-CTL* into Presburger arithmetic, thereby enabling effective model checking. We provide evidence that our results are close to optimal with respect to the class of counter systems described above.

Similar books and articles

Linear-time temporal logics with Presburger constraints: an overview ★.Stéphane Demri - 2006 - Journal of Applied Non-Classical Logics 16 (3-4):311-347.
Presburger sets and p-minimal fields.Raf Cluckers - 2003 - Journal of Symbolic Logic 68 (1):153-162.
A framework for model checking institutions.Francesco Vigano - 2007 - In A. Lomuscio & S. Edelkamp (eds.), Model Checking and Artificial Intelligence. Springer. pp. 129--145.
Model checking for hybrid logic.Martin Lange - 2009 - Journal of Logic, Language and Information 18 (4):465-491.
Flat sets.Arthur D. Grainger - 1994 - Journal of Symbolic Logic 59 (3):1012-1021.


Added to PP

251 (#71,474)

6 months
53 (#71,065)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Valentin Goranko
Stockholm University

References found in this work

Dynamic Logic.Lenore D. Zuck & David Harel - 1989 - Journal of Symbolic Logic 54 (4):1480.
Avis.[author unknown] - 1913 - Revue Philosophique de la France Et de l'Etranger 75 (11):325-325.

Add more references