{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T01:29:57Z","timestamp":1791250197067,"version":"4.1.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T00:00:00Z","timestamp":1309478400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Polish MNII","award":["4 T11C 042 25"],"award-info":[{"award-number":["4 T11C 042 25"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2011,7]]},"abstract":"<jats:p>\n            In a\n            <jats:italic>data word<\/jats:italic>\n            each position carries a label from a finite alphabet and a data value from some infinite domain. This model has been already considered in the realm of semistructured data, timed automata, and extended temporal logics.\n          <\/jats:p>\n          <jats:p>\n            This article shows that satisfiability for the two-variable fragment FO\n            <jats:sup>2<\/jats:sup>\n            (\u223c,&lt;,+1) of first-order logic with data equality test \u223c is decidable over finite and infinite data words. Here +1 and &lt; are the usual successor and order predicates, respectively. The satisfiability problem is shown to be at least as hard as reachability in Petri nets. Several extensions of the logic are considered; some remain decidable while some are undecidable.\n          <\/jats:p>","DOI":"10.1145\/1970398.1970403","type":"journal-article","created":{"date-parts":[[2011,7,21]],"date-time":"2011-07-21T13:27:09Z","timestamp":1311254829000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":111,"title":["Two-variable logic on data words"],"prefix":"10.1145","volume":"12","author":[{"given":"Miko\u0142aj","family":"Boja\u0144czyk","sequence":"first","affiliation":[{"name":"Warsaw University, Warsaw, Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Claire","family":"David","sequence":"additional","affiliation":[{"name":"LIAFA, Paris VII, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anca","family":"Muscholl","sequence":"additional","affiliation":[{"name":"Bordeaux University, Talence Cedex, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Schwentick","sequence":"additional","affiliation":[{"name":"TU Dortmund, Dortmund, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Luc","family":"Segoufin","sequence":"additional","affiliation":[{"name":"INRIA, Cachan Cedex, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2011,7,22]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 34th International Colloquium on Automata, Languages and Programming (ICALP'07)","volume":"4596","author":"Bj\u00f6rklund H.","unstructured":"Bj\u00f6rklund , H. and Boja\u0144czyk , M . 2007a. Bounded depth data trees . In Proceedings of the 34th International Colloquium on Automata, Languages and Programming (ICALP'07) . Lecture Notes in Computer Science , vol. 4596 , Springer-Verlag, Berlin, Germany, 862--874. Bj\u00f6rklund, H. and Boja\u0144czyk, M. 2007a. Bounded depth data trees. In Proceedings of the 34th International Colloquium on Automata, Languages and Programming (ICALP'07). Lecture Notes in Computer Science, vol. 4596, Springer-Verlag, Berlin, Germany, 862--874."},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the 32nd Mathematical Foundations of Computer Science International Symposium (MFCS'07)","volume":"4708","author":"Bj\u00f6rklund H.","unstructured":"Bj\u00f6rklund , H. and Boja\u0144czyk , M . 2007b. Shuffle expressions and words with nested data . In Proceedings of the 32nd Mathematical Foundations of Computer Science International Symposium (MFCS'07) . Lecture Notes in Computer Science , vol. 4708 , Springer-Verlag, Berlin, Germany, 750--761. Bj\u00f6rklund, H. and Boja\u0144czyk, M. 2007b. Shuffle expressions and words with nested data. In Proceedings of the 32nd Mathematical Foundations of Computer Science International Symposium (MFCS'07). Lecture Notes in Computer Science, vol. 4708, Springer-Verlag, Berlin, Germany, 750--761."},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 16th International Symposium on Fundamentals of Computation Theory (FCT'07)","volume":"4639","author":"Bj\u00f6rklund H.","unstructured":"Bj\u00f6rklund , H. and Schwentick , T . 2007. On notions of regularity for data languages . In Proceedings of the 16th International Symposium on Fundamentals of Computation Theory (FCT'07) . Lecture Notes in Computer Science , vol. 4639 , Springer-Verlag, Berlin, Germany, 88--99. Bj\u00f6rklund, H. and Schwentick, T. 2007. On notions of regularity for data languages. In Proceedings of the 16th International Symposium on Fundamentals of Computation Theory (FCT'07). Lecture Notes in Computer Science, vol. 4639, Springer-Verlag, Berlin, Germany, 88--99."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1142351.1142354"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1516512.1516515"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.51"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00038-5"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1507244.1507246"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.08.003"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.2307\/2370405"},{"key":"e_1_2_1_11_1","first-page":"143","article-title":"Decidability issues for Petri nets\u2014a survey","volume":"30","author":"Esparza J.","year":"1994","unstructured":"Esparza , J. and Nielsen , M. 1994 . Decidability issues for Petri nets\u2014a survey . Elektron. Inform. Kybernet. 30 , 3, 143 -- 160 . Esparza, J. and Nielsen, M. 1994. Decidability issues for Petri nets\u2014a survey. Elektron. Inform. Kybernet. 30, 3, 143--160.","journal-title":"Elektron. Inform. Kybernet."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2953"},{"key":"e_1_2_1_13_1","series-title":"Lecture Notes in Computer Science","volume-title":"Logic and Machines: Decision Problems and Complexity","author":"F\u00fcrer M.","unstructured":"F\u00fcrer , M. 1984. The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems) . In Logic and Machines: Decision Problems and Complexity . Lecture Notes in Computer Science , vol. 171 , Springer-Verlag , Berlin, Germany , 312--319. F\u00fcrer, M. 1984. The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems). In Logic and Machines: Decision Problems and Complexity. Lecture Notes in Computer Science, vol. 171, Springer-Verlag, Berlin, Germany, 312--319."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/358746.358767"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00308-9"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021843"},{"key":"e_1_2_1_17_1","unstructured":"Hopcroft J. E. and Ullman J. D. 1979. Introduction to Automata Theory Languages and Computation. Addison-Wesley Reading MA.   Hopcroft J. E. and Ullman J. D. 1979. Introduction to Automata Theory Languages and Computation. Addison-Wesley Reading MA."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90242-9"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.49"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802201"},{"key":"e_1_2_1_21_1","volume-title":"The reachability problem requires exponential space. Tech. rep. 62","author":"Lipton R.","unstructured":"Lipton , R. 1976. The reachability problem requires exponential space. Tech. rep. 62 , Yale University , New Haven, CT . Lipton, R. 1976. The reachability problem requires exponential space. Tech. rep. 62, Yale University, New Haven, CT."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1137\/0213029"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19750210118"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1013560.1013562"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.2307\/2695037"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the 5th International Conference on Developments in Language Theory (DLT'01)","volume":"2295","author":"Schwentick T.","unstructured":"Schwentick , T. , Th\u00e9rien , D. , and Vollmer , H . 2001. Partially-ordered two-way automata: A new characterization of DA . In Proceedings of the 5th International Conference on Developments in Language Theory (DLT'01) . Lecture Notes in Computer Science , vol. 2295 , Springer-Verlag, Berlin, Germany, 239--250. Schwentick, T., Th\u00e9rien, D., and Vollmer, H. 2001. Partially-ordered two-way automata: A new characterization of DA. In Proceedings of the 5th International Conference on Developments in Language Theory (DLT'01). Lecture Notes in Computer Science, vol. 2295, Springer-Verlag, Berlin, Germany, 239--250."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1085"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/276698.276749"},{"key":"e_1_2_1_29_1","first-page":"3","article-title":"Structure theorem and strict alternation hierarchy for FO2 on words","volume":"5","author":"Weis P.","year":"2009","unstructured":"Weis , P. and Immerman , N. 2009 . Structure theorem and strict alternation hierarchy for FO2 on words . Logic. Meth. Comp. Sci. 5 , 3 . Weis, P. and Immerman, N. 2009. Structure theorem and strict alternation hierarchy for FO2 on words. Logic. Meth. Comp. Sci. 5, 3.","journal-title":"Logic. Meth. Comp. Sci."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1970398.1970403","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1970398.1970403","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:52:53Z","timestamp":1750243973000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1970398.1970403"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7]]},"references-count":29,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011,7]]}},"alternative-id":["10.1145\/1970398.1970403"],"URL":"https:\/\/doi.org\/10.1145\/1970398.1970403","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,7]]},"assertion":[{"value":"2007-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-07-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}