Abstract
We show that the problem of checking if an infinite tree generated by a higher-order grammar of level 2 (hyperalgebraic) satisfies a given μ-calculus formula (or, equivalently, if it is accepted by an alternating parity automaton) is decidable, actually 2-Exptime-complete. Consequently, the monadic second-order theory of any hyperalgebraic tree is decidable, so that the safety restriction can be removed from our previous decidability result. The last result has been independently obtained by Aehlig, de Miranda and Ong. Our proof goes via a characterization of possibly unsafe second-order grammars by a new variant of higher-order pushdown automata, which we call panic automata. In addition to the standard pop 1 and pop 2 operations, these automata have an option of a destructive move called panic. The model-checking problem is then reduced to the problem of deciding the winner in a parity game over a suitable 2nd order pushdown system.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Aehlig, K., de Miranda, J.G., Ong, 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)
Aehlig, K., de Miranda, J.G., Ong, L.: The monadic second order theory of trees given by arbitrary level-two recursion schemes is decidable. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 39–54. Springer, Heidelberg (2005)
Cachat, T.: Higher Order Pushdown Automata, the Caucal Hierarchy of Graphs and Parity Games. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 556–569. Springer, Heidelberg (2003)
Cachat, T., Walukiewicz, I.: The complexity of games on higher order pushdown automata, (2004) (manuscript)
Caucal, D.: On infinite terms having a decidable monadic second-order theory. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 165–176. Springer, Heidelberg (2002)
Courcelle, B.: The monadic second-order theory of graphs IX: Machines and their behaviours. Theoretical Comput. Sci. 151, 125–162 (1995)
Courcelle, B., Knapik, T.: The evaluation of if first-order substitution is monadic second-order compatible. Theoretical Comput. Sci. 281(1-2), 177–206 (2002)
Damm, W.: The IO- and OI-hierarchies. Theoretical Comput. Sci. 20(2), 195–208 (1982)
Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Proceedings 32th Annual IEEE Symp. on Foundations of Comput. Sci., pp. 368–377. IEEE Computer Society Press, Los Alamitos (1991)
Engelfriet, J.: Iterated push-down automata and complexity classes. In: Proc. 15th STOC, pp. 365–373 (1983)
Engelfriet, J., Schmidt, E.M.: IO and OI. J. Comput. System Sci. 15(3), 328–353 (1977); 16(1), 67–99 (1978)
Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. A Guide to Current Research. LNCS, vol. 1500. Springer, Heidelberg (2002)
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 and panic automata, draft, http://www.mimuw.edu.pl/~niwinski/prace.html
Maslov, A.N.: The hierarchy of indexed languages of an arbitrary level. Soviet Math. Dokl. 15, 1170–1174 (1974)
Mostowski, A.W.: Games with forbidden positions. Technical Report 78, Instytut Matematyki, University of Gdansk (1991)
Niwiński, D.: Fixed points characterization of infinite behaviour of finite state systems. Theoret. Comput. Sci. 189, 1–69 (1997)
Thomas, W.: Languages, automata, and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol. 3, pp. 389–455. Springer, Heidelberg (1997)
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
Knapik, T., Niwiński, D., Urzyczyn, P., Walukiewicz, I. (2005). Unsafe Grammars and Panic Automata. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds) Automata, Languages and Programming. ICALP 2005. Lecture Notes in Computer Science, vol 3580. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11523468_117
Download citation
DOI: https://doi.org/10.1007/11523468_117
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27580-0
Online ISBN: 978-3-540-31691-6
eBook Packages: Computer ScienceComputer Science (R0)