增广Mu演算的复杂性
The Complexity of Enriched Mu-Calculi
摘要：
完全丰富演算是命题演算的逆程序、分次模态和名值的推广.虽然满足性在几个表达片段的充分丰富的演算被称为是可判定的和ExpTime完全的，它最近被证明，完整的演算是不可判定的。在本文中，我们研究的片段的充分丰富的演算，通过删除至少一个额外的结构。我们表明，在以这种方式获得的所有片段中，可满足性是可判定的和ExpTime完全的。因此，我们确定了一个家庭的可判定的逻辑是最大的（和无与伦比的）的表达能力。我们的结果是通过引入两个新的自动机模型，表明他们的空性问题是ExpTime-完全的，然后减少这些问题的相关逻辑的可满足性。我们介绍的自动机模型是双向分级交替奇偶自动机在无限树（2GAPTs）和完全丰富的自动机在无限森林（FEAs）。前者是文献中两个不可比自动机模型的常见推广。后者扩展交替自动机以类似的方式完全丰富的演算扩展标准演算。
英文摘要：
The fully enriched μ-calculus is the extension of the propositional μ-calculus with inverse programs, graded modalities, and nominals. While satisfiability in several expressive fragments of the fully enriched μ-calculus is known to be decidable and ExpTime-complete, it has recently been proved that the full calculus is undecidable. In this paper, we study the fragments of the fully enriched μ-calculus that are obtained by dropping at least one of the additional constructs. We show that, in all fragments obtained in this way, satisfiability is decidable and ExpTime-complete. Thus, we identify a family of decidable logics that are maximal (and incomparable) in expressive power. Our results are obtained by introducing two new automata models, showing that their emptiness problems are ExpTime-complete, and then reducing satisfiability in the relevant logics to these problems. The automata models we introduce are two-way graded alternating parity automata over infinite trees (2GAPTs) and fully enriched automata (FEAs) over infinite forests. The former are a common generalization of two incomparable automata models from the literature. The latter extend alternating automata in a similar way as the fully enriched μ-calculus extends the standard μ-calculus.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
