Languages of Nested Trees
Languages of Nested Trees
复制标题
嵌套树的语言
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
P. Madhusudan
中科院分区：
文献类型：
--
作者：
R. Alur;Swarat Chaudhuri;P. Madhusudan
我们研究语言的嵌套树结构，通过增加树套嵌套跳边。这些图可以自然地对下推程序的分支行为进行建模，因此分支时软件模型检查的问题可以被描述为此类语言的成员资格问题。我们定义有限状态自动机接受这样的语言，这些自动机可以通过状态沿着跳边以及树的边缘。我们发现，这些自动机上推系统的模型检查问题是EXPTIME-完全的，他们的交替版本是表达等价于NT-μ，最近提出的嵌套树的时态逻辑，可以表达各种分支时间，“上下文无关”的要求。我们还表明，一元二阶逻辑（MSO）不能利用的结构：嵌套树上的MSO是太强的意义上，它有一个不可判定的模型检查问题，似乎太弱，捕捉NT-μ。
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-μ.