Model-Checking CTL* over Flat Presburger Counter Systems

Publication: Research - peer-reviewJournal article – Annual report year: 2010

View graph of relations

This paper studies model-checking of fragments and extensions of CTL* on infinite- state 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.
Original languageEnglish
JournalJournal of Applied Non-Classical Logics
Publication date2010
Volume20
Journal number4
Pages313-344
ISSN1166-3081
DOIs
StatePublished
CitationsWeb of Science® Times Cited: No match on DOI

Keywords

  • model-checking, infinite-state transition systems, Presburger arithmetic, CTL* , counter systems
Download as:
Download as PDF
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
Word

ID: 5505014