论文标题
大小在模态$μ$ -calculus中很重要
Size matters in the modal $μ$-calculus
论文作者
论文摘要
我们讨论并比较模态$ $ $ calculus的复杂度度量，重点是尺寸和交替深度。作为码数，我们采用Wilke的交替树自动机，我们将其称为文本中的奇偶校验公式。在Bruse，Friedmann＆Lange的工作基础上，我们比较了$ $ $ $ calculus公式的两种尺寸度量：subformula-size，即。 ，给定公式的子形成和闭合大小。这些概念对应于公式作为平价公式的表示，分别基于其subformula dag和其闭合图。区别于我们的方法的是，我们明确说明α等效性的作用，因为天真地重命名的绑定变量可以导致指数爆炸。此外，我们将公式的交替深度与奇偶公式的索引匹配。我们从没有α等效的设置开始。我们定义了Subformula尺寸和闭合大小，并回想起可以将$μ$ calculus公式转换为尺寸线性WRT subformula尺寸的奇偶校验公式，并提供一种将$μ$ $ calculus公式转化为等效的奇偶校验公式linear linear linear linear lint lint lint lint lint lint lint lint lint lint lint size。相反，有一个标准转换产生指数subformula的$ $ $ calculus公式 - 但根据原始奇偶校验公式的大小，线性闭合大小。我们确定了所谓的无偏见的平价公式，在该公式中存在subformula大小中的转换线性。然后，我们引入大小的概念，这些概念在alpha等效上完全不变。我们转移了Bruse et alii的结果，表明在我们的设置闭合大小中，大小可能小于subformula尺寸。我们还展示了如何重命名绑定变量，以使alpha-querivalence在闭合集合上变为句法身份。最后，我们回顾了受保护的转型的复杂性。
We discuss and compare complexity measures for the modal $μ$-calculus, focusing on size and alternation depth. As a yardstick we take Wilke's alternating tree automata, which we shall call parity formulas in the text. Building on work by Bruse, Friedmann & Lange, we compare two size measures for $μ$-calculus formulas: subformula-size,i.e. , the number of subformulas of the given formula, and closure-size. These notions correspond to the representation of a formula as a parity formula based on, respectively, its subformula dag, and its closure graph. What distinguishes our approach is that we are explicit about the role of alpha-equivalence, as naively renaming bound variables can lead to an exponential blow-up. In addition, we match the formula's alternation depth with the index of the parity formula. We start in a setting without alpha-equivalence. We define subformula-size and closure-size and recall that a $μ$-calculus formula can be transformed into a parity formula of size linear wrt subformula size, and give a construction that transforms a $μ$-calculus formula into an equivalent parity formula linear wrt closure-size. Conversely, there is a standard transformation producing a $μ$-calculus formula of exponential subformula -- but linear closure-size in terms of the size of the original parity formula. We identify so-called untwisted parity formulas for which a transformation linear in subformula-size exists. We then introduce size notions that are completely invariant under alpha equivalence. We transfer the result of Bruse et alii, showing that also in our setting closure-size can be exponentially smaller than subformula-size. We also show how to rename bound variables so that alpha-equivalence becomes syntactic identity on the closure set. Finally, we review the complexity of guarded transformations.
