LTL with the freeze quantifier and register automata

ABSTRACT

A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. To reason about data words, linear temporal logic is extended by the freeze quantifier, which stores the element at the current word position into a register, for equality comparisons deeper in the formula. By translations from the logic to alternating automata with registers and then to faulty counter automata whose counters may erroneously increase at any time, and from faulty and error-free counter automata to the logic, we obtain a complete complexity table for logical fragments defined by varying the set of temporal operators and the number of registers. In particular, the logic with future-time operators and 1 register is decidable but not primitive recursive over finite data words. Adding past-time operators or 1 more register, or switching to infinite data words, causes undecidability.

REFERENCES

• 1: Rajeev Alur , Thomas A. Henzinger, A really temporal logic, Journal of the ACM (JACM), v.41 n.1, p.181-203, Jan. 1994 [doi>10.1145/174644.174651]
• 2: Mikolaj Bojanczyk , Anca Muscholl , Thomas Schwentick , Luc Segoufin , Claire David, Two-Variable Logic on Words with Data, Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, p.7-16, August 12-15, 2006 [doi>10.1109/LICS.2006.51]
• 3: Ahmed Bouajjani , Peter Habermehl , Yan Jurski , Mihaela Sighireanu, Rewriting Systems with Data, Proceedings of the 16th international symposium on Fundamentals of Computation Theory, August 27-30, 2007, Budapest, Hungary [doi>10.1007/978-3-540-74240-1_1]
• 4: David, C. 2004. Mots et données infinies. M.S. thesis, Laboratoire d'Informatique Algorithmique: Fondements et Applications, Paris.
• 5: Stéphane Demri , Deepak D'Souza , Régis Gascon, A Decidable Temporal Logic of Repeating Values, Proceedings of the international symposium on Logical Foundations of Computer Science, p.180-194, June 04-07, 2007, New York, NY, USA [doi>10.1007/978-3-540-72734-7_13]
• 6: Stephane Demri , Ranko Lazic, LTL with the Freeze Quantifier and Register Automata, Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, p.17-26, August 12-15, 2006 [doi>10.1109/LICS.2006.31]
• 7: Stéphane Demri , Ranko Lazić , David Nowak, On the freeze quantifier in Constraint LTL: Decidability and complexity, Information and Computation, v.205 n.1, p.2-24, January, 2007 [doi>10.1016/j.ic.2006.08.003]
• 8: Demri, S., Lazić, R., and Sangnier, A. 2008. Model checking freeze LTL over one-counter automata. In Proceedings of the 11th International Conference on Foundations of Software Science and Computer Structurers (FoSSaCS). Lecture Notes in Computer Science, vol. 4962. Springer, 490--504.
• 9: Dickson, L. 1913. Finiteness of the odd perfect and primitive abundant numbers with distinct factors. Amer. J. Math. 35, 413--422.
• 10: Kousha Etessami , Moshe Y. Vardi , Thomas Wilke, First-order logic with two variables and unary temporal logic, Information and Computation, v.179 n.2, p.279-295, December 15, 2002 [doi>10.1006/inco.2001.2953]
• 11: Fitting, M. 2002. Modal logic between propositional and first-order. J. Logic Comput. 12, 6, 1017--1026.
• 12: French, T. 2003. Quantified propositional temporal logic with repeating states. In Proceedings of the 10th International Symposium on Temporal Representation and Reasoning/4th International Conference on Temporal Logic (TIME- ICTL). IEEE Computer Society, 155--165.
• 13: Goranko, V. 1996. Hierarchies of modal and temporal logics with references pointers. J. Logic, Lang. Inf. 5, 1--24.
• 14: Michael Kaminski , Nissim Francez, Finite-memory automata, Theoretical Computer Science, v.134 n.2, p.329-363, Nov. 21, 1994 [doi>10.1016/0304-3975(94)90242-9]
• 15: S. Rao Kosaraju, Decidability of reachability in vector addition systems (Preliminary Version), Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.267-281, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802201]
• 16: Lazić, R. 2006. Safely freezing LTL. In Proceedings of the 26th International Conference on Foundations of Software Technology and Theory in Computer Science (FSTTCS). Lecture Notes in Computer Science, vol. 4337. Springer, 381--392.
• 17: Lipton, R. J. 1976. The reachability problem requires exponential space. Tech. rep. 62, Yale University.
• 18: Alexei Lisitsa , Igor Potapov, Temporal Logic with Predicate "-Abstraction, Proceedings of the 12th International Symposium on Temporal Representation and Reasoning, p.147-155, June 23-25, 2005 [doi>10.1109/TIME.2005.34]
• 19: Richard Mayr, Undecidable problems in unreliable computations, Theoretical Computer Science, v.297 n.1-3, p.337-354, 17 March 2003 [doi>10.1016/S0304-3975(02)00646-1]
• 20: Marvin L. Minsky, Computation: finite and infinite machines, Prentice-Hall, Inc., Upper Saddle River, NJ, 1967
• 21: Miyano, S. and Hayashi, T. 1984. Alternating finite automata on ω-words. Theor. Comput. Sci. 32, 321--330.
• 22: D E Muller , A Saoudi , P E Schupp, Alternating automata, the weak monadic theory of the tree, and its complexity, International Colloquium on Automata, Languages and Programming on Automata, languages and programming, p.275-283, September 1986, Rennes, France
• 23: Frank Neven , Thomas Schwentick , Victor Vianu, Finite state machines for strings over infinite alphabets, ACM Transactions on Computational Logic (TOCL), v.5 n.3, p.403-435, July 2004 [doi>10.1145/1013560.1013562]
• 24: Ouaknine, J. and Worrell, J. 2006a. On metric temporal logic and faulty Turing machines. In Proceedings of the 9^th International Conference on Foundations of Software Science and Computer Structures (FoSSaCS). Lecture Notes in Computer Science, vol. 3921. Springer, 217--230.
• 25: Ouaknine, J. and Worrell, J. 2006b. Personal communication.
• 26: Hiroshi Sakamoto , Daisuke Ikeda, Intractability of decision problems for finite-memory automata, Theoretical Computer Science, v.231 n.2, p.297-308, Jan. 28, 2000 [doi>10.1016/S0304-3975(99)00105-X]
• 27: Ph. Schnoebelen, Verifying lossy channel systems has nonprimitive recursive complexity, Information Processing Letters, v.83 n.5, p.251-261, 15 September 2002 [doi>10.1016/S0020-0190(01)00337-4]
• 28: Segoufin, L. 2006. Automata and logics for words and trees over an infinite alphabet. In Proceedings of the 20th International Workshop on Computer Science Logic (CSL). Lecture Notes in Computer Science, vol. 4207. Springer, 41--57.
• 29: Moshe Y. Vardi, An automata-theoretic approach to linear temporal logic, Proceedings of the VIII Banff Higher order workshop conference on Logics for concurrency : structure versus automata: structure versus automata, p.238-266, April 1996, Banff, Canada
• 30: Igor Walukiewicz, Pushdown processes: games and model-checking, Information and Computation, v.164 n.2, p.234-263, Jan. 29, 2001 [doi>10.1006/inco.2000.2894]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Temporal logic

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Decision problems

General Terms:
Algorithms, Verification

Keywords:
Computational complexity, expressiveness