Abstract
We study languages of nested trees—structures obtained by augmenting trees with sets of nested jump-edges. These graphs can naturally model branching behaviors of pushdown programs, so that the problem of branching-time software model checking may be phrased as a membership question for such languages. We define finite-state automata accepting such languages—these automata can pass states along jump-edges as well as tree edges. We find that the model-checking problem for these automata on pushdown systems is EXPTIME-complete, and that their alternating versions are expressively equivalent to NT-μ, a recently proposed temporal logic for nested trees that can express a variety of branching-time, “context-free” requirements. We also show that monadic second order logic (MSO) cannot exploit the structure: MSO on nested trees is too strong in the sense that it has an undecidable model checking problem, and seems too weak to capture NT-μ.
This research was partially supported by ARO URI award DAAD19-01-1-0473 and NSF award CCR-0306382.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Chaudhuri, S., Madhusudan, P.: A fixpoint calculus for local and global program flows. In: Proc. of POPL 2006, pp. 153–165 (2006)
Alur, R., Chaudhuri, S., Madhusudan, P.: Languages of nested trees. University of Pennsylvania Technical Report MS-CIS-06-10 (2006)
Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proc. of STOC 2004, pp. 202–211 (2004)
Alur, R., Madhusudan, P.: Adding nesting structure to words. In: H. Ibarra, O., Dang, Z. (eds.) DLT 2006. LNCS, vol. 4036, pp. 1–13. Springer, Heidelberg (2006)
Ball, T., Rajamani, S.: The SLAM project: debugging system software via static analysis. In: Proc. of POPL 2002, pp. 1–3 (2002)
Burkart, O., Steffen, B.: Model checking the full modal mu-calculus for infinite sequential processes. Theoretical Computer Science 221, 251–270 (1999)
Caucal, D.: On infinite transition graphs having a decidable monadic theory. Theor. Comput. Sci. 290(1), 79–115 (2003)
Comon, H., Dauchet, M., Gilleron, R., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications. Draft (2003)
Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus, and determinacy. In: Proc. of FOCS 1991, pp. 368–377 (1991)
Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)
Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 526–538. Springer, Heidelberg (2002)
Hopcroft, J.E., Ullman, J.D.: Introduction to automata theory, languages, and computation. Addison-Wesley, Reading (1979)
Janin, D., Walukiewicz, I.: On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 263–277. Springer, Heidelberg (1996)
Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science 27, 333–354 (1983)
Kupferman, O., Piterman, N., Vardi, M.Y.: Pushdown specifications. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol. 2514, pp. 262–277. Springer, Heidelberg (2002)
Löding, C.: Private communication
Löding, C., Madhusudan, P., Serre, O.: Visibly pushdown games. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 408–420. Springer, Heidelberg (2004)
McMillan, K.L.: Symbolic model checking: an approach to the state explosion problem. Kluwer Academic Publishers, Dordrecht (1993)
Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. Theor. Comput. Sci. 54(2-3), 267–276 (1987)
Muller, D.E., Schupp, P.E.: The theory of ends, pushdown automata, and second-order logic. Theoretical Computer Science 37, 51–75 (1985)
Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Transactions of the AMS 141, 1–35 (1969)
Reps, T., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: Proc. of POPL 1995, pp. 49–61 (1995)
Walukiewicz, I.: Pushdown processes: Games and model-checking. Information and Computation 164(2), 234–263 (2001)
Walukiewicz, I.: Monadic second-order logic on tree-like structures. Theor. Comput. Sci. 275(1-2), 311–346 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alur, R., Chaudhuri, S., Madhusudan, P. (2006). Languages of Nested Trees. In: Ball, T., Jones, R.B. (eds) Computer Aided Verification. CAV 2006. Lecture Notes in Computer Science, vol 4144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817963_31
Download citation
DOI: https://doi.org/10.1007/11817963_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37406-0
Online ISBN: 978-3-540-37411-4
eBook Packages: Computer ScienceComputer Science (R0)