自动机论模型检查

从全称规格到语言交集 ​

设系统 $M$ 的路径标记语言为 $L(M)$，规格为 LTL 公式 $\phi$。系统违反规格当且仅当

$$L(M)\cap L_{\omega }({\mathcal{A}}_{\mathrm{\neg }\phi })\ne \varnothing ,$$

其中 ${\mathcal{A}}_{\mathrm{\neg }\phi }$ 由LTL 到 Büchi 转换公理库LTL 到 Büchi 自动机的转换LTL to Büchi translation · LTL-to-automata translation将 LTL 公式构造为接受其模型无限词的 Büchi 自动机，并揭示 closure、承诺跟踪与指数状态增长。得到。于是模型检查公理库模型检查问题Model checking problem · Model checking给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。化为 Büchi 语言交与非空性。

取否定是量词变换：$M\models \phi$ 要求所有系统路径满足 $\phi$；交集中的一个接受字就见证存在违反路径。

若系统本身已有公平接受条件，产品需要组合两个接受条件，通常形成 generalized Büchi 或其他 acceptance。不能只保留规格自动机的接受集。

同步积构造 ​

Kripke 状态 $s$ 与自动机状态 $q$ 组成产品状态 $(s,q)$。若系统有 $s\to s^{\prime }$，且自动机读取 $L(s^{\prime })$ 可从 $q$ 到 $q^{\prime }$，则

$$(s,q){\to }_P(s^{\prime },q^{\prime }).$$

有些约定让自动机先读 $L(s)$ 再转移，初始产品状态也随之变化；构造必须前后一致，否则反例会整体偏移一个状态。

产品接受状态通常是 $S\times F_A$。存在从初始产品状态可达、并能无限重复访问接受状态的路径，恰好表示系统路径被反例自动机接受。

产品无需一次性物化。后继生成器可按需组合系统后继与自动机转移，搜索只访问真正可达的状态对。

接受环判空 ​

有限产品图非空，当且仅当存在可达强连通分量公理库强连通分量算法Strongly connected components algorithm在线性时间内把有向图划分为互相可达的极大顶点集合。，其中含接受状态并拥有循环。单节点 SCC 只有在带自环时才形成无限循环。

算法可先求全部可达产品状态，再运行 SCC 分解；也可用 nested DFS on-the-fly 找接受环。若产品有 $N$ 个状态、$E$ 条边，显式判空核心为 $O(N+E)$。

这里的 $N$ 已包含系统状态数与公式自动机状态数的乘积。说“算法线性”必须指生成后的产品图，不能省略公式翻译的指数和产品增长。

请求无响应的 lasso ​

规格为 $G(request\to Fgrant)$。否定自动机猜测某次请求后进入“等待且永不见 grant”的接受监控状态。

若系统路径先到状态 $s_m$ 发出请求，再进入一个无 grant 的循环

$$s_m\to s_{m+1}\to \cdots \to s_n=s_m,$$

产品相应路径最终停留在接受 SCC。投影掉自动机分量，得到系统级 lasso 反例。

若循环中某状态含 grant，监控自动机无法沿接受状态继续，产品环被打断。只看系统图存在循环，不足以说明它违反该公式。

on-the-fly 不变量 ​

on-the-fly 搜索同时生成系统与公式状态，一旦找到接受环即可停止，不必探索与反例无关区域。正确性依赖每个已生成产品边都严格同步标签，并让 visited key 包含两个分量。

若 visited 只按系统状态去重，同一个 $s$ 搭配不同公式义务 $q$ 会被错误合并，可能漏掉接受环。自动机分量正记录“此前发生了什么时间义务”，不能为了省内存删除。

partial-order reduction 若与 LTL 产品结合，还需保持 stutter-invariant 性质并满足 cycle proviso；普通安全可达约简条件不足以自动保存接受循环。

模型与算法边界 ​

自动机路线验证有限或可有限生成模型上的 $\omega$ 行为。无限数据系统仍需抽象；抽象产品出现的接受 lasso 可能是伪反例。

翻译和产品构造产生的反例证明模型违反规格，不保证现实调度公平或实现与模型一致。公平假设、隐藏动作和终止自环都属于输入语义的一部分。

当公式自动机含非确定分支时，同一系统路径可对应多个产品路径；判空只需其中一条接受。visited 集必须保留自动机状态，不能因系统分量相同而合并这些不同义务。

参考资料

• Moshe Y. Vardi and Pierre Wolper, “An Automata-Theoretic Approach to Automatic Program Verification,” LICS, 1986, pp. 332–344。
• Costas Courcoubetis et al., “Memory-Efficient Algorithms for the Verification of Temporal Properties,” Formal Methods in System Design 1, 1992, pp. 275–288。
• Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008, Chs. 4–5。