On the freeze quantifier in Constraint LTL: Decidability and complexity

被引:37
作者
Demri, Stephane
Lazic, Ranko [1 ]
Nowak, David
机构
[1] Univ Warwick, Dept Comp Sci, Coventry CV4 7AL, W Midlands, England
[2] CNRS, LSV, Cachan, France
[3] ENS, Cachan, France
[4] INRIA Futurs, Project SECSI, Futurs, France
[5] Natl Inst Adv Ind Sci & Technol, Res Ctr Informat Secur, Tsukuba, Ibaraki, Japan
基金
英国工程与自然科学研究理事会;
关键词
linear-time temporal logic; constraints; freeze quantifier; decidability; computational complexity; LOGICS; AUTOMATA;
D O I
10.1016/j.ic.2006.08.003
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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). (C) 2006 Elsevier Inc. All rights reserved.
引用
收藏
页码:2 / 24
页数:23
相关论文
共 53 条
[1]   A THEORY OF TIMED AUTOMATA [J].
ALUR, R ;
DILL, DL .
THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235
[2]   A REALLY TEMPORAL LOGIC [J].
ALUR, R ;
HENZINGER, TA .
30TH ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE, 1989, :164-169
[3]   A REALLY TEMPORAL LOGIC [J].
ALUR, R ;
HENZINGER, TA .
JOURNAL OF THE ACM, 1994, 41 (01) :181-204
[4]   The benefits of relaxing punctuality [J].
Alur, R ;
Feder, T ;
Henzinger, TA .
JOURNAL OF THE ACM, 1996, 43 (01) :116-146
[5]  
[Anonymous], 2002, Introduction to Constraint Databases
[6]  
Areces C, 1999, LECT NOTES COMPUT SC, V1683, P307
[7]  
Balbiani P, 2002, LECT NOTES ARTIF INT, V2309, P162
[8]   Representing arithmetic constraints with finite automata: An overview [J].
Boigelot, B ;
Wolper, P .
LOGICS PROGRAMMING, PROCEEDINGS, 2002, 2401 :1-19
[9]  
Boigelot B., 1998, THESIS U LIEGE
[10]  
BOJANCZYK M, 2005, 2005004 LIAFA