DocumentCode :
3618890
Title :
On the freeze quantifier in constraint LTL: decidability and complexity
Author :
S. Demri;R. Lazic;D. Nowak
Author_Institution :
LSV/CNRS UMR 8643 & INRIA Futurs projet SECSI & ENS Cachan, France
fYear :
2005
fDate :
6/27/1905 12:00:00 AM
Firstpage :
113
Lastpage :
121
Abstract :
Constraint LTL, a generalization of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze quantifier can be part of the language, as in some real-time logics, but this variable-binding mechanism is quite general and ubiquitous in many logical languages (first-order temporal logics, hybrid logics, logics for sequence diagrams, navigation logics, etc.). We show that Constraint LTL over the simple domain augmented with the freeze operator is undecidable which is a surprising result regarding the poor language for constraints (only equality tests). Many versions of freeze-free constraint LTL are decidable over domains with qualitative predicates and our undecidability result actually establishes /spl Sigma//sub 1//sup 1/ -completeness. On the positive side, we provide complexity results when the domain is finite (EXPSPACE-completeness) or when the formulae are flat in a sense introduced in the paper.
Keywords :
"Logic","Automata","Counting circuits","Computational complexity","Clocks","Computer science","Formal languages","Navigation","Testing","Protocols"
Publisher :
ieee
Conference_Titel :
Temporal Representation and Reasoning, 2005. TIME 2005. 12th International Symposium on
ISSN :
1530-1311
Print_ISBN :
0-7695-2370-6
Type :
conf
DOI :
10.1109/TIME.2005.28
Filename :
1443358
Link To Document :
بازگشت