Languages of Nested Trees

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 jumpedges 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-

• Type: Conference
• Year: 2006
• Where: CAV
• Authors: Rajeev Alur, Swarat Chaudhuri, P. Madhusudan
• Keywords: CAV 2006, Hardware, Model Checking, Nested, Nested Trees