有界模型检查

路径展开公式 ​

设 $I(s)$ 是初始谓词，$T(s,s^{\prime })$ 是转移关系，坏状态谓词为 $Bad(s)$。长度至多 $k$ 的安全反例可编码为

$$I(s_0)\wedge \underset{i=0}{\overset{k-1}{\bigwedge }}T(s_i,s_{i+1})\wedge \underset{i=0}{\overset{k}{\bigvee }}Bad(s_i).$$

若这个公式可满足公理库可满足公式Satisfiable formula存在至少一个真值赋值使其为真的命题公式。，模型赋值给出 $s_0,\dots ,s_k$，逐步构成真实有界路径。若不可满足，只说明该边界内不存在这种反例。

每个时间帧必须使用新状态变量副本。把所有 $s_i$ 复用为同一变量，会编码成单状态同时满足所有步，而非路径。

增量边界轨迹 ​

假设错误最短需要三步：初态 idle，两步准备后才进入 bad。$k=0,1,2$ 的公式均 UNSAT，$k=3$ 首次 SAT。

增量 SAT 可以复用 $I$ 与已生成转移子句，只加入新帧 $T(s_{k-1},s_k)$ 和对应目标。assumption literals 控制当前检查哪一层，避免每个 $k$ 从头求解。

首次 SAT 的 $k$ 给出最短转移长度反例，前提是从零逐层递增且每层编码确实覆盖“至多 $k$”。若每次只查恰好长度 $k$，终止状态没有自环时，短反例未必能延长到更大边界。

LTL 的 lasso 编码 ​

LTL公理库线性时序逻辑 LTLLinear temporal logic · LTL · Propositional temporal logic在单条无限状态序列上解释 next、until 及其派生算子，并以全路径量词规定系统满足关系。 反例需要无限行为。有限状态下可寻找长度 $k$ 的 stem，并选择回环位置 $0\le l<k$ 使

$$s_k=s_l.$$

随后在 lasso 上编码子公式真值和 until 接受责任。循环只证明路径可无限重复；还必须确保被违反规格对应的 Büchi 接受条件在循环中满足。

若不选择 loop，有限前缀对纯安全错误仍足够，却不能证明“请求永不响应”。任意有限无响应前缀都可能在下一步得到 grant。

bit-blasting 与理论边界 ​

位向量程序可把加法、比较和数组索引展开为布尔电路，再转 CNF。公式大小大致随边界 $k$ 线性复制组合逻辑，但位宽、乘法器和内存编码会决定每帧常数。

使用 SMT 可保留整数、数组或浮点理论结构；此时求解器理论、溢出语义和未定义行为必须与模型一致。把机器整数误编码成无界数学整数，SAT 结果可能对应不存在的实现路径，UNSAT 也可能漏掉回绕错误。

外部输入与非确定选择应作为自由变量，而非固定为某组测试值。BMC 的覆盖来自求解器对所有赋值搜索，不是把测试循环搬进 SAT。

完备阈值 ​

对有限状态安全可达性，若 $k$ 达到系统的 reachability diameter，$k$ 内无坏状态即可推出全局安全。实际求 diameter 可能与原问题同样困难。

还可结合 k-induction：base case 排除前 $k$ 步反例，step case证明任意连续 $k$ 个安全状态后下一状态仍安全。step case 可能因不可达状态失败，需要归纳加强。

因此 BMC 的三种输出要分开：SAT 给可靠反例；普通 UNSAT 给“边界内无反例”；带完备阈值或归纳证明的 UNSAT 才给全局结论。

失败边界与诊断 ​

边界太小会漏深层错误，增加 $k$ 又可能让公式超出内存。求解超时是 unknown，不应当作 UNSAT。

环境公平性和实时限制若未编码，求解器会选择任何合法转移，包括现实中被假设排除的路径。反例报告应显示 loop、输入和调度选择，以便核对模型假设。

编码正确性的独立责任 ​

Tseitin 转换把路径电路变成 CNF 时为子公式引入辅助变量，并以局部等价子句连接。若只编码单向蕴含以节省子句，必须证明当前 SAT 查询只需 equisatisfiability；方向错了会产生无法解码的伪模型。

数组、函数调用和内存常用精化编码：先忽略部分一致性约束，SAT 后检查模型并补 lemma。这是求解器内部的 abstraction refinement，不改变 BMC 的时间边界；报告应区分“当前近似 SAT，待理论检查”与已验证的具体反例。

多性质批量检查时，共享路径展开可节省子句，但每个坏谓词需要独立 assumption。把某个性质的 blocking clause 无条件用于另一个查询，可能排除其合法反例。

参考资料

• Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu, “Symbolic Model Checking without BDDs,” TACAS, 1999, pp. 193–207。
• Armin Biere et al., Handbook of Satisfiability, 2nd ed., IOS Press, 2021, Ch. 15。
• Edmund Clarke, Daniel Kroening, Joël Ouaknine, and Ofer Strichman, “Completeness and Complexity of Bounded Model Checking,” VMCAI, 2004, pp. 85–96。