{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:11:04Z","timestamp":1760202664573,"version":"3.41.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,2,1]],"date-time":"2014-02-01T00:00:00Z","timestamp":1391212800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003130","name":"Fonds Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100003130","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":[[2014,2]]},"abstract":"<jats:p>Data trees are trees in which each node, besides carrying a label from a finite alphabet, also carries a data value from an infinite domain. They have been used as an abstraction model for reasoning tasks on XML and verification. However, most existing approaches consider the case where only equality test can be performed on the data values.<\/jats:p>\n          <jats:p>\n            In this article we study data trees in which the data values come from a linearly ordered domain, and in addition to equality test, we can test whether the data value in a node is greater than the one in another node. We introduce an automata model for them which we call\n            <jats:italic>ordered-data tree automata<\/jats:italic>\n            (ODTA), provide its logical characterisation, and prove that its non-emptiness problem is decidable in 3-NE\n            <jats:sc>xp<\/jats:sc>\n            T\n            <jats:sc>ime<\/jats:sc>\n            . We also show that the two-variable logic on unranked data trees, studied by Bojanczyk et al. [2009], corresponds precisely to a special subclass of this automata model.\n          <\/jats:p>\n          <jats:p>\n            Then we define a slightly weaker version of ODTA, which we call\n            <jats:italic>weak ODTA<\/jats:italic>\n            , and provide its logical characterisation. The complexity of the non-emptiness problem drops to NP. However, a number of existing formalisms and models studied in the literature can be captured already by weak ODTA. We also show that the definition of ODTA can be easily modified, to the case where the data values come from a tree-like partially ordered domain, such as strings.\n          <\/jats:p>","DOI":"10.1145\/2559945","type":"journal-article","created":{"date-parts":[[2014,3,4]],"date-time":"2014-03-04T13:24:59Z","timestamp":1393939499000},"page":"1-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Extending two-variable logic on data trees with order on data values and its automata"],"prefix":"10.1145","volume":"15","author":[{"given":"Tony","family":"Tan","sequence":"first","affiliation":[{"name":"Hasselt University and Transnational University of Limburg"}]}],"member":"320","published-online":{"date-parts":[[2014,3,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(03)00032-1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1137\/050646895"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 24th International Workshop on Computer Science Logic (CSL'10)","volume":"6247","author":"Benedikt M.","unstructured":"M. Benedikt , C. Ley , and G. Puppis . 2010. Automata vs. logics on data words . In Proceedings of the 24th International Workshop on Computer Science Logic (CSL'10) . Lecture Notes in Computer Science , vol. 6247 , Springer-Verlag, Berlin, 110--124. M. Benedikt, C. Ley, and G. Puppis. 2010. Automata vs. logics on data words. In Proceedings of the 24th International Workshop on Computer Science Logic (CSL'10). Lecture Notes in Computer Science, vol. 6247, Springer-Verlag, Berlin, 110--124."},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 34th International Colloquium on Automata, Languages and Programming (ICALP'07)","volume":"4596","author":"Bj\u00f6rklund H.","unstructured":"H. Bj\u00f6rklund and M. Bojanczyk . 2007. 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, 862--874. H. Bj\u00f6rklund and M. Bojanczyk. 2007. 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, 862--874."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85238-4_10"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1970398.1970403"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.48"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1516512.1516515"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 12th International Conference on Concurrency Theory (CONCUR'01)","volume":"2154","author":"Bouyer P.","unstructured":"P. Bouyer , A. Petit , and D. Th\u00e9rien . 2001. An algebraic characterization of data and timed languages . In Proceedings of the 12th International Conference on Concurrency Theory (CONCUR'01) . Lecture Notes in Computer Science , vol. 2154 , Springer-Verlag, Berlin, 248--261. P. Bouyer, A. Petit, and D. Th\u00e9rien. 2001. An algebraic characterization of data and timed languages. In Proceedings of the 12th International Conference on Concurrency Theory (CONCUR'01). Lecture Notes in Computer Science, vol. 2154, Springer-Verlag, Berlin, 248--261."},{"key":"e_1_2_1_10_1","unstructured":"H. Comon M. Dauchet R. Gilleron C. L\u00f6ding F. Jacquemard D. Lugiez S. Tison and M. Tommasi. 2007. Tree automata techniques and applications. http:\/\/www.grappa.univ-lille3.fr\/tata. (Last accessed 10\/07).  H. Comon M. Dauchet R. Gilleron C. L\u00f6ding F. Jacquemard D. Lugiez S. Tison and M. Tommasi. 2007. Tree automata techniques and applications. http:\/\/www.grappa.univ-lille3.fr\/tata. (Last accessed 10\/07)."},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17)","volume":"6397","author":"David C.","unstructured":"C. David , L. Libkin , and T. Tan . 2010. On the satisfiability of two-variable logic over data words . In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17) . Lecture Notes in Computer Science , vol. 6397 , Springer-Verlag, Berlin, 248--262. C. David, L. Libkin, and T. Tan. 2010. On the satisfiability of two-variable logic over data words. In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17). Lecture Notes in Computer Science, vol. 6397, Springer-Verlag, Berlin, 248--262."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338626.2338632"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72734-7_13"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1507244.1507246"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1514894.1514924"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/567112.567117"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1559795.1559827"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.18"},{"key":"e_1_2_1_19_1","first-page":"1","article-title":"Alternating register automata on finite data words and trees","volume":"8","author":"Figueira D.","year":"2012","unstructured":"D. Figueira . 2012 a. Alternating register automata on finite data words and trees . Logic. Methods Comput. Sci. 8 , 1 . D. Figueira. 2012a. Alternating register automata on finite data words and trees. Logic. Methods Comput. Sci. 8, 1.","journal-title":"Logic. Methods Comput. Sci."},{"key":"e_1_2_1_20_1","unstructured":"D. Figueira. 2012b. Satisfiability for two-variable logic with two successor relations on finite linear orders. http:\/\/arxiv.org\/abs\/1204.2495.  D. Figueira. 2012b. Satisfiability for two-variable logic with two successor relations on finite linear orders. http:\/\/arxiv.org\/abs\/1204.2495."},{"volume-title":"Proceedings of the 17th International Workshop on Expressiveness in Concurrency (EXPRESS'10)","author":"Figueira D.","key":"e_1_2_1_21_1","unstructured":"D. Figueira , P. Hofman , and S. Lasota . 2010. Relating timed and register automata . In Proceedings of the 17th International Workshop on Expressiveness in Concurrency (EXPRESS'10) . D. Figueira, P. Hofman, and S. Lasota. 2010. Relating timed and register automata. In Proceedings of the 17th International Workshop on Expressiveness in Concurrency (EXPRESS'10)."},{"volume-title":"Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS'11)","author":"Figueira D.","key":"e_1_2_1_22_1","unstructured":"D. Figueira and L. Segoufin . 2011. Bottom-up automata on data trees and vertical XPath . In Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS'11) . D. Figueira and L. Segoufin. 2011. Bottom-up automata on data trees and vertical XPath. In Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS'11)."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13089-2_47"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.2307\/2274706"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929954.1929956"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90242-9"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28332-1_30"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1877714.1877716"},{"volume-title":"Elements of Finite Model Theory. Texts in Theoretical Computer Science","author":"Libkin L.","key":"e_1_2_1_29_1","unstructured":"L. Libkin . 2004. Elements of Finite Model Theory. Texts in Theoretical Computer Science , Springer . L. Libkin. 2004. Elements of Finite Model Theory. Texts in Theoretical Computer Science, Springer."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1885577.1885622"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/647852.737555"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1013560.1013562"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/974121.974140"},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the 24th International Workshop on Computer Science Logic (CSL'10)","volume":"6247","author":"Schwentick T.","unstructured":"T. Schwentick and T. Zeume . 2010. Two-variable logic with two order relations . In Proceedings of the 24th International Workshop on Computer Science Logic (CSL'10) . Lecture Notes in Computer Science , vol. 6247 , Springer-Verlag, Berlin, 499--513. T. Schwentick and T. Zeume. 2010. Two-variable logic with two order relations. In Proceedings of the 24th International Workshop on Computer Science Logic (CSL'10). Lecture Notes in Computer Science, vol. 6247, Springer-Verlag, Berlin, 499--513."},{"volume-title":"Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS'11)","author":"Segoufin L.","key":"e_1_2_1_35_1","unstructured":"L. Segoufin and S. Torunczyk . 2011. Automata based verification over linearly ordered data domains . In Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS'11) . L. Segoufin and S. Torunczyk. 2011. Automata based verification over linearly ordered data domains. In Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS'11)."},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the 31st International Colloquium on Automata, Languages and Programming (ICALP'04)","volume":"3142","author":"Seidl H.","unstructured":"H. Seidl , T. Schwentick , A. Muscholl , and P. Habermehl . 2004. Counting in trees for free . In Proceedings of the 31st International Colloquium on Automata, Languages and Programming (ICALP'04) . Lecture Notes in Computer Science , vol. 3142 , Springer-Verlag, Berlin, 1136--1149. H. Seidl, T. Schwentick, A. Muscholl, and P. Habermehl. 2004. Counting in trees for free. In Proceedings of the 31st International Colloquium on Automata, Languages and Programming (ICALP'04). Lecture Notes in Computer Science, vol. 3142, Springer-Verlag, Berlin, 1136--1149."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(67)80022-9"},{"volume-title":"Handbook of Formal Languages","author":"Thomas W.","key":"e_1_2_1_38_1","unstructured":"W. Thomas . 1997. Languages , automata, and logic . In Handbook of Formal Languages , vol. 3 , Beyond Words, Springer , 389--455. W. Thomas. 1997. Languages, automata, and logic. In Handbook of Formal Languages, vol. 3, Beyond Words, Springer, 389--455."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_25"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2559945","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2559945","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:10:25Z","timestamp":1750234225000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2559945"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["10.1145\/2559945"],"URL":"https:\/\/doi.org\/10.1145\/2559945","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2014,2]]},"assertion":[{"value":"2013-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-03-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}