{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T22:29:43Z","timestamp":1791412183023,"version":"4.3.3"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2009,4,1]],"date-time":"2009-04-01T00:00:00Z","timestamp":1238544000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["GR\/S52759\/01"],"award-info":[{"award-number":["GR\/S52759\/01"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2009,4]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/1507244.1507246","type":"journal-article","created":{"date-parts":[[2009,4,15]],"date-time":"2009-04-15T13:37:07Z","timestamp":1239802627000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":161,"title":["LTL with the freeze quantifier and register automata"],"prefix":"10.1145","volume":"10","author":[{"given":"St\u00e9phane","family":"Demri","sequence":"first","affiliation":[{"name":"LSV, CNRS &amp; ENS Cachan &amp; INRIA Futurs, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ranko","family":"Lazi\u0107","sequence":"additional","affiliation":[{"name":"University of Warwick, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2009,4,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/174644.174651"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.51"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74240-1_1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72734-7_13"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.31"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.08.003"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 11th International Conference on Foundations of Software Science and Computer Structurers (FoSSaCS). Lecture Notes in Computer Science","volume":"4962","author":"Demri S.","unstructured":"Demri , S. , Lazi\u0107 , 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. Demri, S., Lazi\u0107, 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."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.2307\/2370405"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2953"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/12.6.1017"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2003.1214891"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00215625"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90242-9"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802201"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11944836_35"},{"key":"e_1_2_1_17_1","volume-title":"The reachability problem requires exponential space. Tech. rep. 62","author":"Lipton R. J.","unstructured":"Lipton , R. J. 1976. The reachability problem requires exponential space. Tech. rep. 62 , Yale University . Lipton, R. J. 1976. The reachability problem requires exponential space. Tech. rep. 62, Yale University."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2005.34"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00646-1"},{"key":"e_1_2_1_20_1","volume-title":"Computation, Finite and Infinite Machines","author":"Minsky M.","unstructured":"Minsky , M. 1967. Computation, Finite and Infinite Machines . Prentice Hall . Minsky, M. 1967. Computation, Finite and Infinite Machines. Prentice Hall."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90049-5"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the 13th International Colloquium on Automata, Languages, and Programming (ICALP). Lecture Notes in Computer Science","volume":"226","author":"Muller D. E.","unstructured":"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. 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."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1013560.1013562"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11690634_15"},{"key":"e_1_2_1_25_1","unstructured":"Ouaknine J. and Worrell J. 2006b. Personal communication.  Ouaknine J. and Worrell J. 2006b. Personal communication."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00105-X"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(01)00337-4"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_3"},{"key":"e_1_2_1_29_1","series-title":"Lecture Notes in Computer Science","volume-title":"Banff Higher Order Works","author":"Vardi M. Y.","unstructured":"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. 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."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2894"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1507244.1507246","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1507244.1507246","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:29:37Z","timestamp":1750253377000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1507244.1507246"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,4]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,4]]}},"alternative-id":["10.1145\/1507244.1507246"],"URL":"https:\/\/doi.org\/10.1145\/1507244.1507246","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,4]]},"assertion":[{"value":"2006-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-04-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}