Alternating register automata on finite words and trees

Diego Figueira

doi:10.2168/LMCS-8(1:22)2012

Diego Figueira - Alternating register automata on finite words and trees

lmcs:907 - Logical Methods in Computer Science, March 9, 2012, Volume 8, Issue 1 - https://doi.org/10.2168/LMCS-8(1:22)2012

Alternating register automata on finite words and treesArticle

Authors: Diego Figueira

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.

https://doi.org/10.2168/LMCS-8(1:22)2012

Source: arXiv.org:1202.3957

Volume: Volume 8, Issue 1

Secondary volumes: Selected Papers of the 13th International Conference on Database Theory (ICDT 2010)

Published on: March 9, 2012

Imported on: November 5, 2010

Keywords: Computer Science - Databases, Computer Science - Formal Languages and Automata Theory, Computer Science - Logic in Computer Science, I.7.2, H.2.3, H.2.3

Licence: arXiv.org - Non-exclusive license to distribute

Funding:

Source : OpenAIRE Graph

Foundations of XML - Safe Processing of Dynamic Data over the Internet; Funder: European Commission; Code: 233599
Towards Improved Logics For Reasoning About Security; Funder: National Science Foundation; Code: 0208535

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

23 Documents citing this article

Ansuman Banerjee;Kingshuk Chatterjee;Shibashis Guha, 2023, Set Augmented Finite Automata over Infinite Alphabets, Lecture notes in computer science, pp. 36-50, 10.1007/978-3-031-33264-7_4.

Ryoma Senda;Yoshiaki Takata;Hiroyuki Seki, 2022, Complexity results on register context-free grammars and related formalisms, Theoretical Computer Science, 923, pp. 99-125, 10.1016/j.tcs.2022.04.055, https://doi.org/10.1016/j.tcs.2022.04.055.

Schmitz, Sylvain, 2021, Branching in Well-Structured Transition Systems (Invited Talk), DROPS (Schloss Dagstuhl – Leibniz Center for Informatics), 10.4230/lipics.csl.2021.3, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.3.

Antoine Mottet;Karin Quaas, 2020, The Containment Problem for Unambiguous Register Automata and Unambiguous Timed Automata, Theory of Computing Systems, 65, 4, pp. 706-735, 10.1007/s00224-020-09997-2.

Clovis Eberhart;Bartek Klin, 2019, History-Dependent Nominal μ-Calculus, SPIRE - Sciences Po Institutional REpository, 65, pp. 1-13, 10.1109/lics.2019.8785736.

David Baelde;Anthony Lick;Sylvain Schmitz, 2019, Decidable XPath Fragments in the Real World, SPIRE - Sciences Po Institutional REpository, pp. 285-302, 10.1145/3294052.3319685, https://inria.hal.science/hal-01852475.

Karin Quaas;Mahsa Shirmohammadi, 2019, Synchronizing Data Words for Register Automata, arXiv (Cornell University), 20, 2, pp. 1-27, 10.1145/3309760, http://arxiv.org/abs/1710.02329.

Diego Figueira, 2018, Satisfiability of Xpath on data trees, ACM SIGLOG News, 5, 2, pp. 4-16, 10.1145/3212019.3212021, https://doi.org/10.1145/3212019.3212021.

Ryoma Senda;Yoshiaki Takata;Hiroyuki Seki, 2018, Complexity Results on Register Context-Free Grammars and Register Tree Automata, Lecture notes in computer science, pp. 415-434, 10.1007/978-3-030-02508-3_22.

Sergio Abriola;Diego Figueira;Santiago Figueira, 2017, Logics of Repeating Values on Data Trees and Branching Counter Systems, Lecture notes in computer science, pp. 196-212, 10.1007/978-3-662-54458-7_12.

Taolue Chen;Fu Song;Zhilin Wu, 2017, Formal Reasoning on Infinite Data Values: An Ongoing Quest, Lecture notes in computer science, pp. 195-257, 10.1007/978-3-319-56841-6_6.

Wojciech Czerwiński;Claire David;Filip Murlak;Paweł Parys, 2017, Reasoning about integrity constraints for tree-structured data, 62, 4, pp. 941-976, 10.1007/s00224-017-9771-z, https://hal.science/hal-01799446.

Fu Song;Zhilin Wu, 2016, On temporal logics with data variable quantifications: Decidability and complexity, Information and Computation, 251, pp. 104-139, 10.1016/j.ic.2016.08.002.

Normann Decker;Daniel Thoma, 2016, On Freeze LTL with Ordered Attributes, Lecture notes in computer science, pp. 269-284, 10.1007/978-3-662-49630-5_16.

Sylvain Schmitz, 2016, Complexity Hierarchies beyond Elementary, arXiv (Cornell University), 8, 1, pp. 1-36, 10.1145/2858784, http://arxiv.org/abs/1312.5686.

Azadeh Farzan;Matthias Heizmann;Jochen Hoenicke;Zachary Kincaid;Andreas Podelski, 2015, Automated Program Verification, Lecture notes in computer science, pp. 25-46, 10.1007/978-3-319-15579-1_2.

Azadeh Farzan;Zachary Kincaid;Andreas Podelski, 2015, Proof Spaces for Unbounded Parallelism, ACM SIGPLAN Notices, 50, 1, pp. 407-420, 10.1145/2775051.2677012.

Parosh Aziz Abdulla;Mohamed Faouzi Atig;Ahmet Kara;Othmane Rezine, 2015, Verification of Buffered Dynamic Register Automata, Lecture notes in computer science, pp. 15-31, 10.1007/978-3-319-26850-7_2.

Azadeh Farzan;Zachary Kincaid;Andreas Podelski, 2014, Proof Spaces for Unbounded Parallelism, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 407-420, 10.1145/2676726.2677012.

Tony Tan, 2014, Extending two-variable logic on data trees with order on data values and its automata, Document Server@UHasselt (UHasselt), 15, 1, pp. 1-39, 10.1145/2559945, http://hdl.handle.net/1942/16522.

Anudhyan Boral;Sylvain Schmitz, 2013, Model-Checking Parse Trees, arXiv (Cornell University), 57, pp. 153-162, 10.1109/lics.2013.21, http://arxiv.org/abs/1211.5256.

Leonid Libkin;Tony Tan;Domagoj Vrgoč, 2013, Regular Expressions with Binding over Data Words for Querying Graph Databases, Lecture notes in computer science, pp. 325-337, 10.1007/978-3-642-38771-5_29.

Orna Grumberg;Orna Kupferman;Sarai Sheinvald, 2013, An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications, Lecture notes in computer science, pp. 397-411, 10.1007/978-3-319-02444-8_28.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3464 times.

This article's PDF has been downloaded 645 times.