自动机论模型检查

同步积构造 ​

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

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

没有额外系统公平条件且规格自动机采用单一 Büchi 接受集时，产品接受状态是 $S\times F_A$。存在从初始产品状态可达、并能无限重复访问该集合的路径，恰好表示系统路径被反例自动机接受。

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

接受环判空 ​

对单一接受集的普通 Büchi 产品，语言非空当且仅当存在一个可达强连通分量公理库强连通分量算法Strongly connected components algorithm在线性时间内把有向图划分为互相可达的极大顶点集合。，它拥有循环并与接受集相交。单节点 SCC 只有在带自环时才形成无限循环。

若产品采用 generalized Büchi 接受集合 $F_1,\dots ,F_m$，则同一个可达循环 SCC 必须与每个 $F_j$ 都相交；分别找到落在不同 SCC 的接受状态并不够。也可以先用计数器 degeneralize 成普通 Büchi，再应用单接受集判据。

算法可先求全部可达产品状态，再运行 SCC 分解；普通 Büchi 也可用 nested DFS on-the-fly 找接受环，generalized Büchi 则先退化或使用对应的多接受集算法。对普通产品，或把退化计数器计入产品规模后，若图有 $N$ 个状态、$E$ 条边，显式判空核心为 $O(N+E)$。

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

请求无响应的产品轨迹 ​

取两状态系统 $s_0\to s_1$、$s_1\to s_1$，其中

规格 $G(request\to Fgrant)$ 的否定自动机可在读到 $s_0$ 时猜中该请求，进入接受监控状态 $q_w$；$q_w$ 只要继续读到 $\mathrm{\neg }grant$ 就自环。采用“先读当前状态标记”的约定，产品运行是

$(s_1,q_w)$ 是可达接受自环，所以产品非空；投影得到系统 lasso $s_0{s}_1^{\omega }$。若 $s_1$ 标有 grant，$q_w$ 的无授权监控边就不能继续，接受环随之消失。可见系统图“有循环”只是必要结构，是否违反公式还取决于自动机义务。

on-the-fly 不变量 ​

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

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

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

模型与算法边界 ​

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

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

当公式自动机含非确定分支时，同一系统路径可对应多个产品路径；判空只需其中一条接受。