The Community for Technology Leaders
Temporal Representation and Reasoning, International Syposium on (2005)
Burlington, Vermont
June 23, 2005 to June 25, 2005
ISSN: 1530-1311
ISBN: 0-7695-2370-6
pp: 113-121
Stéphane Demri , LSV/CNRS UMR 8643 & INRIA Futurs projet SECSI & ENS Cachan
David Nowak , LSV/CNRS UMR 8643 & INRIA Futurs projet SECSI & ENS Cachan
Ranko Lazić , University of Warwick
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 (N,=) 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 \sum _1^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.
INDEX TERMS
null
CITATION
Stéphane Demri, David Nowak, Ranko Lazić, "On the Freeze Quantifier in Constraint LTL: Decidability and Complexity", Temporal Representation and Reasoning, International Syposium on, vol. 00, no. , pp. 113-121, 2005, doi:10.1109/TIME.2005.28
80 ms
(Ver 3.3 (11022016))