Stéphane Demri
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.
- Alur, R. and Henzinger, T. 1994. A really temporal logic. J. ACM 41, 1, 181--204. Google Scholar
Digital Library
- Bojańczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., and David, C. 2006. Two-Variable logic on words with data. In Proceedings of the 21st IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 7--16. Google ScholarDigital Library
- Bouajjani, A., Habermehl, P., Jurski, Y., and Sighireanu, M. 2007. Rewriting systems with data. In Proceedings of the 16th International Symposium on Fundamentals of Computer Theory (FCT). Lecture Notes in Computer Science, vol. 4639. Springer, 1--22. Google ScholarDigital Library
- David, C. 2004. Mots et données infinies. M.S. thesis, Laboratoire d'Informatique Algorithmique: Fondements et Applications, Paris.Google Scholar
- Demri, S., D'Souza, D., and Gascon, R. 2007. A decidable temporal logic of repeating values. In Proceedings of the International Symposium on Logical Foundations of Computer Science (LFCS). Lecture Notes in Computer Science, vol. 4514. Springer, 180--194. Google ScholarDigital Library
- Demri, S. and Lazić, R. 2006. LTL with the freeze quantifier and register automata. In Proceedings of the 21st IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 17--26. Google ScholarDigital Library
- Demri, S., Lazić, R., and Nowak, D. 2007. On the freeze quantifier in Constraint LTL: Decidability and complexity. Inf. Comput. 205, 1, 2--24. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Dickson, L. 1913. Finiteness of the odd perfect and primitive abundant numbers with distinct factors. Amer. J. Math. 35, 413--422.Google ScholarCross Ref
- Etessami, K., Vardi, M., and Wilke, T. 2002. First-Order logic with two variables and unary temporal logic. Inf. Comput. 179, 2, 279--295. Google ScholarDigital Library
- Fitting, M. 2002. Modal logic between propositional and first-order. J. Logic Comput. 12, 6, 1017--1026.Google ScholarCross Ref
- 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.Google ScholarCross Ref
- Goranko, V. 1996. Hierarchies of modal and temporal logics with references pointers. J. Logic, Lang. Inf. 5, 1--24.Google ScholarCross Ref
- Kaminski, M. and Francez, N. 1994. Finite-Memory automata. Theor. Comput. Sci. 134, 2, 329--363. Google ScholarDigital Library
- Kosaraju, S. R. 1982. Decidability of reachability in vector addition systems (preliminary version). In Proceedings of the 14th Annual ACM Symposium on Theory of Computing (STOC). ACM, 267--281. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Lipton, R. J. 1976. The reachability problem requires exponential space. Tech. rep. 62, Yale University.Google Scholar
- Lisitsa, A. and Potapov, I. 2005. Temporal logic with predicate λ -abstraction. In Proceedings of the12th International Symposium on Temporal Representation and Reasoning (TIME). IEEE Computer Society, 147--155. Google ScholarDigital Library
- Mayr, R. 2003. Undecidable problems in unreliable computations. Theor. Comput. Sci. 297, 1-3, 337--354. Google ScholarDigital Library
- Minsky, M. 1967. Computation, Finite and Infinite Machines. Prentice Hall. Google ScholarDigital Library
- Miyano, S. and Hayashi, T. 1984. Alternating finite automata on ω-words. Theor. Comput. Sci. 32, 321--330.Google ScholarCross Ref
- Muller, D. E., Saoudi, A., and Schupp, P. E. 1986. Alternating automata, the weak monadic theory of the tree, and its complexity. In Proceedings of the 13th International Colloquium on Automata, Languages, and Programming (ICALP). Lecture Notes in Computer Science, vol. 226. Springer, 275--283. Google ScholarDigital Library
- Neven, F., Schwentick, T., and Vianu, V. 2004. Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Logic 5, 3, 403--435. Google ScholarDigital Library
- Ouaknine, J. and Worrell, J. 2006a. On metric temporal logic and faulty Turing machines. In Proceedings of the 9th International Conference on Foundations of Software Science and Computer Structures (FoSSaCS). Lecture Notes in Computer Science, vol. 3921. Springer, 217--230. Google ScholarDigital Library
- Ouaknine, J. and Worrell, J. 2006b. Personal communication.Google Scholar
- Sakamoto, H. and Ikeda, D. 2000. Intractability of decision problems for finite-memory automata. Theor. Comput. Sci. 231, 2, 297--308. Google ScholarDigital Library
- Schnoebelen, P. 2002. Verifying lossy channel systems has nonprimitive recursive complexity. Inf. Process. Lett. 83, 5, 251--261. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Vardi, M. Y. 1996. An automata-theoretic approach to linear temporal logic. In Banff Higher Order Works. Lecture Notes in Computer Science, vol. 1043. Springer, 238--266. Google ScholarDigital Library
- Walukiewicz, I. 2001. Pushdown processes: Games and model-checking. Inf. Comput. 164, 2, 234--263. Google ScholarDigital Library
Index Terms
- LTL with the freeze quantifier and register automata
Recommendations
LTL with the Freeze Quantifier and Register Automata
LICS '06: Proceedings of the 21st Annual IEEE Symposium on Logic in Computer ScienceTemporal logics, first-order logics, and automata over data words have recently attracted considerable attention. A data word is a word over a finite alphabet, together with a datum (an element of an infinite domain) at each position. Examples include ...
On the freeze quantifier in Constraint LTL: Decidability and complexity
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 ...
Model checking freeze LTL over one-counter automata
FOSSACS'08/ETAPS'08: Proceedings of the Theory and practice of software, 11th international conference on Foundations of software science and computational structuresWe study complexity issues related to the model-checking problem for LTL with registers (a.k.a. freeze LTL) over one-counter automata. We consider several classes of one-counter automata (mainly deterministic vs. nondeterministic) and several syntactic ...
Comments