The Library
On the freeze quantifier in Constraint LTL : decidability and complexity
Tools
Demri, Stephane, Lazic, Ranko and Nowak, David (2005) On the freeze quantifier in Constraint LTL : decidability and complexity. In: 12th International Symposium on Temporal Representation and Reasoning, Burlington, VT, 23-25 Jun 2005. Published in: Information and Computation, Volume 205 (Number 1). pp. 2-24. doi:10.1016/j.ic.2006.08.003 ISSN 0890-5401.
Research output not available from this repository.
Request-a-Copy directly from author or use local Library Get it For Me service.
Official URL: http://dx.doi.org/10.1016/j.ic.2006.08.003
Abstract
Constraint LTL, a generalisation 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, logics with lambda-abstraction, etc.). We show that Constraint LTL over the simple domain [N, =] augmented with the freeze quantifier is undecidable which is a surprising result in view of 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 Sigma(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. Our undecidability results are sharp (i.e. with restrictions on the number of variables) and all our complexity characterisations ensure completeness with respect to some complexity class (mainly PSPACE and EXPSPACE).
Item Type: | Conference Item (Paper) | ||||
---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software Q Science > QA Mathematics |
||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||
Journal or Publication Title: | Information and Computation | ||||
Publisher: | Academic Press | ||||
ISSN: | 0890-5401 | ||||
Official Date: | 1 January 2005 | ||||
Dates: |
|
||||
Volume: | Volume 205 | ||||
Number: | Number 1 | ||||
Number of Pages: | 23 | ||||
Page Range: | pp. 2-24 | ||||
DOI: | 10.1016/j.ic.2006.08.003 | ||||
Status: | Peer Reviewed | ||||
Publication Status: | Published | ||||
Access rights to Published version: | Restricted or Subscription Access | ||||
Conference Paper Type: | Paper | ||||
Title of Event: | 12th International Symposium on Temporal Representation and Reasoning | ||||
Type of Event: | Other | ||||
Location of Event: | Burlington, VT | ||||
Date(s) of Event: | 23-25 Jun 2005 |
Data sourced from Thomson Reuters' Web of Knowledge
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |