显式状态模型检查

BFS 的最短反例轨迹 ​

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

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

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

无限性质与嵌套 DFS ​

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

若找到 stem $u$ 到达接受状态 $f$，再找到从 $f$ 返回 $f$ 的非空 cycle $v$，就得到 lasso

只发现一个接受状态不够。例如 $s_0\to f\to d$，其中只有 $f$ 接受而 $d\to d$：唯一无限执行只访问 $f$ 一次，因此不满足“无限次访问接受状态”。若改为 $f\to g\to f$，则 $s_0(fg{)}^{\omega }$ 无限次访问 $f$，构成接受运行。验证 LTL 时，这里的图通常是系统与否定性质自动机的乘积图；接受运行因此表示原性质的反例，而不是原系统中任意一个循环。

也可以在可达图上做强连通分量理路强连通分量算法Strongly connected components algorithm在线性时间内把有向图划分为互相可达的极大顶点集合。（SCC）分解：普通 Büchi 只需找到含接受点的可达循环分量。完整请求系统积图理路自动机论模型检查Automata-theoretic model checking · Automata-based LTL model checking将系统与否定规格 Büchi 自动机同步取积，并以可达接受环判定 LTL 违反行为。给出了一个可以手算的任务：两个初始积状态展开出五个顶点、七条边，分为三个 SCC。接受点 $R_b$ 所在分量没有自环，不能报告；$W_b$ 的接受自环才交付 lasso。算法若只按系统分量 $r,w,g$ 去重，会把同一位置的不同监控义务合并，破坏这个结论。

这个任务的已解变体只删系统等待自环，积仍有五个可达顶点，但仅剩五条边。两个接受点都存在，却没有接受循环；其中一个积点没有后继，是自动机猜测被后续授权否定的结果。后继生成器应返回空集，不得为保持图的 total 性自行补边。

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

复杂度与真实存储 ​

若可达显式图有 $N$ 个状态、$E$ 条边，安全搜索的时间为 $O(N+E)$，visited、父指针和 frontier 使用 $O(N)$ 辅助空间。若完整邻接表已经物化，图存储还需 $O(N+E)$，不能把辅助数组的界当成总存储界。普通 Büchi 的 SCC 判空也在这个显式规模下使用 $O(N+E)$ 时间。这里 $N$ 是展开后的状态数，不是程序变量数或源代码行数。

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

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

工程边界 ​

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

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

显式检查的优势是状态和反例直观、算法成本可按展开图解释；缺点是已探索的组合状态仍需逐个表示。状态空间爆炸理路状态空间爆炸State-space explosion · Combinatorial state explosion并发组件、变量域和未界结构组合后使全局状态数呈乘积或指数增长的结构性现象。分析这种增长从何而来，符号模型检查理路符号模型检查Symbolic model checking · BDD-based symbolic model checking用布尔公式或 OBDD 整体表示状态集合与转移关系，并通过量化和不动点运算检查时序性质。则用一个布尔对象表示整批状态。后者可能压缩规则集合，也可能因表示膨胀更差；两条路线改变表示，不改变满足语义。

搜索状态的规范化 ​

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

无限状态系统不能总靠列出全部状态结束搜索。后向覆盖算法理路覆盖性的后向基算法Backward coverability algorithm从向上闭坏状态反向扩展有限基，给出 Petri 网前驱公式、完整小例运行与终止和安全不动点证明。保存向上闭坏状态集的有限最小基，Karp–Miller 树理路Karp–Miller 覆盖树Karp-Miller tree用沿祖先的增长比较将 Petri 网无界计数加速为 omega，手算树并以奇偶约束区分覆盖与精确可达。则从初态用 omega 概括可泵大的 Petri 计数。二者都回答覆盖问题，不能把摘要中的一个目标直接当作精确可达状态。