显式状态模型检查

状态生成接口 ​

显式状态模型检查不要求预先列出整张图，而是提供三个可计算接口：初始状态枚举器 $Init$、后继生成器 $Succ(s)$ 与性质检查器 $bad(s)$。算法从初始状态开始逐个生成可达节点和转移。

对安全性质，worklist 版本维护已见集合 $V$ 与待处理集合 $W$：

$$V\leftarrow I,W\leftarrow I.$$

每次取出 $s\in W$，若 $bad(s)$ 则返回反例；否则对每个 $s^{\prime }\in Succ(s)$，仅在 $s^{\prime }\notin V$ 时记录父边并加入 $V,W$。当 $W$ 为空，所有可达状态均已检查。

这个算法实现模型检查公理库模型检查问题Model checking problem · Model checking给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。中的可达性特例。状态相等判定必须与模型语义一致；若哈希遗漏某变量，会错误合并状态，若加入无关地址或时间戳，又可能阻止本应共享的状态去重。

BFS 的最短反例轨迹 ​

设系统初态 $s_0$ 有两个分支：一条经 $s_1,s_2$ 到坏状态 $b$，另一条经十个状态后也到 $b$。BFS公理库广度优先搜索Breadth-first search · BFS按无权距离分层访问可达顶点的图遍历算法。按距离分层展开，第一次发现 $b$ 时父指针给出步数最短反例

$$s_0\to s_1\to s_2\to b.$$

最短按转移条数计，不一定是最短现实时间或最容易理解的根因。若边有成本，普通 BFS 的最短性不适用。

BFS frontier 可能非常宽，内存通常是瓶颈。DFS公理库深度优先搜索Depth-first search · DFS沿未访问边尽可能深入后回溯的图遍历算法。只保留搜索栈与 visited 表，更早深入某条长路径，却不保证最短安全反例。

无限性质与嵌套 DFS ​

检查 Büchi 接受条件需要寻找从初态可达的接受环。经典 nested DFS 先做外层 DFS；当一个接受状态完成时，再从它启动内层 DFS，检查能否回到仍相关的搜索区域。

若找到 stem $u$ 到接受状态 $f$，再找到 cycle $v$ 从 $f$ 回到 $f$ 或接受 SCC，就得到 lasso

$$u{v}^{\omega }.$$

只发现一个接受状态不够，因为它可能没有无限延伸回接受区域。相反，一个不含接受状态的循环也不构成 Büchi 反例。

不同 nested DFS 变体对颜色、搜索次序和 on-the-fly 产品构造有严格不变量；把两个普通 DFS 随意嵌套可能漏环或重复指数工作。

复杂度与真实存储 ​

若可达显式图有 $N$ 个状态、$M$ 条边，安全搜索的时间为 $O(N+M)$，visited、父指针和 frontier 使用 $O(N)$ 空间。这里 $N$ 是展开后的状态数，不是程序变量数或源代码行数。

每个状态还需序列化、归一化和哈希；每条转移需执行 guard 与 update。若状态包含大堆对象，单个节点成本不是常数。严谨报告应给出状态数、转移数、每状态字节和峰值 frontier。

哈希压缩若允许碰撞并把碰撞视为相等，会漏状态，成为有损搜索；只用哈希定位后再比较完整状态才能保留可靠性。bitstate hashing 明确以可能漏报换内存，结论不能写成完全证明。

工程边界 ​

对称约简、partial-order reduction 与状态压缩可以嵌入显式搜索，但各自需要证明代表状态覆盖原行为。搜索框架相同不意味着约简天然 sound。

动态内存、未界队列和递归栈使状态空间无限。给队列设上界能得到有限模型，却只验证该界内行为；若反例需要更长队列，“无反例”不能推广到原系统。

显式检查的优势是状态和反例直观、算法可预测；缺点是组合状态全部物化。状态空间爆炸公理库状态空间爆炸State-space explosion · Combinatorial state explosion并发组件、变量域和未界结构组合后使全局状态数呈乘积或指数增长的结构性现象。分析这种增长从何而来，符号方法则尝试用一个公式代表许多状态。

搜索状态的规范化 ​

并发状态若含无关进程编号、堆对象地址或消息排列，可以在入 visited 前做 canonicalization，但规范化必须保持后继行为和观察。两个状态排序后字节相同却拥有不同权限或未来动作时，合并会漏路径。正确做法是先证明 canonical representative 与原状态模拟或对称等价，再把它作为去重键，而不是凭数据外观压缩。

参考资料

• Gerard J. Holzmann, The SPIN Model Checker, Addison-Wesley, 2004, Chs. 6–9。
• Edmund M. Clarke, Orna Grumberg, and Doron A. Peled, Model Checking, MIT Press, 1999, Chs. 2, 9。
• Costas Courcoubetis, Moshe Vardi, Pierre Wolper, and Mihalis Yannakakis, “Memory-Efficient Algorithms for the Verification of Temporal Properties,” Formal Methods in System Design 1, 1992, pp. 275–288。