Automata on Infinite Trees with Equality and Disequality Constraints Between Siblings

ABSTRACT

This article is inspired by two works from the early 90s. The first one is by Bogaert and Tison who considered a model of automata on finite ranked trees where one can check equality and disequality constraints between direct subtrees: they proved that this class of automata is closed under Boolean operations and that both the emptiness and the finiteness problem of the accepted language are decidable. The second one is by Niwinski who showed that one can compute the cardinality of any ω-regular language of infinite trees.

Here, we generalise the model of automata of Tison and Bogaert to the setting of infinite binary trees. Roughly speaking we consider parity tree automata where some transitions are guarded and can be used only when the two direct sub-trees of the current node are equal/disequal. We show that the resulting class of languages encompasses the one of ω-regular languages of infinite trees while sharing most of its closure properties, in particular it is a Boolean algebra. Our main technical contribution is then to prove that it also enjoys a decidable cardinality problem. In particular, this implies the decidability of the emptiness problem.

References

1. L. Barguñó, C. Creus, G. Godoy, F. Jacquemard, and C. 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.
2. B. Bogaert and S. Tison. Equality and disequality constraints on direct subterms in tree automata. In Proceedings of the 19th Symposium on Theoretical Aspects of Computer Science (STACS 2002), volume 577 of Lecture Notes in Computer Science, pages 161--171. Springer-Verlag, 1992.
3. B. Bogaert, F. Seynhaeve, and S. Tison. The recognizability problem for tree automata with comparisons between brothers. In FoSSaCS'99, Proceedings, volume 1578 of LNCS. Springer, 1999.
4. M. Bojańczyk. A bounding quantifier. In Proceedings of Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, volume 3210 of LNCS, pages 41--55. Springer, 2004.
5. M. Bojańczyk. Weak MSO with the unbounding quantifier. Theory of Computing Systems, 48(3):554--576, 2011. ISSN 1432-4350.
6. M. Bojanczyk. Weak MSO+U with path quantifiers over infinite trees. In Proceedings of Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, volume 8573 of LNCS, pages 38--49. Springer Berlin Heidelberg, 2014.
7. L. Cardelli and G. Ghelli. TQL: a query language for semistructured data based on the ambient logic. Mathematical Structures in Computer Science, 14(3):285--327, 2004.
8. T. Colcombet and C. Löding. The non-deterministic mostowski hierarchy and distance-parity automata. In Proceedings of the 35th International Colloquium on Automata, Languages, and Programming (ICALP 2008), volume 5126 of Lecture Notes in Computer Science, pages 398--409. Springer-Verlag, 2008.
9. T. Colcombet, D. Kuperberg, C. Löding, and M. Vanden Boom. Deciding the weak definability of büchi definable tree languages. In "Proceedings of Computer Science Logic, 27th Annual Conference of the EACSL (CSL 2013)", volume 23 of LIPIcs, pages 215--230. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013.
10. H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. http://tata.gforge.inria.fr/, 2007. release October, 12th 2007.
11. E. Filiot, J. Talbot, and S. 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 LNCS, pages 130--145. Springer, 2007.
12. E. Filiot, J. Talbot, and S. Tison. Tree automata with global constraints. In Proceedings of Developments in Language Theory, 12th International Conference, DLT 2008, volume 5257 of LNCS, pages 314--326. Springer, 2008.
13. E. Filiot, J. Talbot, and S. Tison. Tree automata with global constraints. Int. J. Found. Comput. Sci., 21(4):571--596, 2010.
14. G. Godoy and O. Giménez. The HOM problem is decidable. Journal of the Association for Computing Machinery (ACM), 60(4):23, 2013.
15. G. Godoy, O. Giménez, L. Ramos, and C. Àlvarez. The HOM problem is decidable. In Proceedings of the 42nd ACM Symposium on Theory of Computing, STOC 2010, pages 485--494. ACM, 2010.
16. D. E. Muller and P. E. Schupp. Simulating alternating tree automata by nondeterministic automata. Theoretical Computer Science, 141(1&2): 69--107, 1995.
17. D. Niwinski. On the cardinality of sets of infinite trees recognizable by finite automata. In Proceedings of the 16th Symposium, Mathematical Foundations of Computer Science (MFCS 1991), volume 520 of Lecture Notes in Computer Science, pages 367--376. Springer-Verlag, 1991.
18. R. Paige and R. E. Tarjan. Three partition refinement algorithms. SIAM J. Comput., 16(6):973--989, 1987.
19. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proceedings of the Symposium on Principles of Programming Languages, POPL'89, pages 179--190, 1989.
20. M. O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141: 1--35, 1969.
21. M. O. Rabin. Automata on infinite objects and Church's problem. American Mathematical Society, Providence, R.I., 1972. Conference Board of the Mathematical Sciences Regional Conference Series in Mathematics, No. 13.
22. W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Language Theory, volume III, pages 389--455. Springer-Verlag, 1997.
23. M. Vanden Boom. Weak cost monadic logic over infinite trees. In Proceedings of Mathematical Foundations of Computer Science 2011 - 36th International Symposium, MFCS 2011, pages 580--591, 2011.
24. W. Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 200 (1-2):135--183, 1998.

• Theory of computation