On the freeze quantifier in Constraint LTL: Decidability and complexity. (English) Zbl 1116.03014
Summary: 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 \(\langle\mathbb{N},= \rangle\) 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).
MSC:
| 03B44 | Temporal logic |
| 03B25 | Decidability of theories and sets of sentences |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
| 68Q25 | Analysis of algorithms and problem complexity |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Keywords:
linear-time temporal logic; constraints; freeze quantifier; decidability; computational complexityReferences:
| [1] | S. Demri, R. Lazić, D. Nowak, On the freeze quantifier in constraint LTL: decidability and complexity, in: 12th Int. Symp. Temporal Representation and Reasoning (TIME), IEEE, 2005, pp. 113-121.; S. Demri, R. Lazić, D. Nowak, On the freeze quantifier in constraint LTL: decidability and complexity, in: 12th Int. Symp. Temporal Representation and Reasoning (TIME), IEEE, 2005, pp. 113-121. |
| [2] | P. Schnoebelen, The complexity of temporal logic model checking, in: AiML’02, vol. 4 of Advances in Modal Logic, King’s College, 2003, pp. 393-436.; P. Schnoebelen, The complexity of temporal logic model checking, in: AiML’02, vol. 4 of Advances in Modal Logic, King’s College, 2003, pp. 393-436. · Zbl 1084.03013 |
| [3] | Revesz, P., Introduction to Constraint Databases (2002), Springer: Springer Berlin · Zbl 0995.68035 |
| [4] | Alur, R.; Dill, D., A theory of timed automata, Theoretical Comput. Sci., 126, 183-235 (1994) · Zbl 0803.68071 |
| [5] | Ibarra, O., Reversal-bounded multicounter machines and their decision problems, J. ACM, 25, 1, 116-133 (1978) · Zbl 0365.68059 |
| [6] | B. Boigelot, Symbolic methods for exploring infinite state spaces, Ph.D. thesis, Université de Liège, (1998).; B. Boigelot, Symbolic methods for exploring infinite state spaces, Ph.D. thesis, Université de Liège, (1998). |
| [7] | B. Boigelot, P. Wolper, Representing arithmetic constraints with finite automata: an overview, in: 18th Int. Conf. Logic Prog. (ICLP), vol. 2401 of Lecture Notes in Computer Science, Springer, Berlin, 2002, pp. 1-19.; B. Boigelot, P. Wolper, Representing arithmetic constraints with finite automata: an overview, in: 18th Int. Conf. Logic Prog. (ICLP), vol. 2401 of Lecture Notes in Computer Science, Springer, Berlin, 2002, pp. 1-19. · Zbl 1045.03038 |
| [8] | A. Finkel, J. Leroux, How to compose Presburger accelerations: Applications to broadcast protocols, in: 22nd Conf. Foundations of Software Tech. and Theoretical Comput. Sci. (FSTTCS), vol. 2256 of Lecture Notes in Computer Science, Springer, Berlin, 2002, pp. 145-156.; A. Finkel, J. Leroux, How to compose Presburger accelerations: Applications to broadcast protocols, in: 22nd Conf. Foundations of Software Tech. and Theoretical Comput. Sci. (FSTTCS), vol. 2256 of Lecture Notes in Computer Science, Springer, Berlin, 2002, pp. 145-156. · Zbl 1027.68616 |
| [9] | J. Leroux, G. Sutre, Flat counter systems are everywhere!, in: 3rd Int. Symp. Automated Tech. for Verification and Analysis (ATVA), vol. 3707 of Lecture Notes in Computer Science, Springer, Berlin, 2005, pp. 489-503.; J. Leroux, G. Sutre, Flat counter systems are everywhere!, in: 3rd Int. Symp. Automated Tech. for Verification and Analysis (ATVA), vol. 3707 of Lecture Notes in Computer Science, Springer, Berlin, 2005, pp. 489-503. · Zbl 1170.68519 |
| [10] | H. Comon, V. Cortier, Flatness is not a weakness, in: 14th Int. Works. Comput. Sci. Logic (CSL), vol. 1862 of Lecture Notes in Computer Science, Springer, Berlin, 2000, pp. 262-276.; H. Comon, V. Cortier, Flatness is not a weakness, in: 14th Int. Works. Comput. Sci. Logic (CSL), vol. 1862 of Lecture Notes in Computer Science, Springer, Berlin, 2000, pp. 262-276. · Zbl 0973.68142 |
| [11] | S. Demri, D. D’Souza, An automata-theoretic approach to constraint LTL, Tech. Rep. 03-11, LSV, an extended abstract appeared in FSTTCS’02 (2003).; S. Demri, D. D’Souza, An automata-theoretic approach to constraint LTL, Tech. Rep. 03-11, LSV, an extended abstract appeared in FSTTCS’02 (2003). |
| [12] | Alur, R.; Henzinger, T., A really temporal logic, J. ACM, 41, 1, 181-204 (1994) · Zbl 0807.68065 |
| [13] | E. Harel, O. Lichtenstein, A. Pnueli, Explicit clock temporal logic, in: 5th Symp. Logic in Comput. Sci. (LICS), IEEE, 1990, pp. 400-413.; E. Harel, O. Lichtenstein, A. Pnueli, Explicit clock temporal logic, in: 5th Symp. Logic in Comput. Sci. (LICS), IEEE, 1990, pp. 400-413. |
| [14] | S. Demri, LTL over Integer Periodicity Constraints, Tech. Rep. 04-6, LSV, an extended abstract appeared in FOSSACS’04 (2004).; S. Demri, LTL over Integer Periodicity Constraints, Tech. Rep. 04-6, LSV, an extended abstract appeared in FOSSACS’04 (2004). |
| [15] | A. Lisitsa, I. Potapov, Temporal logic with predicate λ-abstraction, in: 12th Int. Symp. Temporal Representation and Reasoning (TIME), IEEE, 2005, pp. 147-155.; A. Lisitsa, I. Potapov, Temporal logic with predicate λ-abstraction, in: 12th Int. Symp. Temporal Representation and Reasoning (TIME), IEEE, 2005, pp. 147-155. |
| [16] | F. Wolter, M. Zakharyaschev, Spatio-temporal representation and reasoning based on RCC-8, in: 7th Int. Conf. Principles of Knowledge Representation and Reasoning (KR), Morgan Kaufmann, Los Altos, CA, 2000, pp. 3-14.; F. Wolter, M. Zakharyaschev, Spatio-temporal representation and reasoning based on RCC-8, in: 7th Int. Conf. Principles of Knowledge Representation and Reasoning (KR), Morgan Kaufmann, Los Altos, CA, 2000, pp. 3-14. |
| [17] | P. Balbiani, J. Condotta, Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning, in: 4th Int. Works. Frontiers of Combining Systems (FroCoS), vol. 2309 of Lecture Notes in Artificial Intelligence, Springer, Berlin, 2002, pp. 162-173.; P. Balbiani, J. Condotta, Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning, in: 4th Int. Works. Frontiers of Combining Systems (FroCoS), vol. 2309 of Lecture Notes in Artificial Intelligence, Springer, Berlin, 2002, pp. 162-173. · Zbl 1057.68116 |
| [18] | D. Gabelaia, R. Kontchakov, A. Kurucz, F. Wolter, M. Zakharyaschev, On the computational complexity of spatio-temporal logics, in: 16th Int. Florida AI Research Soc. Conf. (FLAIRS), AAAI, 2003, pp. 460-464.; D. Gabelaia, R. Kontchakov, A. Kurucz, F. Wolter, M. Zakharyaschev, On the computational complexity of spatio-temporal logics, in: 16th Int. Florida AI Research Soc. Conf. (FLAIRS), AAAI, 2003, pp. 460-464. · Zbl 1080.68682 |
| [19] | Sistla, A.; Clarke, E., The complexity of propositional linear temporal logic, J. ACM, 32, 3, 733-749 (1985) · Zbl 0632.68034 |
| [20] | Dams, D., Flat fragments of CTL and CTL*: separating the expressive and distinguishing powers, Logic J. IGPL, 7, 1, 55-78 (1999) · Zbl 0920.03031 |
| [21] | O. Ibarra, Z. Dang, On removing the stack from reachability constructions, in: Int. Symp. Algorithms and Computation (ISAAC), vol. 2223 of Lecture Notes in Computer Science, Springer, Berlin, 2001, pp. 244-256.; O. Ibarra, Z. Dang, On removing the stack from reachability constructions, in: Int. Symp. Algorithms and Computation (ISAAC), vol. 2223 of Lecture Notes in Computer Science, Springer, Berlin, 2001, pp. 244-256. · Zbl 1077.68668 |
| [22] | A. Bouajjani, P. Habermehl, Constrained properties, semilinear sets, Petri nets, in: 7th Int. Conf. Concurrency Theory (CONCUR), vol. 1119 of Lecture Notes in Computer Science, Springer, Berlin, 1996, pp. 481-497.; A. Bouajjani, P. Habermehl, Constrained properties, semilinear sets, Petri nets, in: 7th Int. Conf. Concurrency Theory (CONCUR), vol. 1119 of Lecture Notes in Computer Science, Springer, Berlin, 1996, pp. 481-497. · Zbl 1514.68125 |
| [23] | B. ten Cate, M. Franceschet, On the complexity of hybrid logics with binders, in: 19th Int. Works. Comput. Sci. Logic (CSL), vol. 3634 of Lecture Notes in Computer Science, Springer, Berlin, 2005, pp. 339-354.; B. ten Cate, M. Franceschet, On the complexity of hybrid logics with binders, in: 19th Int. Works. Comput. Sci. Logic (CSL), vol. 3634 of Lecture Notes in Computer Science, Springer, Berlin, 2005, pp. 339-354. · Zbl 1136.03311 |
| [24] | Wolper, P., Temporal logic can be more expressive, Inf. Comput., 56, 72-99 (1983) · Zbl 0534.03009 |
| [25] | P. van Emde Boas, The convenience of tilings, in: Complexity, Logic, Recursion Theory, vol. 187 of Lecture Notes in Pure and Applied Logic, Marcel Dekker, New York, 1997, pp. 331-363.; P. van Emde Boas, The convenience of tilings, in: Complexity, Logic, Recursion Theory, vol. 187 of Lecture Notes in Pure and Applied Logic, Marcel Dekker, New York, 1997, pp. 331-363. · Zbl 0874.03050 |
| [26] | F. Laroussinie, N. Markey, P. Schnoebelen, Temporal logic with forgettable past, in: 17th Symp. Logic in Comput. Sci. (LICS), IEEE, 2002, pp. 383-392.; F. Laroussinie, N. Markey, P. Schnoebelen, Temporal logic with forgettable past, in: 17th Symp. Logic in Comput. Sci. (LICS), IEEE, 2002, pp. 383-392. |
| [27] | E. Kieronski, EXPSPACE-complete variant of guarded fragment with transitivity, in: 19th Ann. Symp. Theoretical Aspects of Comput. Sci. (STACS), vol. 2285 of Lecture Notes in Computer Science, Springer, Berlin, 2002, pp. 608-619.; E. Kieronski, EXPSPACE-complete variant of guarded fragment with transitivity, in: 19th Ann. Symp. Theoretical Aspects of Comput. Sci. (STACS), vol. 2285 of Lecture Notes in Computer Science, Springer, Berlin, 2002, pp. 608-619. · Zbl 1054.03504 |
| [28] | Emerson, A.; Halpern, J., “Sometimes” and “Not Never” revisited: on branching versus linear time temporal logic, J. ACM, 33, 151-178 (1986) · Zbl 0629.68020 |
| [29] | S. Demri, R. Gascon. Verification of qualitative \(\mathbb{Z} \); S. Demri, R. Gascon. Verification of qualitative \(\mathbb{Z} \) · Zbl 1134.68405 |
| [30] | Rogers, H., Theory of Recursive Functions and Effective Computability (1967), McGraw-Hill: McGraw-Hill New York · Zbl 0183.01401 |
| [31] | Neven, F.; Schwentick, T.; Vianu, V., Finite state machines for strings over infinite alphabets, ACM Trans. Comput. Logic, 5, 3, 403-435 (2004) · Zbl 1367.68175 |
| [32] | C. David. Mots et données infinies, Master’s thesis, LIAFA (2004).; C. David. Mots et données infinies, Master’s thesis, LIAFA (2004). |
| [33] | Lutz, C., NEXPTIME-complete description logics with concrete domains, ACM Trans. Comput. Logic, 5, 4, 669-705 (2004) · Zbl 1367.68288 |
| [34] | A. Bouajjani, R. Echahed, and P. Habermehl, On the verification problem of nonregular properties for nonregular processes, in: 10th Symp. Logic in Comput. Sci. (LICS), IEEE, 1995, pp. 123-133.; A. Bouajjani, R. Echahed, and P. Habermehl, On the verification problem of nonregular properties for nonregular processes, in: 10th Symp. Logic in Comput. Sci. (LICS), IEEE, 1995, pp. 123-133. |
| [35] | T. Henzinger. Half-order modal logic: how to prove real-time properties, in: 9th Ann. Symp. Principles of Distr. Comput. (PODC), ACM, 1990, pp. 281-296.; T. Henzinger. Half-order modal logic: how to prove real-time properties, in: 9th Ann. Symp. Principles of Distr. Comput. (PODC), ACM, 1990, pp. 281-296. |
| [36] | T. Brihaye, V. Bruyère, J. Raskin, Model-checking for weighted timed automata, in: 2nd Int. Conf. Formal Modelling and Analysis of Timed Systems (FORMATS), vol. 3253 of Lecture Notes in Computer Science, Springer, Berlin, 2004, pp. 277-292.; T. Brihaye, V. Bruyère, J. Raskin, Model-checking for weighted timed automata, in: 2nd Int. Conf. Formal Modelling and Analysis of Timed Systems (FORMATS), vol. 3253 of Lecture Notes in Computer Science, Springer, Berlin, 2004, pp. 277-292. · Zbl 1109.68512 |
| [37] | R. Alur, T. Henzinger, A really temporal logic, in: 30th Ann. Symp. Foundations Comput. Sci. (FOCS), IEEE, 1989, pp. 164-169.; R. Alur, T. Henzinger, A really temporal logic, in: 30th Ann. Symp. Foundations Comput. Sci. (FOCS), IEEE, 1989, pp. 164-169. · Zbl 0807.68065 |
| [38] | Alur, R.; Feder, T.; Henzinger, T., The benefits of relaxing punctuality, J. ACM, 43, 116-146 (1996) · Zbl 0882.68021 |
| [39] | Goranko, V., Hierarchies of modal and temporal logics with references pointers, J. Logic, Lang. Inf., 5, 1-24 (1996) · Zbl 0851.03003 |
| [40] | C. Areces, P. Blackburn, M. Marx, A road-map on complexity for hybrid logics, in: 13th Int. Works. Comput. Sci. Logic (CSL), vol. 1683 of Lecture Notes in Computer Science, Springer, Berlin, 1999, pp. 307-321.; C. Areces, P. Blackburn, M. Marx, A road-map on complexity for hybrid logics, in: 13th Int. Works. Comput. Sci. Logic (CSL), vol. 1683 of Lecture Notes in Computer Science, Springer, Berlin, 1999, pp. 307-321. · Zbl 0942.03048 |
| [41] | M. Franceschet, M. de Rijke, B.-H Schlingloff, Hybrid logics on linear structures: Expressivity and complexity, in: 10th Int. Symp. Temporal Representation and Reasoning and 4th Int. Conf. Temporal Logic (TIME-ICTL), IEEE, 2003, pp. 164-171.; M. Franceschet, M. de Rijke, B.-H Schlingloff, Hybrid logics on linear structures: Expressivity and complexity, in: 10th Int. Symp. Temporal Representation and Reasoning and 4th Int. Conf. Temporal Logic (TIME-ICTL), IEEE, 2003, pp. 164-171. |
| [42] | F. de Boer, R. van Eijk, Decidable navigation logics for object structures, in: 15th Int. Works. Comput. Sci. Logic (CSL), vol. 2142 of Lecture Notes in Computer Science, Springer, Berlin, 2001, pp. 324-338.; F. de Boer, R. van Eijk, Decidable navigation logics for object structures, in: 15th Int. Works. Comput. Sci. Logic (CSL), vol. 2142 of Lecture Notes in Computer Science, Springer, Berlin, 2001, pp. 324-338. · Zbl 0999.03018 |
| [43] | Cho, S. M.; Kim, H. H.; Cha, S. D.; Bae, D. H., A semantics of sequence diagrams, Inf. Process. Lett., 84, 125-130 (2002) · Zbl 1042.68072 |
| [44] | T. French, Quantified propositional temporal logic with repeating states, in: 10th Int. Symp. Temporal Representation and Reasoning and 4th Int. Conf. Temporal Logic (TIME-ICTL), IEEE, 2003, pp. 155-165.; T. French, Quantified propositional temporal logic with repeating states, in: 10th Int. Symp. Temporal Representation and Reasoning and 4th Int. Conf. Temporal Logic (TIME-ICTL), IEEE, 2003, pp. 155-165. |
| [45] | Fitting, M., Modal logic between propositional and first-order, J. Logic and Comput., 12, 6, 1017-1026 (2002) · Zbl 1017.03008 |
| [46] | Degtyarev, A.; Fisher, M.; Lisitsa, A., Equality and monodic first-order temporal logic, Studia Logica, 72, 147-156 (2002) · Zbl 1011.03007 |
| [47] | Wolter, F.; Zakharyaschev, M., Axiomatizing the monodic fragment of first-order temporal logic, Ann. Pure Appl. Logic, 118, 133-145 (2002) · Zbl 1031.03023 |
| [48] | I. Hodkinson, R. Kontchakov, A. Kurucz, F. Wolter, M. Zakharyaschev, On the computational complexity of decidable fragments of first-order linear temporal logics, in: 10th Int. Symp. Temporal Representation and Reasoning and 4th Int. Conf. Temporal Logic (TIME-ICTL), IEEE, 2003, pp. 91-98.; I. Hodkinson, R. Kontchakov, A. Kurucz, F. Wolter, M. Zakharyaschev, On the computational complexity of decidable fragments of first-order linear temporal logics, in: 10th Int. Symp. Temporal Representation and Reasoning and 4th Int. Conf. Temporal Logic (TIME-ICTL), IEEE, 2003, pp. 91-98. |
| [49] | Gabbay, D.; Kurucz, A.; Wolter, F.; Zakharyaschev, M., Many-dimensional modal logics: theory and practice (2003), Cambridge University Press: Cambridge University Press Cambridge · Zbl 1051.03001 |
| [50] | Hodkinson, I.; Wolter, F.; Zakharyaschev, M., Decidable fragments of first-order temporal logics, Ann. Pure and Applied Logic, 106, 85-134 (2000) · Zbl 0999.03015 |
| [51] | Bouyer, P.; Petit, A.; Thérien, D., An algebraic approach to data languages and timed languages, Inf. Comput., 182, 2, 137-162 (2003) · Zbl 1028.68080 |
| [52] | Bouyer, P., A logical characterization of data languages, Inf. Process. Lett., 84, 2, 75-85 (2002) · Zbl 1042.68544 |
| [53] | M. Bojańczyk, C. David, A. Muscholl, T. Schwentick, L. Segoufin, Two-variable logic on words with data, Tech. Rep. 2005-004, LIAFA (2005).; M. Bojańczyk, C. David, A. Muscholl, T. Schwentick, L. Segoufin, Two-variable logic on words with data, Tech. Rep. 2005-004, LIAFA (2005). |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
