TY - GEN
T1 - Languages of nested trees
AU - Alur, Rajeev
AU - Chaudhuri, Swarat
AU - Madhusudan, P.
PY - 2006
Y1 - 2006
N2 - 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-μ, 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-μ.
AB - 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-μ, 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-μ.
UR - http://www.scopus.com/inward/record.url?scp=33749865109&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33749865109&partnerID=8YFLogxK
U2 - 10.1007/11817963_31
DO - 10.1007/11817963_31
M3 - Conference contribution
AN - SCOPUS:33749865109
SN - 354037406X
SN - 9783540374060
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 329
EP - 342
BT - Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings
PB - Springer
T2 - 18th International Conference on Computer Aided Verification, CAV 2006
Y2 - 17 August 2006 through 20 August 2006
ER -