Languages of nested trees

Rajeev Alur; Swarat Chaudhuri; P. Madhusudan

doi:10.1007/11817963_31

Languages of nested trees

Rajeev Alur, Swarat Chaudhuri, P. Madhusudan

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 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-μ.

Original language	English (US)
Title of host publication	Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings
Publisher	Springer
Pages	329-342
Number of pages	14
ISBN (Print)	354037406X, 9783540374060
DOIs	https://doi.org/10.1007/11817963_31
State	Published - 2006
Event	18th International Conference on Computer Aided Verification, CAV 2006 - Seattle, WA, United States Duration: Aug 17 2006 → Aug 20 2006

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	4144 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	18th International Conference on Computer Aided Verification, CAV 2006
Country	United States
City	Seattle, WA
Period	8/17/06 → 8/20/06

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/11817963_31

Fingerprint Dive into the research topics of 'Languages of nested trees'. Together they form a unique fingerprint.

Cite this

Alur, R., Chaudhuri, S., & Madhusudan, P. (2006). Languages of nested trees. In Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings (pp. 329-342). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4144 LNCS). Springer. https://doi.org/10.1007/11817963_31

Languages of nested trees. / Alur, Rajeev; Chaudhuri, Swarat; Madhusudan, P.

Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings. Springer, 2006. p. 329-342 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4144 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Alur, R, Chaudhuri, S & Madhusudan, P 2006, Languages of nested trees. in Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4144 LNCS, Springer, pp. 329-342, 18th International Conference on Computer Aided Verification, CAV 2006, Seattle, WA, United States, 8/17/06. https://doi.org/10.1007/11817963_31

@inproceedings{e06fd5a11eb843299a0df81d14425366,

title = "Languages of nested trees",

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 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-μ.",

author = "Rajeev Alur and Swarat Chaudhuri and P. Madhusudan",

year = "2006",

doi = "10.1007/11817963_31",

language = "English (US)",

isbn = "354037406X",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "329--342",

booktitle = "Computer Aided Verification - 18th International Conference, CAV 2006, Proceedings",

address = "Germany",

}

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 -

Languages of nested trees

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Cite this