论文标题
一项有关通过树自动机对$μ$ calculus进行满意度检查的调查
A Survey on Satisfiability Checking for the $μ$-Calculus through Tree Automata
论文作者
论文摘要
模型检查和满足算法的模态$ $ $ -CALCULUS首先将公式转换为交替的平等树自动机。因此，模型检查将减少为通过树自动机检查接受，并为检查其空虚而满意。第一个直接减少到平等游戏的解决方案，但第二个更为复杂。 我们通过减少解决某种结构，所谓的空虚游戏的平价游戏来审查对交替的树自动机进行的非空置检查。由于交替的树自动机的空虚问题是exptime complete，因此这些游戏的大小在输入自动机的状态数量中是指数的。我们展示了空虚游戏的构建如何结合（固定的）结构部分与（历史 - ）确定奇偶校词自动机。对于具有某些句法结构的树自动机，可以使用更简单的方法来处理Automata一词的处理，然后在一般情况下可能比一般情况小。 这些结果在满意度和有效性检查（各种片段）中有直接的后果。
Algorithms for model checking and satisfiability of the modal $μ$-calculus start by converting formulas to alternating parity tree automata. Thus, model checking is reduced to checking acceptance by tree automata and satisfiability to checking their emptiness. The first reduces directly to the solution of parity games but the second is more complicated. We review the non-emptiness checking of alternating tree automata by a reduction to solving parity games of a certain structure, so-called emptiness games. Since the emptiness problem for alternating tree automata is EXPTIME-complete, the size of these games is exponential in the number of states of the input automaton. We show how the construction of the emptiness games combines a (fixed) structural part with (history-)determinization of parity word automata. For tree automata with certain syntactic structures, simpler methods may be used to handle the treatment of the word automata, which then may be asymptotically smaller than in the general case. These results have direct consequences in satisfiability and validity checking for (various fragments of) the modal $μ$-calculus.
