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
fDate :
6/27/1905 12:00:00 AM
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"
Conference_Titel :
Temporal Representation and Reasoning, 2005. TIME 2005. 12th International Symposium on
Print_ISBN :
0-7695-2370-6
DOI :
10.1109/TIME.2005.28