Paper Info
Title
Branching-time temporal logic extended with qualitative presburger constraints
Abstract
Recently, LTL extended with atomic formulas built over a constraint language interpreting variables in ℤ has been shown to have a decidable satisfiability and model-checking problem. This language allows to compare the variables at different states of the model and include periodicity constraints, comparison constraints, and a restricted form of quantification. On the other hand, the CTL counterpart of this logic (and hence also its CTL* counterpart which subsumes both LTL and CTL) has an undecidable model-checking problem. In this paper, we substantially extend the decidability border, by considering a meaningful fragment of CTL* extended with such constraints (which subsumes both the universal and existential fragments, as well as the EF-like fragment) and show that satisfiability and model-checking over relational automata that are abstraction of counter machines are decidable. The correctness and the termination of our algorithm rely on a suitable well quasi-ordering defined over the set of variable valuations.
Year
DOI
Venue
2006
10.1007/11916277_14
LPAR
Keywords
Field
DocType
qualitative presburger constraint,constraint language,ef-like fragment,ctl counterpart,decidable satisfiability,atomic formula,existential fragment,meaningful fragment,model-checking problem,comparison constraint,branching-time temporal logic,undecidable model-checking problem,satisfiability,temporal logic,model checking
Computation tree logic,Computer science,Satisfiability,Algorithm,Decidability,Presburger arithmetic,Theoretical computer science,Linear temporal logic,Temporal logic,Linear logic,Undecidable problem
Conference
Volume
ISSN
ISBN
4246
0302-9743
3-540-48281-4
Citations 
PageRank 
References 
8
0.60
20
Authors
2
Name
Order
Citations
PageRank
Laura Bozzelli118326.47
Régis Gascon2765.23