模型检查问题

Model–Specification–Decision–Witness ​

一项模型检查任务由四部分组成：

1. Model：有限或有限表示的系统模型 $M$，包括初始状态与转移；
2. Specification：在明确语义下解释的规格 $\phi$；
3. Decision：判定指定初始行为是否满足规格；
4. Witness：为违反、存在性成立或证明成功提供可核验的诊断对象。

对Kripke 结构公理库Kripke 结构Kripke structure · Kripke transition structure以状态转移和原子命题标记解释分支时间性质的状态模型。 $K=(S,I,R,AP,L)$，全局 decision 通常写作

$$K\models \phi ⟺\mathrm{\forall }{s}_0\in I,K,s_0\models \phi .$$

局部问题给定单个状态 $s$，询问 $K,s\models \phi$。若公式是路径公式，还要按照所选时序逻辑公理库时序逻辑Temporal logic · Temporal modal logic在执行序列上解释下一步、最终、始终与直到，并区分线性时间和分支时间的统一规格层。规定路径量词；不能在 LTL、CTL 和 CTL* 之间复用一个未说明的满足符号。

decision 至少返回 satisfied 或 violated。witness 可以是违反时的反例路径、存在性公式成立时的见证路径，或安全证明中的归纳不变式。证书能否由较小内核独立检查，是工具可信边界的一部分；布尔答案本身没有解释模型和规格是否写对。

一个小型互斥检查 ​

设两个进程的组合状态为 $({\ell }_1,{\ell }_2)$，每个位置属于 $N,T,C$。初始状态是 $(N,N)$，规格为

$$\phi =G\mathrm{\neg }(c_1\wedge c_2).$$

显式检查可以从初态枚举可达图；一旦到达 $(C,C)$，当前有限路径就见证安全性失败。若图搜索穷尽全部可达状态仍未遇到双临界状态，便对这个有限模型证明互斥。

这个结论的量词覆盖模型中的全部可达交错，不只是测试运行采样到的路径。反过来，它只覆盖模型写出的进程位置、共享变量和转移；若真实代码还有未建模的中断处理，模型检查并未验证那条实现路径。

求解路线不属于问题定义 ​

“模型检查”是一类判定任务，不是一种固定搜索算法。显式搜索枚举可达图，符号方法压缩状态集合，自动机路线寻找接受环，有界方法只展开有限深度，归纳方法则学习可推广的安全证书。它们共享同一个 model–specification–decision 接口，却有不同的完备条件、资源尺度和 witness 形状；选择哪条路线不能改变原问题的满足关系。

复杂度的正确尺度 ​

显式图已经给出时，基本可达性成本按 $|S|+|R|$ 衡量。若模型由 $n$ 个布尔变量紧凑描述，潜在状态数却是 $2^n$。因此“对状态数线性”不等于“对程序文本线性”。

公式大小同样属于输入。CTL 检查对显式 Kripke 图和公式大小可做到近线性乘积量级；LTL 路线通常在公式长度上产生指数规模的自动机，再对乘积图做线性搜索。复杂度陈述必须指出模型表示、逻辑种类与公式是否固定。

无限状态系统不能直接以有限 $|S|$ 计数。某些系统有有限符号表示并可借抽象、归纳或约束求解处理，另一些模型检查问题不可判定。工具在若干基准上终止，不能推出整个语言片段都有判定算法。

反例、无反例与证明 ​

安全性质的反例通常是一条到达坏状态的有限路径；liveness 反例常是 stem 加 cycle 的 lasso，表示无限重复的坏行为。CTL 的存在或全称子公式还可能需要树状 witness，而不总是一条线性路径。

有界模型检查找到长度不超过 $k$ 的真实路径时，反例是可靠的。若 SAT 求解器只返回“$k$ 内无反例”，这并不证明更长路径不存在；只有达到已证明的 completeness threshold，或另有归纳证书时，才能把无反例升级为全局正确。

反例也不自动定位根因。最短反例减少路径长度，却可能穿过多个症状状态；工程诊断还需映射回源代码、输入和环境假设。

模型、规格与实现三层 ​

正确性公理库算法正确性Algorithm correctness · Partial and total correctness所有合法执行都符合规格，并在完全正确时保证终止。陈述必须固定被验证对象。模型检查能证明 $M\models \phi$，但要推广到实现 $P$，还需要证明 $P$ 的行为被 $M$ 覆盖，或建立 simulation/refinement。若抽象模型遗漏实现行为，模型内证明依然可能为真。

规格本身也可能错误。公式 $G\mathrm{\neg }error$ 若把所有错误状态都漏标成正常，检查器会忠实地返回满足。模型检查减少的是状态空间内的遗漏，不代替需求评审和原子命题校准。

有限状态不等于小状态。并发组件的笛卡尔积、变量域和队列内容都会造成状态空间爆炸。某种表示或约简能否缓解它，取决于模型结构和待保持性质；把工具链名称列得更长，不会让任意系统自动变得紧凑。

参考资料

• Edmund M. Clarke and E. Allen Emerson, “Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic,” Logic of Programs, Springer, 1981, pp. 52–71。
• Edmund M. Clarke, Orna Grumberg, and Doron A. Peled, Model Checking, MIT Press, 1999, Chs. 1–4。
• Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008, Chs. 1, 4–6。
• Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, eds., Handbook of Model Checking, Springer, 2018, Chs. 1–3。