Document Open Access Logo

Deterministic and Game Separability for Regular Languages of Infinite Trees

Authors Lorenzo Clemente , Michał Skrzypczak

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2021.126.pdf
  • Filesize: 0.77 MB
  • 15 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Tree languages
Keywords
  • separation
  • infinite trees
  • regular languages
  • deterministic automata
  • game automata

Metrics

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

Abstract

We show that it is decidable whether two regular languages of infinite trees are separable by a deterministic language, resp., a game language. We consider two variants of separability, depending on whether the set of priorities of the separator is fixed, or not. In each case, we show that separability can be decided in EXPTIME, and that separating automata of exponential size suffice. We obtain our results by reducing to infinite duration games with ω-regular winning conditions and applying the finite-memory determinacy theorem of Büchi and Landweber.

Cite As Get BibTex

Lorenzo Clemente and Michał Skrzypczak. Deterministic and Game Separability for Regular Languages of Infinite Trees. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 126:1-126:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ICALP.2021.126

Author Details

Lorenzo Clemente
  • University of Warsaw, Poland
Michał Skrzypczak
  • University of Warsaw, Poland

Funding

  • Clemente, Lorenzo: Partially supported by the Polish NCN grant 2017/26/D/ST6/00201.
  • Skrzypczak, Michał: Partially supported by the Polish NCN grant 2017/26/D/ST6/00201.

