Model-checking CTL* over flat Presburger counter systems

Download Edit this record How to cite View on PhilPapers
Abstract
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.
ISBN(s)
PhilPapers/Archive ID
DEMMCO-2
Revision history
Archival date: 2018-04-20
View upload history
References found in this work BETA
Dynamic Logic.Harel, David; Kozen, Dexter & Tiuryn, Jerzy

Add more references

Citations of this work BETA

No citations found.

Add more citations

Added to PP index
2013-12-19

Total downloads
44 ( #29,158 of 37,180 )

Recent downloads (6 months)
13 ( #22,876 of 37,180 )

How can I increase my downloads?

Monthly downloads since first upload
This graph includes both downloads from PhilArchive and clicks to external links.