{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T07:52:36Z","timestamp":1767772356766,"version":"3.41.2"},"reference-count":30,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,3,9]],"date-time":"2012-03-09T00:00:00Z","timestamp":1331251200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["233599"],"award-info":[{"award-number":["233599"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We study alternating register automata on data words and data trees in relation to logics. A data word (resp. data tree) is a word (resp. tree) whose every position carries a label from a finite alphabet and a data value from an infinite domain. We investigate one-way automata with alternating control over data words or trees, with one register for storing data and comparing them for equality. This is a continuation of the study started by Demri, Lazic and Jurdzinski. From the standpoint of register automata models, this work aims at two objectives: (1) simplifying the existent decidability proofs for the emptiness problem for alternating register automata; and (2) exhibiting decidable extensions for these models. From the logical perspective, we show that (a) in the case of data words, satisfiability of LTL with one register and quantification over data values is decidable; and (b) the satisfiability problem for the so-called forward fragment of XPath on XML documents is decidable, even in the presence of DTDs and even of key constraints. The decidability is obtained through a reduction to the automata model introduced. This fragment contains the child, descendant, next-sibling and following-sibling axes, as well as data equality and inequality tests.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:22)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":17,"title":["Alternating register automata on finite words and trees"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"given":"Diego","family":"Figueira","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,3,9]]},"reference":[{"key":"10.2168\/LMCS-8(1:22)2012_ACJT-lics96","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. General decidability theorems for infinite-state systems. InAnnual IEEE Symposium on Logic in Computer Science (LICS'96), pages 313-321, 1996.","DOI":"10.1109\/LICS.1996.561359"},{"key":"10.2168\/LMCS-8(1:22)2012_ADOW05","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla, Johann Deneux, Jo\u00ebl Ouaknine, and James Worrell. Decidability and complexity results for timed automata via channel machines. InInternational Colloquium on Automata, Languages and Programming (ICALP'05), pages 1089-1101, 2005.","DOI":"10.1007\/11523468_88"},{"key":"10.2168\/LMCS-8(1:22)2012_AD94","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"issue":"2","key":"10.2168\/LMCS-8(1:22)2012_BFG08","first-page":"1","volume":"55","author":"Michael Benedikt, Wenfei Fan, and Floris","year":"2008","journal-title":"Journal of the ACM"},{"issue":"3","key":"10.2168\/LMCS-8(1:22)2012_BMSS09:xml:jacm","first-page":"1","volume":"56","author":"Mikolaj Bojanczyk, Anca Mus","year":"2009","journal-title":"Journal of the ACM"},{"key":"10.2168\/LMCS-8(1:22)2012_CS-lics08","doi-asserted-by":"crossref","unstructured":"Pierre Chambart and Philippe Schnoebelen. The ordinal recursive complexity of lossy channel systems. InAnnual IEEE Symposium on Logic in Computer Science (LICS'08), pages 205-216. IEEE Computer Society Press, 2008.","DOI":"10.1109\/LICS.2008.47"},{"key":"10.2168\/LMCS-8(1:22)2012_xpath:w3c","unstructured":"James Clark and Steve DeRose. XML path language (XPath). Website, 1999. W3C Recommendation. http:\/\/www.w3.org\/TR\/xpath."},{"key":"10.2168\/LMCS-8(1:22)2012_DL-tocl08","doi-asserted-by":"crossref","unstructured":"St\u00e9phane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata.ACM Transactions on Computational Logic, 10(3), 2009.","DOI":"10.1145\/1507244.1507246"},{"key":"10.2168\/LMCS-8(1:22)2012_DLN05","doi-asserted-by":"crossref","unstructured":"St\u00e9phane Demri, Ranko Lazic, and David Nowak. On the freeze quantifier in constraint LTL: Decidability and complexity. InInternational Symposium on Temporal Representation and Reasoning (TIME'05), pages 113-121. IEEE Computer Society Press, 2005.","DOI":"10.1109\/TIME.2005.28"},{"key":"10.2168\/LMCS-8(1:22)2012_dicksonslem","doi-asserted-by":"publisher","DOI":"10.2307\/2370405"},{"key":"10.2168\/LMCS-8(1:22)2012_F09","doi-asserted-by":"crossref","unstructured":"Diego Figueira. Satisfiability of downward XPath with data equality tests. InACM Symposium on Principles of Database Systems (PODS'09), pages 197-206. ACM Press, 2009.","DOI":"10.1145\/1559795.1559827"},{"key":"10.2168\/LMCS-8(1:22)2012_Fig10","doi-asserted-by":"crossref","unstructured":"Diego Figueira. Forward-XPath and extended register automata on data-trees. InInternational Conference on Database Theory (ICDT'10). ACM Press, 2010.","DOI":"10.1145\/1804669.1804699"},{"key":"10.2168\/LMCS-8(1:22)2012_FigPhD","unstructured":"Diego Figueira.Reasoning on Words and Trees with Data. Ph.D. thesis, Laboratoire Sp\u00e9cification et V\u00e9rification, ENS Cachan, France, December 2010."},{"key":"10.2168\/LMCS-8(1:22)2012_Fig11","doi-asserted-by":"crossref","unstructured":"Diego Figueira. A decidable two-way logic on data words. InAnnual IEEE Symposium on Logic in Computer Science (LICS'11). IEEE Computer Society Press, 2011.","DOI":"10.1109\/LICS.2011.18"},{"key":"10.2168\/LMCS-8(1:22)2012_FFSS10","doi-asserted-by":"crossref","unstructured":"Diego Figueira, Santiago Figueira, Sylvain Schmitz, and Philippe Schnoebelen. Ackermannian and primitive-recursive bounds with Dickson's lemma. InAnnual IEEE Symposium on Logic in Computer Science (LICS'11). IEEE Computer Society Press, 2011.","DOI":"10.1109\/LICS.2011.39"},{"key":"10.2168\/LMCS-8(1:22)2012_FHL10","doi-asserted-by":"crossref","unstructured":"Diego Figueira, Piotr Hofman, and Slawomir Lasota. Relating timed and register automata. InInternational Workshop on Expressiveness in Concurrency (EXPRESS'10), 2010.","DOI":"10.4204\/EPTCS.41.5"},{"key":"10.2168\/LMCS-8(1:22)2012_FS09","doi-asserted-by":"crossref","unstructured":"Diego Figueira and Luc Segoufin. Future-looking logics on data words and trees. InInternational Symposium on Mathematical Foundations of Computer Science (MFCS'09), volume 5734 ofLNCS, pages 331-343. Springer, 2009.","DOI":"10.1007\/978-3-642-03816-7_29"},{"key":"10.2168\/LMCS-8(1:22)2012_FS10","unstructured":"Diego Figueira and Luc Segoufin. Bottom-up automata on data trees and vertical XPath. InInternational Symposium on Theoretical Aspects of Computer Science (STACS'11). Springer, 2011."},{"key":"10.2168\/LMCS-8(1:22)2012_FS01","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"10.2168\/LMCS-8(1:22)2012_GF05","doi-asserted-by":"crossref","unstructured":"Floris Geerts and Wenfei Fan. Satisfiability of XPath queries with sibling axes. InInternational Symposium on Database Programming Languages (DBPL'05), volume 3774 ofLecture Notes in Computer Science, pages 122-137. Springer, 2005.","DOI":"10.1007\/11601524_8"},{"key":"10.2168\/LMCS-8(1:22)2012_GKP05","doi-asserted-by":"publisher","DOI":"10.1145\/1071610.1071614"},{"key":"10.2168\/LMCS-8(1:22)2012_higmanslem","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-2.1.326"},{"key":"10.2168\/LMCS-8(1:22)2012_JL07","doi-asserted-by":"crossref","unstructured":"Marcin Jurdzinski and Ranko Lazic. Alternation-free modal mu-calculus for data trees. InAnnual IEEE Symposium on Logic in Computer Science (LICS'07), pages 131-140. IEEE Computer Society Press, 2007.","DOI":"10.1109\/LICS.2007.11"},{"issue":"3","key":"10.2168\/LMCS-8(1:22)2012_JL08","first-page":"19","volume":"12","author":"Marcin Jurdzinski and Ranko Lazic","year":"2011","journal-title":"ACM Transactions on Computational Logic"},{"issue":"2","key":"10.2168\/LMCS-8(1:22)2012_Kr60","first-page":"210","volume":"95","author":"Joseph B. Kruskal","year":"1960","journal-title":"Transactions of the American Mathematical Society 95(2):210-225, 1960"},{"key":"10.2168\/LMCS-8(1:22)2012_fast","doi-asserted-by":"publisher","DOI":"10.1007\/BF01967649"},{"key":"10.2168\/LMCS-8(1:22)2012_M04","doi-asserted-by":"crossref","unstructured":"Maarten Marx. XPath with conditional axis relations. InInternational Conference on Extending Database Technology (EDBT'04), volume 2992 ofLecture Notes in Computer Science, pages 477-494. Springer, 2004.","DOI":"10.1007\/978-3-540-24741-8_28"},{"key":"10.2168\/LMCS-8(1:22)2012_phs-mfcs2010","doi-asserted-by":"crossref","unstructured":"Philippe Schnoebelen. Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. InInternational Symposium on Mathematical Foundations of Computer Science (MFCS'10), volume 6281 ofLecture Notes in Computer Science, pages 616-628. Springer, 2010.","DOI":"10.1007\/978-3-642-15155-2_54"},{"key":"10.2168\/LMCS-8(1:22)2012_tC06","doi-asserted-by":"crossref","unstructured":"Balder ten Cate. The expressivity of XPath with transitive closure. InACM Symposium on Principles of Database Systems (PODS'06), pages 328-337. ACM Press, 2006.","DOI":"10.1145\/1142351.1142398"},{"key":"10.2168\/LMCS-8(1:22)2012_tCS08","doi-asserted-by":"crossref","unstructured":"Balder ten Cate and Luc Segoufin. XPath, transitive closure logic, and nested tree walking automata. InACM Symposium on Principles of Database Systems (PODS'08), pages 251-260. ACM Press, 2008.","DOI":"10.1145\/1376916.1376952"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/907\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/907\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T23:10:18Z","timestamp":1744067418000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/907"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,9]]},"references-count":30,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:22)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1202.3957","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1202.3957","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,3,9]]},"article-number":"907"}}