符号模型检查

集合变成特征函数 ​

令状态由布尔向量 $x=(x_1,\dots ,x_n)$ 编码，下一状态用 $x^{\prime }$。状态集合 $S$ 表示为特征公式 $S(x)$，转移关系表示为

$$T(x,x^{\prime }).$$

一个公式节点可以代表许多显式状态。OBDD公理库有序二元决策图 OBDDOrdered binary decision diagram · Reduced ordered binary decision diagram · ROBDD · OBDD固定变量顺序并共享、约简等价子图后得到的规范布尔函数有向无环表示。提供规范布尔函数表示及 conjunction、quantification、renaming 等操作。

符号模型检查改变的是表示与集合算法，不改变模型检查问题公理库模型检查问题Model checking problem · Model checking给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。的满足语义。公式必须精确编码变量位宽、初态和每条转移。

image 与 predecessor ​

从集合 $S(x)$ 出发的一步后继为

$$Post(S)(x^{\prime })=\mathrm{\exists }x.S(x)\wedge T(x,x^{\prime }).$$

量化掉旧状态变量后，再把 $x^{\prime }$ 重命名为 $x$ 以继续迭代。前驱运算是

$$Pre(S)(x)=\mathrm{\exists }{x}^{\prime }.T(x,x^{\prime })\wedge S(x^{\prime }).$$

变量量化方向若写反，会把目标集合约束到当前状态而非后继。当前/下一变量必须分成两套互不冲突的编码。

可达性固定点轨迹 ​

从初始集合 $R_0=I$ 开始，计算

$$R_{i+1}=R_i\vee Post(R_i).$$

当 OBDD 表示的布尔函数不再变化时，得到全部可达状态。规范 OBDD 允许用根节点相等判断固定点，而无需枚举具体赋值。

例如 $n$ 位计数器从零递增，显式需访问 $2^n$ 个状态；可达集合最终是 true，表示可能为任意位模式，终值极紧凑。不过中间 transition relation 和 image 的 BDD 大小仍依变量顺序而变。

若计数器只允许偶数状态，特征函数可压成最低位为零。符号压缩来自函数结构，不来自状态数量本身。

CTL 的集合递归 ​

对CTL公理库计算树逻辑 CTLComputation tree logic · CTL · Branching-time temporal logic将路径量词 A/E 与时间算子成对组合，在 Kripke 状态上表达分支未来性质。，每个子公式对应满足状态 OBDD。布尔联结直接用集合运算，$EX\phi$ 用 $Pre(Sat(\phi ))$。

$E[\phi U\psi ]$ 通过最小不动点

$$Z_{i+1}=Sat(\psi )\vee (Sat(\phi )\wedge Pre(Z_i)),Z_0=false,$$

计算；$EG\phi$ 从 $Z_0=true$ 出发按

$$Z_{i+1}=Sat(\phi )\wedge Pre(Z_i)$$

求最大不动点。初值和迭代方向对应公式语义，互换会得到另一个解。

partitioned transition relation ​

整体 $T$ 可能过大，可按组件或赋值分解为 $T_1\wedge \cdots \wedge T_m$，在 relational product 中尽早量化不再需要的变量。这个优化减少中间峰值，但量化时机必须保证变量以后不再被剩余分区引用。

若过早量化共享变量，会把不同转移约束解耦，产生不存在的后继；过晚量化则保持正确但可能造成 BDD 爆炸。

变量重排、分区顺序和缓存决定实际性能，任何一种启发式都没有对全部布尔函数的紧凑保证。

symbolic 不等于 SAT-only ​

“symbolic”泛指用公式代表集合。经典路线以 BDD 和不动点为中心；SAT-based BMC 展开有限路径，PDR 学习归纳子句，SMT 还能处理理论值域。它们不能因都出现布尔公式就视为同一算法。

BDD 图可能指数大，符号算法也会耗尽内存。反过来，显式搜索在稀疏小图上可能更快。选择表示应基于转移结构和性质，不是默认 symbolic 一定避免状态爆炸。

反例提取 ​

集合不动点只告诉哪些状态满足或违反公式，要输出路径还需保存 frontier 层、选择具体满足赋值，并逐层求一个与 $T$ 相容的 predecessor。随意从每层 BDD 各取一个状态，选出的相邻赋值可能没有转移边。可靠提取应反向约束

$$s_i(x)\wedge T(x,x^{\prime })\wedge s_{i+1}(x^{\prime })$$

并由可满足模型确定每一步；liveness 还要在接受 SCC 中闭合循环。符号证书最终仍必须对应合法具体路径。

状态编码也可能含 unused bit patterns。若两位编码只代表三个枚举值，第四种位型必须由 invariant 排除或赋予明确语义；否则符号运算会把不存在状态传播进可达集。

参考资料

• Kenneth L. McMillan, Symbolic Model Checking, Kluwer, 1993, Chs. 2–4。
• Jerry R. Burch et al., “Symbolic Model Checking: ${10}^{20}$ States and Beyond,” Information and Computation 98(2), 1992, pp. 142–170。
• Edmund M. Clarke, Orna Grumberg, and Doron A. Peled, Model Checking, MIT Press, 1999, Chs. 6–8。