Document Open Access Logo

Nominal Tree Automata with Name Allocation

Authors Simon Prucker , Lutz Schröder

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.35.pdf
  • Filesize: 0.77 MB
  • 17 pages

Document Identifiers

Author Details

Simon Prucker
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Lutz Schröder
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Funding

Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) -– Projektnummer 517924115.

Cite AsGet BibTex

Simon Prucker and Lutz Schröder. Nominal Tree Automata with Name Allocation. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.35

Abstract

Data trees serve as an abstraction of structured data, such as XML documents. A number of specification formalisms for languages of data trees have been developed, many of them adhering to the paradigm of register automata, which is based on storing data values encountered on the tree in registers for subsequent comparison with further data values. Already on word languages, the expressiveness of such automata models typically increases with the power of control (e.g. deterministic, non-deterministic, alternating). Language inclusion is typically undecidable for non-deterministic or alternating models unless the number of registers is radically restricted, and even then often remains non-elementary. We present an automaton model for data trees that retains a reasonable level of expressiveness, in particular allows non-determinism and any number of registers, while admitting language inclusion checking in elementary complexity, in fact in parametrized exponential time. We phrase the description of our automaton model in the language of nominal sets, building on the recently introduced paradigm of explicit name allocation in nominal automata.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Data languages
  • tree automata
  • nominal automata
  • inclusion checking

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Jiří Adámek, Horst Herrlich, and George E. Strecker. Abstract and Concrete Categories. John Wiley and Sons, 1990. Reprint: URL: http://www.tac.mta.ca/tac/reprints/articles/17/tr17abs.html.
  2. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1998. Google Scholar
  3. Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log., 12(4):27:1-27:26, 2011. URL: https://doi.org/10.1145/1970398.1970403.
  4. Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota. Automata theory in nominal sets. Log. Methods Comput. Sci., 10(3), 2014. URL: https://doi.org/10.2168/LMCS-10(3:4)2014.
  5. Mikolaj Bojanczyk, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data trees and XML reasoning. J. ACM, 56(3):13:1-13:48, 2009. URL: https://doi.org/10.1145/1516512.1516515.
  6. Benedikt Bollig, Peter Habermehl, Martin Leucker, and Benjamin Monmege. A robust class of data languages and an application to learning. Log. Meth. Comput. Sci., 10(4), 2014. URL: https://doi.org/10.2168/LMCS-10(4:19)2014.
  7. Thomas Colcombet. Unambiguity in automata theory. In Descriptional Complexity of Formal Systems, DCFS 2015, volume 9118 of LNCS, pages 3-18. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-19225-3.
  8. Thomas Colcombet and Amaldev Manuel. μ-calculus on data words. CoRR, 2014. URL: https://arxiv.org/abs/1404.4827.
  9. Hubert Comon, Max Dauchet, Rémi Gilleron, Florent Jacquemard, Denis Lugiez, Christof Löding, Sophie Tison, and Marc Tommasi. Tree Automata Techniques and Applications. HAL Portal Inria, 2008. hal-03367725. URL: https://hal.inria.fr/hal-03367725/document.
  10. Wojciech Czerwiński and Lukasz Orlikowski. Reachability in vector addition systems is Ackermann-complete. CoRR, 2021. URL: https://arxiv.org/abs/2104.13866.
  11. Stéphane Demri and Ranko Lazić. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3):16:1-16:30, 2009. URL: https://doi.org/10.1145/1507244.1507246.
  12. Diego Figueira. Forward-XPath and extended register automata on data-trees. In Luc Segoufin, editor, Database Theory, ICDT 2010, pages 231-241. ACM, 2010. URL: https://doi.org/10.1145/1804669.1804699.
  13. Murdoch James Gabbay and Vincenzo Ciancia. Freshness and name-restriction in sets of traces with names. In Foundations of Software Science and Computation Structures, FOSSACS 2011, volume 6604 of LNCS, pages 365-380. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19805-2.
  14. Radu Grigore, Dino Distefano, Rasmus Petersen, and Nikos Tzevelekos. Runtime verification based on register automata. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2013, volume 7795 of LNCS, pages 260-276. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-36742-7_19.
  15. Orna Grumberg, Orna Kupferman, and Sarai Sheinvald. Model checking systems and specifications with parameterized atomic apropositions. In Automated Technology for Verification and Analysis, ATVA 2012, volume 7561 of LNCS, pages 122-136. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33386-6_11.
  16. Daniel Hausmann, Stefan Milius, and Lutz Schröder. A linear-time nominal μ-calculus with name allocation. In Filippo Bonchi and Simon J. Puglisi, editors, Mathematical Foundations of Computer Science, MFCS 2021, volume 202 of LIPIcs, pages 58:1-58:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.MFCS.2021.58.
  17. Falk Howar, Bengt Jonsson, and Frits Vaandrager. Combining black-box and white-box techniques for learning register automata. In Computing and Software Science - State of the Art and Perspectives, volume 10000 of LNCS, pages 563-588. Springer, 2019. URL: https://doi.org/10.1007/978-3-319-91908-9_26.
  18. Marcin Jurdziński and Ranko Lazić. Alternation-free modal mu-calculus for data trees. In Logic in Computer Science, LICS 2007, pages 131-140. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/LICS.2007.11.
  19. Marcin Jurdziński and Ranko Lazić. Alternating automata on data trees and XPath satisfiability. ACM Trans. Comput. Log., 12(3):19:1-19:21, 2011. URL: https://doi.org/10.1145/1929954.1929956.
  20. Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994. URL: https://doi.org/10.1016/0304-3975(94)90242-9.
  21. Michael Kaminski and Tony Tan. Tree automata over infinite alphabets. In Arnon Avron, Nachum Dershowitz, and Alexander Rabinovich, editors, Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, volume 4800 of LNCS, pages 386-423. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78127-1_21.
  22. Michael Kaminski and Daniel Zeitlin. Finite-memory automata with non-deterministic reassignment. Int. J. Found. Comput. Sci., 21(5):741-760, 2010. URL: https://doi.org/10.1142/S0129054110007532.
  23. Bartek Klin and Mateusz Łełyk. Scalar and vectorial μ-calculus with atoms. Log. Methods Comput. Sci., 15(4), 2019. URL: https://doi.org/10.23638/LMCS-15(4:5)2019.
  24. Klaas Kürtz, Ralf Küsters, and Thomas Wilke. Selecting theories and nonce generation for recursive protocols. In Formal methods in security engineering, FMSE 2007, pages 61-70. ACM, 2007. URL: https://doi.org/10.1145/1314436.1314445.
  25. Jérôme Leroux. The reachability problem for Petri nets is not primitive recursive. CoRR, 2021. URL: https://arxiv.org/abs/2104.12695.
  26. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In Logic in Computer Science, LICS 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785796.
  27. Amaldev Manuel, Anca Muscholl, and Gabriele Puppis. Walking on data words. Theory Comput. Sys., 59(2):180-208, 2016. URL: https://doi.org/10.1007/s00224-014-9603-3.
  28. Antoine Mottet and Karin Quaas. The containment problem for unambiguous register automata. In Theoretical Aspects of Computer Science, STACS 2019, volume 126 of LIPIcs, pages 53:1-53:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.STACS.2019.53.
  29. Frank Neven, Thomas Schwentick, and Victor Vianu. Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log., 5(3):403-435, 2004. URL: https://doi.org/10.1145/1013560.1013562.
  30. Daniela Petrişan. Investigations into Algebra and Topology over Nominal Sets. PhD thesis, University of Leicester, 2011. Google Scholar
  31. Andrew Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013. Google Scholar
  32. Simon Prucker and Lutz Schröder. Nominal tree automata with name allocation. CoRR, abs/2405.14272, 2024. URL: https://doi.org/10.48550/arXiv.2405.14272.
  33. Jan Rutten. Universal coalgebra: A theory of systems. Theor. Comput. Sci., 249:3-80, 2000. Google Scholar
  34. Lutz Schröder, Dexter Kozen, Stefan Milius, and Thorsten Wißmann. Nominal automata with name binding. In Foundations of Software Science and Computation Structures, FOSSACS 2017, volume 10203 of LNCS, pages 124-142, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_8.
  35. Helmut Seidl. Deciding equivalence of finite tree automata. SIAM J. Comput., 19(3):424-437, 1990. URL: https://doi.org/10.1137/0219027.
  36. Ryoma Senda, Yoshiaki Takata, and Hiroyuki Seki. Complexity results on register context-free grammars and register tree automata. In Theoretical Aspects of Computing, ICTAC 2018, volume 11187 of LNCS, pages 415-434. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02508-3_22.
  37. Tony Tan. Extending two-variable logic on data trees with order on data values and its automata. ACM Trans. Comput. Log., 15(1):8:1-8:39, 2014. URL: https://doi.org/10.1145/2559945.
  38. Szymon Torunczyk and Thomas Zeume. Register automata with extrema constraints, and an application to two-variable logic. Log. Methods Comput. Sci., 18(1), 2022. URL: https://doi.org/10.46298/LMCS-18(1:42)2022.
  39. Nikos Tzevelekos. Nominal Game Semantics. PhD thesis, University of Oxford, 2008. Google Scholar
  40. Henning Urbat, Daniel Hausmann, Stefan Milius, and Lutz Schröder. Nominal büchi automata with name allocation. In Serge Haddad and Daniele Varacca, editors, Concurrency Theory, CONCUR 2021, volume 203 of LIPIcs, pages 4:1-4:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.CONCUR.2021.4.
  41. Gerco van Heerdt, Tobias Kappé, Jurriaan Rot, Matteo Sammartino, and Alexandra Silva. Tree automata as algebras: Minimisation and determinisation. In Algebra and Coalgebra in Computer Science, CALCO 2019, volume 139 of LIPIcs, pages 6:1-6:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CALCO.2019.6.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact