Languages of nested trees

Rajeev Alur, Swarat Chaudhuri, P. Madhusudan

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish (US)
Title of host publicationComputer Aided Verification - 18th International Conference, CAV 2006, Proceedings
PublisherSpringer
Pages329-342
Number of pages14
ISBN (Print)354037406X, 9783540374060
DOIs
StatePublished - 2006
Event18th International Conference on Computer Aided Verification, CAV 2006 - Seattle, WA, United States
Duration: Aug 17 2006Aug 20 2006

Publication series

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

Other

Other18th International Conference on Computer Aided Verification, CAV 2006
CountryUnited States
CitySeattle, WA
Period8/17/068/20/06

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

Cite this