The Nesting-Depth of Disjunctive µ-Calculus for Tree Languages and the Limitedness Problem
The Nesting-Depth of Disjunctive µ-Calculus for Tree Languages and the Limitedness Problem
复制标题
树语言析取μ微积分的嵌套深度和有限性问题
DOI：
10.1007/978-3-540-87531-4_30
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Christof Löding
中科院分区：
文献类型：
--
作者：
Thomas Colcombet;Christof Löding
本文将Hashiguchi关于词的限制星高问题的可判定性的结果提升到有限树的层次上。形式上，我们证明了它是可判定的，给定一个正则树语言和一个自然数，L是否可以用一个析取μ-演算公式描述，其中至多有一个不动点。对于允许替换的析取μ-公式，我们也得到了同样的结果.后一个结果是等价于决定如果语言是可定义的一个正则表达式与嵌套深度在mostkof Kleene-stars.The证明，以下的方法Kirsten在字的情况下，去减少的可判定性的有限性问题的非确定性嵌套距离沙漠自动机在树上。我们解决这个问题的更一般的框架交替树自动机。
In this paper we lift the result of Hashiguchi of decidability of the restricted star-height problem for words to the level of finite trees. Formally, we show that it is decidable, given a regular tree languageLand a natural numberkwhetherLcan be described by a disjunctiveμ-calculus formula with at mostknesting of fixpoints. We show the same result for disjunctiveμ-formulas allowing substitution. The latter result is equivalent to deciding if the language is definable by a regular expression with nesting depth at mostkof Kleene-stars.The proof, following the approach of Kirsten in the word case, goes by reduction to the decidability of the limitedness problem for non-deterministic nested distance desert automata over trees. We solve this problem in the more general framework of alternating tree automata.