Abstract
A tree automaton can simulate the successful runs of a word or tree automaton working on the word or tree denoted by a level-2 lambda-tree. In particular the monadic second order theory of trees given by arbitrary, rather than only by safe, recursion schemes of level 2 is decidable. This solves the level-2 case of an open problem by Knapik, Niwiński and Urzyczyn.
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
Preview
Unable to display preview. Download preview PDF.
References
Aehlig, K., de Miranda, J.G., Ong, C.-H.L.: Safety is not a restriction at level 2 for string languages. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 490–504. Springer, Heidelberg (2005) (To appear)
Asperti, A., Danos, V., Laneve, C., Regnier, L.: Paths in the lambda-calculus. In: Proceedings of the Ninth Annual IEEE Symposium an Logic in Computer Science (LICS 1994), July 1994, pp. 426–436 (1994)
Caucal, D.: On infinite transition graphs having a decidable monadic theory. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 194–205. Springer, Heidelberg (1996)
Courcelle, B.: The monadic second-order logic of graphs IX: Machines and their behaviours. Theoretical Comput. Sci. 151(1), 125–162 (1995)
Kennaway, J.R., Klop, J.W., Sleep, M.R., de Vries, F.J.: Infinitary lambda calculus. Theoretical Comput. Sci. 175(1), 93–125 (1997)
Knapik, T., Niwiński, D., Urzyczyn, P.: Deciding monadic theories of hyperalgebraic trees. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 253–267. Springer, Heidelberg (2001)
Knapik, T., Niwiński, D., Urzyczyn, P.: Higher-order pushdown trees are easy. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 205–222. Springer, Heidelberg (2002)
Knapik, T., Niwiński, D., Urzyczyn, P., Walukiewicz, I.: Unsafe grammars, panic automata, and decidability. In: Manuscript (October 2004)
Kupferman, O., Vardi, M.Y.: An automata-theoretic approach to reasoning about infinite-state systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 36–52. Springer, Heidelberg (2000)
Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. Theoretical Comput. Sci. 54, 267–276 (1987)
Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society 141, 1–35 (1969)
Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 628–641. Springer, Heidelberg (1998)
Walukiewicz, I.: Pushdown processes: Games and model-checking. Information and Computation 164(2), 234–263 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aehlig, K., de Miranda, J.G., Ong, C.H.L. (2005). The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable. In: Urzyczyn, P. (eds) Typed Lambda Calculi and Applications. TLCA 2005. Lecture Notes in Computer Science, vol 3461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11417170_5
Download citation
DOI: https://doi.org/10.1007/11417170_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25593-2
Online ISBN: 978-3-540-32014-2
eBook Packages: Computer ScienceComputer Science (R0)