References

  1. David Barozzini, Lorenzo Clemente, Thomas Colcombet, and Paweł Parys. Cost Automata, Safe Schemes, and Downward Closures. In Proc. of ICALP'20, LIPIcs, pages 109:1-109:18, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.109.
  2. Achim Blumensath. Recognisability for algebras of infinite trees. Theoretical Computer Science, 412(29):3463-3486, 2011. Google Scholar
  3. Mikołaj Bojańczyk. Star height via games. In LICS, pages 214-219, 2015. Google Scholar
  4. Mikołaj Bojańczyk, Filippo Cavallari, Thomas Place, and Michał Skrzypczak. Regular tree languages in low levels of the Wadge Hierarchy. Log. Meth. Comput. Sci., Volume 15, Issue 3, 2019. URL: https://lmcs.episciences.org/5743.
  5. Mikołaj Bojańczyk and Wojciech Czerwiński. An automata toolbox, February 2018. URL: https://www.mimuw.edu.pl/~bojan/paper/automata-toolbox-book.
  6. Mikołaj Bojańczyk and Thomas Place. Regular languages of infinite trees that are boolean combinations of open sets. In Proc. of ICALP'12, ICALP'12, pages 104 - -115, Berlin, Heidelberg, 2012. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-31585-5_13.
  7. J. Richard Büchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295-311, 1969. URL: http://www.jstor.org/stable/1994916.
  8. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In Proc. of STOC'17, 2017. Google Scholar
  9. Filippo Cavallari, Henryk Michalewski, and Michał Skrzypczak. A characterisation of Π⁰₂ regular tree languages. In Proc. of MFCS'17, 2017. Google Scholar
  10. Lorenzo Clemente, Wojciech Czerwiński, Sławomir Lasota, and Charles Paperman. Regular separability of parikh automata. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, Proc. of ICALP'17, volume 80, pages 117:1-117:13, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.117.
  11. Lorenzo Clemente, Wojciech Czerwiński, Sławomir Lasota, and Charles Paperman. Separability of Reachability Sets of Vector Addition Systems. In Proc. of STACS'17, volume 66 of LIPICs, pages 24:1-24:14, 2017. URL: https://doi.org/10.4230/LIPIcs.STACS.2017.24.
  12. Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski. Determinisability of One-Clock Timed Automata. In Proc. of CONCUR'20, volume 171 of LIPIcs, pages 42:1-42:17, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.42.
  13. Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski. Timed Games and Deterministic Separability. In Proc. of ICALP'20, volume 168 of LIPIcs, pages 121:1-121:16, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.121.
  14. Lorenzo Clemente, Paweł Parys, Sylvain Salvati, and Igor Walukiewicz. The diagonal problem for higher-order recursion schemes is decidable. In Proc. of LICS'16, 2016. URL: https://doi.org/10.1145/2933575.2934527.
  15. Lorenzo Clemente and Michał Skrzypczak. Deterministic and game separability for regular languages of infinite trees, May 2021. URL: http://arxiv.org/abs/2105.01137.
  16. Thomas Colcombet. Fonctions régulières de coût. Habilitation thesis, Université Paris Diderot - Paris 7, 2013. Google Scholar
  17. Thomas Colcombet, Denis Kuperberg, Christof Löding, and Michael Vanden Boom. Deciding the weak definability of Büchi definable tree languages. In Proc. of CSL'13, LIPIcs, pages 215-230, 2013. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.215.
  18. Thomas Colcombet and Christof Löding. The Non-deterministic Mostowski Hierarchy and Distance-Parity Automata. In Proc. of ICALP'08, pages 398-409, 2008. URL: https://doi.org/10.1007/978-3-540-70583-3_33.
  19. William Craig. Three uses of the herbrand-gentzen theorem in relating model theory and proof theory. The Journal of Symbolic Logic, 22(3):269-285, 1957. URL: http://www.jstor.org/stable/2963594.
  20. Wojciech Czerwiński, Laure Daviaud, Nathanaël Fijalkow, Marcin Jurdziński, Ranko Lazić, and Paweł Parys. Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games. In Proc. of SODA'19, pages 2333-2349, USA, 2019. Society for Industrial and Applied Mathematics. Google Scholar
  21. Wojciech Czerwiński and Sławomir Lasota. Regular Separability of One Counter Automata. Logical Methods in Computer Science, Volume 15, Issue 2, June 2019. URL: https://lmcs.episciences.org/5563.
  22. Wojciech Czerwiński, Sławomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan. Regular Separability of Well-Structured Transition Systems. In Proc. of CONCUR'18, LIPIcs, pages 35:1-35:18, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.35.
  23. Wojciech Czerwiński, Wim Martens, Lorijn van Rooijen, and Marc Zeitoun. A note on decidable separability by piecewise testable languages. In Proc. of FCT'15, 2015. URL: https://doi.org/10.1007/978-3-319-22177-9_14.
  24. Wojciech Czerwiński and Georg Zetzsche. An approach to regular separability in vector addition systems. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 341-354. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394776.
  25. E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy. In Proc. of SFCS'91, pages 368-377. IEEE Computer Society, 1991. URL: https://doi.org/10.1109/SFCS.1991.185392.
  26. Alessandro Facchini, Filip Murlak, and Michał Skrzypczak. Index problems for game automata. ACM Trans. Comput. Logic, 17(4):24:1-24:38, November 2016. URL: https://doi.org/10.1145/2946800.
  27. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata Logics, and Infinite Games - A Guide to Current Research. Springer, 2002. Google Scholar
  28. Alexander Kechris. Classical Descriptive Set Theory. Springer-Verlag, 1995. Google Scholar
  29. Ralf Küsters and Thomas Wilke. Deciding the first level of the μ-calculus alternation hierarchy. In Proc. of FSTTCS'02, pages 241-252, Berlin, 2002. Google Scholar
  30. Robert McNaughton and Seymour Papert. Counter-free automata. M.I.T. Press research monographs. M.I.T. Press, 1971. Google Scholar
  31. Filip Murlak. Weak index versus Borel rank. In Proc. of STACS'08, volume 1 of LIPIcs, pages 573-584, 2008. URL: https://doi.org/10.4230/LIPIcs.STACS.2008.1318.
  32. Damian Niwiński. On fixed-point clones (extended abstract). In Proc. of ICALP'86, pages 464-473, 1986. URL: http://dl.acm.org/citation.cfm?id=646240.683678.
  33. Damian Niwiński and Igor Walukiewicz. Relating hierarchies of word and tree automata. In Proc. of STACS'98, pages 320-331, 1998. Google Scholar
  34. Damian Niwiński and Igor Walukiewicz. A gap property of deterministic tree languages. Theoretical Computer Science, 303(1):215-231, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00452-8.
  35. Damian Niwiński and Igor Walukiewicz. Deciding nondeterministic hierarchy of deterministic tree automata. Electronic Notes in Theoretical Computer Science, 123:195-208, 2005. Proceedings of the 11th Workshop on Logic, Language, Information and Computation (WoLLIC 2004). URL: https://doi.org/10.1016/j.entcs.2004.05.015.
  36. Thomas Place and Marc Zeitoun. Separating regular languages with first-order logic. Log. Methods Comput. Sci., 12(1), 2016. URL: https://doi.org/10.2168/LMCS-12(1:5)2016.
  37. Thomas Place and Marc Zeitoun. Adding successor: A transfer theorem for separation and covering. ACM Trans. Comput. Logic, 21(2), 2019. URL: https://doi.org/10.1145/3356339.
  38. Michael O. Rabin. Weakly definable relations and special automata. In Mathematical Logic and Foundations of Set Theory, volume 59 of Studies in Logic and the Foundations of Mathematics, pages 1-23. Elsevier, 1970. URL: https://doi.org/10.1016/S0049-237X(08)71929-3.
  39. Luigi Santocanale and André Arnold. Ambiguous classes in mu-calculi hierarchies. Theoretical Computer Science, 333(1):265-296, 2005. Foundations of Software Science and Computation Structures. URL: https://doi.org/10.1016/j.tcs.2004.10.024.
  40. Marcel Paul Schützenberger. On finite monoids having only trivial subgroups. Information and Control, 8(2):190-194, 1965. Google Scholar
  41. Michał Skrzypczak and Igor Walukiewicz. Deciding the Topological Complexity of Büchi Languages. In Proc. of ICALP'16, volume 55 of LIPIcs, pages 99:1-99:13, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.99.
  42. Tomasz Fryderyk Urbanski. On Deciding if Deterministic Rabin Language Is in Büchi Class. In Proc. of ICALP'00, volume 1853 of LNCS, pages 663-674. Springer, 2000. URL: https://doi.org/10.1007/3-540-45022-X_56.
  43. Klaus Wagner. On omega-regular sets. Information and Control, 43(2):123-177, 1979. URL: https://doi.org/10.1016/S0019-9958(79)90653-3.
  44. Igor Walukiewicz. Deciding low levels of tree-automata hierarchy. ENTCS, 67:61-75, 2002. URL: https://doi.org/10.1016/S1571-0661(04)80541-3.
  45. Georg Zetzsche. An approach to computing downward closures. In Proc. of ICALP'15, volume 9135 of LNCS, pages 440-451, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_35.
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