Document Open Access Logo

Tree Automata with Global Constraints for Infinite Trees

Authors Patrick Landwehr, Christof Löding

PDF

File

Thumbnail PDF
PDF
LIPIcs.STACS.2019.47.pdf
  • Filesize: 480 kB
  • 15 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • Tree automata
  • infinite trees
  • global constraints

Metrics

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

Abstract

We study an extension of tree automata on infinite trees with global equality and disequality constraints. These constraints can enforce that all subtrees for which in the accepting run a state q is reached (at the root of that subtree) are identical, or that these trees differ from the subtrees at which a state q' is reached. We consider the closure properties of this model and its decision problems. While the emptiness problem for the general model remains open, we show the decidability of the emptiness problem for the case that the given automaton only uses equality constraints.

Cite As Get BibTex

Patrick Landwehr and Christof Löding. Tree Automata with Global Constraints for Infinite Trees. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 126, pp. 47:1-47:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.STACS.2019.47

Author Details

Patrick Landwehr
  • RWTH Aachen University, Germany
Christof Löding
  • RWTH Aachen University, Germany

Acknowledgements

We thank Arnaud Carayol for discussions on the subject.

References

  1. Franz Baader and Alexander Okhotin. Solving Language Equations and Disequations with Applications to Disunification in Description Logics and Monadic Set Constraints. In Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, volume 7180 of Lecture Notes in Computer Science, pages 107-121. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-28717-6.
  2. Luis Barguñó, Carles Creus, Guillem Godoy, Florent Jacquemard, and Camille Vacher. The Emptiness Problem for Tree Automata with Global Constraints. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, pages 263-272. IEEE Computer Society, 2010. Google Scholar
  3. Orna Bernholtz, Moshe Y. Vardi, and Pierre Wolper. An Automata-Theoretic Approach to Branching-Time Model Checking. In Proceedings of the 6th International Conference on Computer Aided Verification, CAV '94, volume 818 of Lecture Notes in Computer Science, pages 142-155. Springer, 1994. Google Scholar
  4. Bruno Bogaert and Sophie Tison. Equality and Disequality Constraints on Direct Subterms in Tree Automata. In Proceedings of STACS 92, 9th Annual Symposium on Theoretical Aspects of Computer Science, volume 577 of Lecture Notes in Computer Science, pages 161-171. Springer, 1992. Google Scholar
  5. Arnaud Carayol, Christof Löding, and Olivier Serre. Automata on Infinite Trees with Equality and Disequality Constraints Between Siblings. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 227-236, 2016. URL: http://dx.doi.org/10.1145/2933575.2934504.
  6. Luca Cardelli and Giorgio Ghelli. TQL: a query language for semistructured data based on the ambient logic. Mathematical Structures in Computer Science, 14(3):285-327, 2004. URL: http://dx.doi.org/10.1017/S0960129504004141.
  7. Emmanuel Filiot, Jean-Marc Talbot, and Sophie Tison. Satisfiability of a Spatial Logic with Tree Variables. In Proceedings of Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, volume 4646 of Lecture Notes in Computer Science, pages 130-145. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-74915-8_13.
  8. Emmanuel Filiot, Jean-Marc Talbot, and Sophie Tison. Tree Automata with Global Constraints. In Proceedings of Developments in Language Theory, 12th International Conference, DLT 2008, volume 5257 of Lecture Notes in Computer Science, pages 314-326. Springer, 2008. URL: http://dx.doi.org/10.1007/978-3-540-85780-8_25.
  9. Emmanuel Filiot, Jean-Marc Talbot, and Sophie Tison. Tree Automata with Global Constraints. Int. J. Found. Comput. Sci., 21(4):571-596, 2010. URL: http://dx.doi.org/10.1142/S012905411000743X.
  10. Florent Jacquemard, Francis Klay, and Camille Vacher. Rigid tree automata and applications. Inf. Comput., 209(3):486-512, 2011. URL: http://dx.doi.org/10.1016/j.ic.2010.11.015.
  11. Barbara Jobstmann and Roderick Bloem. Optimizations for LTL Synthesis. In Formal Methods in Computer-Aided Design, 6th International Conference, FMCAD 2006, pages 117-124. IEEE Computer Society, 2006. Google Scholar
  12. Michael Kaminski and Tony Tan. Tree Automata over Infinite Alphabets. In Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, volume 4800 of Lecture Notes in Computer Science, pages 386-423. Springer, 2008. Google Scholar
  13. Felix Klaedtke and Harald Rueß. Monadic Second-Order Logics with Cardinalities. In Automata, Languages and Programming, 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30 - July 4, 2003. Proceedings, volume 2719 of Lecture Notes in Computer Science, pages 681-696. Springer, 2003. Google Scholar
  14. Orna Kupferman and Moshe Y. Vardi. Safraless Decision Procedures. In 46th Annual IEEE Symposium on Foundations of Computer Science, FOCS'05, Proceedings, pages 531-542. IEEE Computer Society, 2005. Google Scholar
  15. Patrick Landwehr and Christof Löding. Projection for Büchi Tree Automata with Constraints Between Siblings. In Developments in Language Theory, DLT 2018, volume 11088 of Lecture Notes in Computer Science, pages 478-490. Springer, 2018. URL: http://dx.doi.org/10.1007/978-3-319-98654-8.
  16. Frank Nießner and Ulrich Ultes-Nitsche. A complete characterization of deterministic regular liveness properties. Theor. Comput. Sci., 387(2):187-195, 2007. URL: http://dx.doi.org/10.1016/j.tcs.2007.07.038.
  17. Amir Pnueli and Roni Rosner. On the Synthesis of a Reactive Module. In Proceedings of the Symposium on Principles of Programming Languages, POPL'89, pages 179-190, 1989. Google Scholar
  18. Michael O. Rabin. Decidability of Second-Order Theories and Automata on Infinite Trees. Transactions of the American Mathematical Society, 141:1-35, 1969. Google Scholar
  19. Michael O. Rabin. Automata on Infinite Objects and Church’s Problem. American Mathematical Society, Boston, MA, USA, 1972. Google Scholar
  20. Helmut Seidl, Thomas Schwentick, and Anca Muscholl. Numerical document queries. In Proceedings of the Twenty-Second ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 9-12, 2003, San Diego, CA, USA, pages 155-166. ACM, 2003. Google Scholar
  21. James W. Thatcher and Jesse B. Wright. Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical Systems Theory, 2(1):57-81, 1968. Google Scholar
  22. Wolfgang Thomas. Automata on Infinite Objects. In Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 133-192. Elsevier Science Publishers, Amsterdam, 1990. Google Scholar
  23. Wolfgang Thomas. Languages, Automata, and Logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Language Theory, volume III, pages 389-455. Springer, 1997. Google Scholar
  24. Moshe Y. Vardi and Thomas Wilke. Automata: from logics to algorithms. In Logic and automata - history and perspectives, volume 2 of Texts in Logic and Games, pages 629-724. Amsterdam University Press, 2007. Google Scholar
  25. Margus Veanes and Nikolaj Bjørner. Symbolic tree automata. Inf. Process. Lett., 115(3):418-424, 2015. URL: http://dx.doi.org/10.1016/j.ipl.2014.11.005.
  26. Wieslaw Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 200(1-2):135-183, 1998. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact