弱之威力

形式化验证逻辑研究中的一个标志性成果是 Janin 与 Walukiewicz 的定理，该定理指出模态 $\mu$-演算（$\mu\mathrm{ML}$）在带标转移系统（简称 LTS）类上关于双模拟等价于标准一元二阶逻辑（此处缩写为 $\mathrm{smso}$）。我们的工作证明了同类中的两个结果，一个关于 $\mu\mathrm{ML}$ 的无交错片段（$\mu_D\mathrm{ML}$），另一个关于弱 $\mathrm{mso}$（$\mathrm{wmso}$）。尽管已知 $\mu_D\mathrm{ML}$ 与 $\mathrm{wmso}$ 在二叉树上关于双模拟等价，我们的分析表明一旦在任意 LTS 上进行推理，图景便发生根本改变。我们证明的第一个定理是：在 LTS 上，$\mu_D\mathrm{ML}$ 关于双模拟等价于 noetherian $\mathrm{mso}$（$\mathrm{nmso}$）——一种新引入的 $\mathrm{smso}$ 变体，其中二阶量化仅作用于“良基”子集。我们的第二个定理从 $\mathrm{wmso}$ 出发，证明其关于双模拟等价于由连续性概念定义的 $\mu_D\mathrm{ML}$ 片段。类似于 Janin 与 Walukiewicz 的结果，我们的证明本质上基于自动机理论：作为另一贡献，我们引入了刻画 $\mathrm{wmso}$ 与 $\mathrm{nmso}$（在树模型上）以及 $\mu_C\mathrm{ML}$ 与 $\mu_D\mathrm{ML}$（对所有转移系统）表达能力的奇偶自动机类。