模态 μ-演算

形式陈述 ​

给定 Kripke 结构 $K=(S,R,L)$，模态 $\mu$-演算在布尔联结与 $⟨⟩,[]$ 模态之外加入 $\mu X.\phi$ 和 $\nu X.\phi$。环境把变量解释为 $S$ 的子集，模态解释为关系 $R$ 上的存在或全称前驱；绑定变量只在 $\phi$ 中正出现，使其诱导的幂集算子单调，再分别以最小和最大不动点解释 $\mu$ 与 $\nu$。下面把这四部分写成可直接计算的集合语义。

带不动点变量的模态语法 ​

模态 $\mu$-演算公式由原子命题、布尔联结、模态 $⟨⟩,[]$、变量 $X$ 以及

$$\mu X.\phi ,\nu X.\phi$$

构成。$\mu$ 取最小不动点，$\nu$ 取最大不动点。为保证语义单调，绑定变量 $X$ 在 $\phi$ 中必须只出现在正位置。

在Kripke 结构公理库Kripke 结构Kripke structure · Kripke transition structure以状态转移和原子命题标记解释分支时间性质的状态模型。 $K=(S,R,L)$ 上，环境 $\eta$ 把变量映射为状态集合。模态语义为

$$[[⟨⟩\phi ]]=Pre([[\phi ]]),$$$$[[[]\phi ]]=\{s:\mathrm{\forall }{s}^{\prime },sR{s}^{\prime }\Rightarrow s^{\prime }\in [[\phi ]]\}.$$

Tarski 保证语义存在 ​

对 $\mu X.\phi$，固定其他变量后得到幂集格上的算子

$$F_X(U)=[[\phi {]]}_{\eta [X\mapsto U]}.$$

正出现保证 $F_X$ 单调。Knaster–Tarski 定理公理库Knaster–Tarski 不动点定理Knaster-Tarski fixed-point theorem · Tarski fixed-point theorem完备格上的单调自映射之全部不动点构成完备格，并具有规范的最小与最大不动点。给出

$$[[\mu X.\phi ]]=\mu F_X,[[\nu X.\phi ]]=\nu F_X.$$

若 $X$ 在否定下负出现，算子可能反单调，不再能直接使用该定理。语法 positivity 是语义良定义的证明条件，不是风格约定。

例子与边界 ​

以下公式展示最小/最大不动点、交替层级和对偶在验证中的作用；同时标出终止状态、变量替换、性质语言与复杂度口径的边界。

可达性与安全公式 ​

到达目标 $goal$ 的状态集合为

$$\mu X.(goal\vee ⟨⟩X).$$

从空集迭代：第一轮加入目标，随后逐轮加入一步、两步等可到目标的前驱，有限图上最终稳定。

存在一条路径永远保持 $safe$ 可写成

$$\nu X.(safe\wedge ⟨⟩X).$$

从全状态集向下迭代，删除不安全或无法继续留在候选集中的状态。选择最大不动点允许无限地续接见证。

若把第二式误用 $\mu$，只从空集开始永远得空，无法表达无限协归纳行为。

全称模态可写作

$$[]X=S\setminus Pre(S\setminus X)$$

这个恒等式对任意转移关系都成立：右边恰好排除那些至少有一个后继落在 $S\setminus X$ 中的状态。在标准 box 语义下，无后继状态因而真空满足“所有后继都在 $X$”。给终止状态补自环是对 Kripke 结构的模型变换，会改变某些 next-like 公式；它不是恒等式成立的前提。

带动作标签的版本使用 $⟨a⟩,[a]$ 只量化 $a$ 边，可表达协议接口责任；把所有标签投影成一个无名模态会丢失动作区分。

嵌套不动点与无限重复 ​

“存在路径无限多次到达 $p$”可用交替不动点表达为

$$\nu X.\mu Y.((p\wedge ⟨⟩X)\vee ⟨⟩Y).$$

内层 $\mu Y$ 寻找有限路径到下一次 $p$，外层 $\nu X$ 要求这个责任可以无限重复。交换 $\mu ,\nu$ 会改变性质。

不动点 alternation depth 是表达和算法复杂度的重要参数。无交替片段可用较简单迭代，任意嵌套常归约为 parity game。

模型检查游戏中，析取和 existential modality 由验证者选择，合取和 universal modality 由反驳者选择；不动点优先级决定无限 play 胜者。状态满足公式当且仅当验证者有获胜策略。

游戏可输出反例或证明策略，而非只给满足状态集合。含 universal 分支的证明通常需要共享策略子图，单条 play 不足以覆盖对手所有选择。

与 CTL/CTL* 的关系 ​

CTL 可线性嵌入模态 $\mu$-演算：$EFp$ 使用最小不动点，$EGp$ 使用最大不动点。$\mu$-演算对有限转移系统的 bisimulation-invariant 性质提供高度统一语言。

表达能力强不代表每个规格都应写成嵌套不动点。时序算子通常更接近需求文本，$\mu$ 公式更适合统一算法与证明结构。

该逻辑是 qualitative 的；概率 $\mu$-演算或 quantitative extensions 需要把真值域和算子改变，不能从集合语义直接读取概率。

对偶与变量替换 ​

最小、最大不动点在否定下对偶：若把公式化到 positive normal form，需同时交换 $\mu /\nu$、$⟨⟩/[]$ 和原子命题极性。仅把 $\mu$ 改成 $\nu$ 不会得到补性质。

捕获避免替换同样重要。展开

$$\mu X.\phi \equiv \phi [X\mapsto \mu X.\phi ]$$

时，必须先重命名内部绑定变量，避免自由变量被意外捕获。实现 parser 或 normalizer 的 alpha-renaming 错误会直接改变不动点方程。

有限模型上的迭代最多严格改变 $|S|$ 次每个不动点变量，但嵌套重算可能更昂贵。parity-game 路线把优先级对应到交替层级，算法成本不能只按最外层循环估计。

公式大小和系统状态数都属于输入。固定公式的数据复杂度与公式一起变化的 combined complexity 是不同陈述，引用复杂度时需说明哪一项固定。

参考资料

• Dexter Kozen, “Results on the Propositional μ-Calculus,” Theoretical Computer Science 27, 1983, pp. 333–354。
• Julian Bradfield and Colin Stirling, “Modal Mu-Calculi,” in Handbook of Modal Logic, Elsevier, 2007, pp. 721–756。
• E. Allen Emerson, “Model Checking and the Mu-Calculus,” in Descriptive Complexity and Finite Models, AMS, 1996, pp. 185–214。