有界模型检查

增量边界轨迹 ​

设唯一相关路径是

则 $C{E}_0,C{E}_1,C{E}_2$ 均 UNSAT，$C{E}_3$ 首次 SAT，并给出赋值

增量 SAT 可以复用 $I$ 与已生成的转移子句，每轮只加入新帧和 $Bad(s_k)$ 查询；assumption literals 控制当前目标而不污染后续边界。

从 $0$ 逐层检查 $C{E}_k$ 时，首次 SAT 的 $k$ 就是最短转移长度。若跳过较小边界，或用强制长路径却没有终止自环，便不能从首次求解结果推出最短性。

LTL 的 lasso 编码 ​

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

随后在 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 无条件用于另一个查询，可能排除其合法反例。