Abstract
We consider an extension of tree automata on infinite trees that can check equality and disequality constraints between direct subtrees of a node. Recently, it has been shown that the emptiness problem for these kind of automata with a parity acceptance condition is decidable and that the corresponding class of languages is closed under Boolean operations. In this paper, we show that the class of languages recognizable by such tree automata with a Büchi acceptance condition is closed under projection. This construction yields a new algorithm for the emptiness problem, implies that a regular tree is accepted if the language is non-empty (for the Büchi condition), and can be used to obtain a decision procedure for an extension of monadic second-order logic with predicates for subtree comparisons.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
A parity condition assigns priorities (natural numbers) to states and is satisfied in a state sequence if the maximal priority that appears infinitely often is even. A Büchi condition corresponds to a parity condition with priorities 1 and 2.
- 2.
The use of cylindrification is often not mentioned explicitly in translations from logic to automata because for standard automata it is a trivial operation.
References
Barguñó, L., Creus, C., Godoy, G., Jacquemard, F., Vacher, C.: The emptiness problem for tree automata with global constraints. In: LICS, pp. 263–272 (2010)
Bogaert, B.: Automates d’arbres avec test d’égalité. Ph.D. thesis, L’Universitédes Sciences et Techniques de Lille Flandres-Arto (1990)
Bogaert, B., Tison, S.: Equality and disequality constraints on direct subterms in tree automata. In: STACS, pp. 161–171 (1992)
Carayol, A., Löding, C., Serre, O.: Automata on infinite trees with equality and disequality constraints between siblings. In: LICS, pp. 227–236 (2016)
Comon, H., et al.: Tree Automata Techniques and Applications. http://tata.gforge.inria.fr/. Accessed 12 Oct 2007
Filiot, E., Talbot, J., Tison, S.: Tree automata with global constraints. Int. J. Found. Comput. Sci. 21(4), 571–596 (2010)
Godoy, G., Giménez, O.: The HOM problem is decidable. J. ACM 60(4), 23:1–23:44 (2013)
Godoy, G., Giménez, O., Ramos, L., Àlvarez, C.: The HOM problem is decidable. In: STOC, pp. 485–494 (2010)
Kaminski, M., Tan, T.: Tree automata over infinite alphabets. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 386–423. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78127-1_21
Klaedtke, F., Rueß, H.: Monadic second-order logics with cardinalities. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 681–696. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-45061-0_54
Klarlund, N., Møller, A.: MONA Version 1.4 User Manual. BRICS (2001). http://www.brics.dk/mona/. Revision of BRICS NS-98-3
Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: FOCS, pp. 531–542. IEEE Computer Society (2005)
Muller, D.E., Saoudi, A., Schupp, P.E.: Alternating automata, the weak monadic theory of the tree, and its complexity. In: Kott, L. (ed.) ICALP 1986. LNCS, vol. 226, pp. 275–283. Springer, Heidelberg (1986). https://doi.org/10.1007/3-540-16761-7_77
Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Am. Math. Soc. 141, 1–35 (1969)
Rabin, M.O.: Weakly definable relations and special automata. In: BarHillel, Y. (ed.) Mathematical Logic and Foundations of Set Theory, pp. 1–23 (1970)
Safra, S.: On the complexity of omega-automata. In: FOCS, pp. 319–327 (1988)
Seidl, H., Schwentick, T., Muscholl, A.: Numerical document queries. In: ACM SIGACT-SIGMOD-SIGART, pp. 155–166. ACM (2003)
Thatcher, J.W., Wright, J.B.: Generalized finite automata theory with an application to a decision problem of second-order logic. Math. Syst. Theory 2(1), 57–81 (1968)
Thomas, W.: Languages, automata, and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, pp. 389–455. Springer, Heidelberg (1997). https://doi.org/10.1007/978-3-642-59126-6_7
Veanes, M., Bjørner, N.: Symbolic tree automata. Inf. Process. Lett. 115(3), 418–424 (2015)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Landwehr, P., Löding, C. (2018). Projection for Büchi Tree Automata with Constraints Between Siblings. In: Hoshi, M., Seki, S. (eds) Developments in Language Theory. DLT 2018. Lecture Notes in Computer Science(), vol 11088. Springer, Cham. https://doi.org/10.1007/978-3-319-98654-8_39
Download citation
DOI: https://doi.org/10.1007/978-3-319-98654-8_39
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-98653-1
Online ISBN: 978-3-319-98654-8
eBook Packages: Computer ScienceComputer Science (R0)