状态空间爆炸 | Codeboy's Blog

乘积状态不是实现偶然

若组件 $i$ 有 $n_i$ 个局部状态，不考虑约束时同步产品最多有

N=\prod_{i=1}^{k}n_i

个全局状态。 $k$ 个布尔变量已经给出 $2^k$ 个赋值； $k$ 个各有 $m$ 个位置的线程给出 $m^k$ 个控制位置组合。

这就是状态空间爆炸：紧凑系统描述经组合语义展开后，状态数按变量或组件数指数增长。它不是单纯“工具内存管理不好”，而是模型对象本身的渐近规模发生了变化。

可达约束会删去某些笛卡尔积状态，但最坏情形仍可接近乘积。仅因为一个样例协议的多数状态不可达，不能推断同类系统普遍紧凑。

三个线程各执行四条原子指令，忽略共享数据时，每线程程序计数器有五个位置。全局控制向量已有

5^3=125

种组合。若再有六个布尔共享变量，上界乘以 $2^6$ ，变成 $8000$ 个状态。

这还没有计算寄存器值、锁所有者和消息缓冲。若每个线程两条指令的顺序固定，全部跨线程 interleaving 数为多项式系数

\frac{12!}{(4!)^3}=34650,

路径数可以远大于状态数，因为多条交错会汇合到同一全局状态。路径爆炸与状态爆炸相关，却不是同一个计数。

一个 $w$ 位整数变量有 $2^w$ 个位模式；两个独立数组的组合取域大小乘积。把整数数学模型换成有限机器整数能使状态有限，却可能得到极大的有限空间，并引入溢出行为。

长度上界为 $B$ 、消息字母表大小为 $m$ 的 FIFO 队列有

1+m+m^2+\cdots+m^B

种内容。若队列无界，系统通常直接变成无限状态，而不只是一个更大的有限图。

递归调用栈、动态对象身份和时间戳也会扩大状态。抽象掉它们必须证明被删除差异不影响待验证性质，不能为节省内存任意截断。

位打包把每状态字节数从数十字节降到少量字节，却没有改变状态个数的指数。哈希表优化常数，不能改变 $2^k$ 的增长阶。

符号表示有时能用短公式代表指数多状态，例如“所有变量为任意值”只需常量 true；但也存在 OBDD 或逻辑表示必须指数大的函数。符号方法利用结构，不是对所有输入的通用压缩定理。

并发动作独立时，偏序约简可只探索同一 Mazurkiewicz trace 的代表交错；若动作读写冲突，交换会改变结果，就不能合并。对称约简、抽象解释和 compositional verification 也各有适用不变量。

显式检查应分别报告生成状态数、唯一状态数、转移数、最大 frontier、每状态存储和探索时间。只写“搜索了很多状态”无法区分后继生成慢、重复率高或真正状态数巨大。

组合参数也要列出：线程数、变量位宽、队列界和上下文切换界。把队列上界从 $B$ 改成 $B+1$ 可能乘上近似 $m$ ；换一个小数字例子不能代表伸缩规律。

状态空间爆炸是结构性风险，不等于模型检查不可用。实际系统常有局部性、对称性和不变量可利用；正确问题是识别哪种结构允许哪种约简，并保存哪些性质。

将循环展开到 $k$ 步、队列限制到 $B$ 或线程切换限制到 $c$ ，能得到可检查子模型。找到反例时，只要路径在原模型中合法，就有真实诊断价值。

没有反例只说明所给边界内未发现违反。除非证明 completeness threshold 或小模型性质，不能把有限边界结果升级成无界正确性。

状态数量也不是验证难度的唯一因素。一个巨大但规则的状态集合可有紧凑符号表示；一个较小却后继计算昂贵的模型也可能难查。规模与结构需要分别报告。

组合式验证尝试不先构造完整产品：为组件建立 assume–guarantee 契约，再证明局部行为在环境假设下满足局部保证。它能把某些乘积拆开，但契约推导本身可能困难，且循环依赖的假设需独立闭合。把系统文件拆成多个模块不会自动降低语义产品规模；真正节省来自被证明可隐藏的接口状态。

参数化系统又增加一层风险：固定三、四个进程通过，不代表任意进程数成立。cutoff 定理若能证明检查某个有限规模足够，就必须写出协议拓扑、对称性和性质局部性假设；没有 cutoff 时，逐个提高实例数只是寻找反例的半判定过程。

参考资料

Edmund M. Clarke, Orna Grumberg, and Doron A. Peled, Model Checking, MIT Press, 1999, Chs. 1, 10。
Gerard J. Holzmann, The SPIN Model Checker, Addison-Wesley, 2004, Chs. 9, 11–12。
Patrice Godefroid, Partial-Order Methods for the Verification of Concurrent Systems, Springer, 1996, Chs. 1–2。