模型检查问题

一个小型互斥检查 ​

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

显式检查公理库显式状态模型检查Explicit-state model checking · Explicit model checking逐个生成和存储可达状态，以图搜索检查安全性及接受环的模型检查路线。可以从初态枚举可达图。若模型允许每个进程独立执行 $N\to T\to C$，就有反例 $(N,N)\to (T,N)\to (C,N)\to (C,T)\to (C,C)$。每一步只推进一个进程，最后状态使两个临界区命题同时为真；这说明“每次只运行一个进程”本身并不保证互斥。

若改为仅当另一进程不在 $C$ 时才能执行 $T\to C$，上述最后一步便被禁止。要证明修改后的模型安全，仍须穷尽全部可达状态或提供归纳不变式，不能只重放这一条已被阻断的反例。

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

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

“模型检查”是一类判定任务，不是一种固定搜索算法。显式搜索枚举可达图，符号方法压缩状态集合，自动机路线寻找接受环，有界方法只展开有限深度，归纳方法则学习可推广的安全证书。它们共享 model–specification–decision 接口，却有不同的 soundness/completeness 条件、资源尺度和 witness 形状；更换后端不能偷偷更改原问题的满足关系。具体适用范围也须匹配：显式可达搜索和有限布尔 PDR直接处理安全性，CTL 可用精确符号不动点，LTL 可用自动机积判空。BMC在普通边界内只实现有界反例查询；只有再给出相应完备阈值或归纳证书时，它才为原来的全局任务交付判定。

复杂度的正确尺度 ​

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

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

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

反例、无反例与证明 ​

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

有界模型检查公理库有界模型检查Bounded model checking · BMC · SAT-based bounded model checking将前 k 步转移展开为 SAT 公式寻找有界反例，并明确无解结果何时不能升级为全局证明。找到长度不超过 $k$ 的真实路径时，反例是可靠的。若 SAT 求解器只返回“$k$ 内无反例”，这并不证明更长路径不存在；只有达到已证明的 completeness threshold，或另有归纳证书时，才能把无反例升级为全局正确。

安全证书可以具体写成状态集合 $J$：检查 $I\subseteq J$、$s\in J\wedge R(s,s^{\prime })\Rightarrow s^{\prime }\in J$，以及 $J$ 不含坏状态。三个义务分别保证覆盖起点、沿每一步封闭和排除错误；它们说明为什么有限证书可以覆盖任意长执行。只列出若干已访问的安全状态，若没有闭包检查，就还不是这种证书。

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

实现路线由规格形态和状态表示决定。符号模型检查公理库符号模型检查Symbolic model checking · BDD-based symbolic model checking用布尔公式或 OBDD 整体表示状态集合与转移关系，并通过量化和不动点运算检查时序性质。用 BDD 或逻辑公式整体表示状态集合并做不动点运算；自动机论模型检查公理库自动机论模型检查Automata-theoretic model checking · Automata-based LTL model checking将系统与否定规格 Büchi 自动机同步取积，并以可达接受环判定 LTL 违反行为。把 LTL 等性质转成 $\omega$-自动机，再检查与系统积的空性；Property-Directed Reachability / IC3公理库Property-Directed Reachability / IC3Property-directed reachability · PDR · IC3以 SAT 查询阻塞坏状态前驱、学习逐层归纳子句，最终得到反例或安全归纳不变式。为安全性质逐层学习归纳子句。三者分别依赖可压缩集合表示、自动机翻译和可归纳阻断，不存在对任意模型都占优的单一后端。

模型、规格与实现三层 ​

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

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

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