自动机论模型检查

系统记位置，自动机记尚未兑现的义务 ​

系统顶点告诉我们“程序现在在哪里”，自动机顶点告诉我们“为了证明违反性质，此前选中了什么义务”。同一个系统状态可以搭配不同自动机状态。只按系统状态去重，会把不同历史义务混成同一个搜索节点；正确的 visited key 必须包含两个分量。

产品后继可以按需生成：枚举系统后继，读取其标签，再枚举自动机后继。显式状态搜索公理库显式状态模型检查Explicit-state model checking · Explicit model checking逐个生成和存储可达状态，以图搜索检查安全性及接受环的模型检查路线。因此不必先建立所有可能状态对，而只展开初始集合实际可达的部分。生成方式改变内存和发现反例的时机，却不改变每条边应满足的同步条件。

下面的共享算例把所有对象都列出来。积图的蓝色入箭头表示初态，双圈表示接受，虚线框表示强连通分量；红色 stem 与 loop 是完整反例证书。进入双圈一次还不够，必须有非空闭合路径能反复回来。积顶点名称的首字母表示系统状态，下标表示自动机状态，例如 $R_b=(r,b)$。

三状态请求系统与完整否定自动机 ​

取 $S=\{r,w,g\}$、$I=\{r\}$、$AP=\{request,grant\}$。四条系统边及标签如下；$w$ 可以继续等待，也可以得到授权。

规格为 $\phi =G(request\to Fgrant)$，否定为 $\psi =F(request\wedge G\mathrm{\neg }grant)$。$F$ 包括当前位置：同一时刻 request 和 grant 同真时，这个请求已获响应。公式也没有要求请求与授权一一匹配。

构造 $A_{\psi }=(\{z,b\},2^{AP},\delta ,\{z\},\{b\})$。状态 $z$ 表示尚未选择一个永不获响应的请求，$b$ 表示已选中并持续检查没有授权。下面列出字母表的全部四个字母；空集表示没有后继，自动机允许不完整。

证明它恰好识别 $\psi$。若运行接受，必须在某个位置第一次从 $z$ 进入 $b$；该字母含 request 且不含 grant。此后运行只能在 $b$ 留下，而每次留下都要求当前字母没有 grant，所以选中的请求此后永无授权，$\psi$ 成立。若词满足 $\psi$，取其见证位置 $i$，之前一直选择 $z$，读第 $i$ 个字母时选择 $b$，以后一直留在 $b$；这条运行无限访问接受态，故词被接受。

这个证明也解释了两种失败猜测：永远留在 $z$ 不接受；过早进入 $b$ 后遇到 grant，则该分支没有无限运行。非确定性允许放弃一次错误猜测，在另一个一直保持 $z$ 的分支上选择后来的坏请求。

手算全部五点七边 ​

读取初态 $r$ 的标签后，$z$ 可以转到 $z$ 或 $b$，故 $I_P=\{(r,z),(r,b)\}$。简记 $R_z=(r,z)$、$R_b=(r,b)$、$W_z=(w,z)$、$W_b=(w,b)$、$G_z=(g,z)$。逐项应用积定义得到：

这恰好是五点七边。没有 $(g,b)$，因为读取 grant 时 $b$ 没有后继；也没有 $W_z\to W_b$，因为 $w$ 的空标签没有 request，不能在这里新选坏请求。相反，$G_z\to R_b$ 合法：下一状态 $r$ 的 request 可以启动一次新的监控。

三个强连通分量公理库强连通分量算法Strongly connected components algorithm在线性时间内把有向图划分为互相可达的极大顶点集合。是 $C_0=\{R_z,W_z,G_z\}$、$C_1=\{R_b\}$、$C_2=\{W_b\}$。$C_0$ 有循环但没有接受点；$C_1$ 含接受点，却没有自环，不能无限停留；$C_2$ 有接受自环 $W_b\to W_b$。因此积非空。SCC 不必没有出边：只要存在内部接受循环，就可始终选择内部边；这里检查的是存在一条执行。

打印反例并回到原规格 ​

取 stem 为 $R_b\to W_b$，loop 为 $W_b\to W_b$。作为无限顶点序列，它是 $R_b(W_b{)}^{\omega }$；投影得到 $r{w}^{\omega }$，观察词为 $\{request\}{\varnothing }^{\omega }$，标准自动机运行为 $zbbb\cdots$。原规格在位置 $0$ 失败，因为该处存在请求，而任意 $j\ge 0$ 都没有授权。

这里 request 只在 stem 出现，loop 内没有 request。义务已经由 $b$ 记住，循环只需证明它永远不能兑现。反例与见证轨迹公理库反例与见证轨迹Counterexample trace · Witness trace · Diagnostic trace把模型检查结论具体化为安全坏前缀、活性 lasso 或存在性性质的行为见证。给出这个证书的逐边核验，包含初始分支、标签同步、闭环边和接受条件。

已解迁移题：删除等待自环 ​

只删系统边 $w\to w$，其余不变。系统仍然每个状态都有后继，唯一初始无限路径是 $(rwg{)}^{\omega }$；每个请求都在两步后授权，因此无需公平假设，规格就成立。

重新计算积，可达顶点仍为上述五个，边却只剩 $R_z\to W_z$、$R_b\to W_b$、$W_z\to G_z$、$G_z\to R_z$、$G_z\to R_b$，共五条。$C_0$ 的循环没有接受点，两个接受单点都没有自环；$W_b$ 甚至没有积后继。它代表“请求将永无授权”的一次有限猜测，下一步系统必到 $g$，授权标签使猜测失败。

积图有死路完全合法。系统 total 不意味着不完整自动机与它的积也 total；给 $W_b$ 补自环会凭空制造无限接受运行，改变监控语言。这不是修复图结构，而是引入假反例。

一般接受环判据及证明 ​

有限普通 Büchi 积非空，当且仅当有一个初始可达 SCC 同时包含接受点和正长度循环。必要性来自接受运行的无限访问：有限接受集中至少有一个顶点 $f$ 出现无限次，取两次不同时间的出现，便得到从 $f$ 返回 $f$ 的非空路径，其顶点都在同一个可达 SCC 中。

充分性也要构造实际路径。设该 SCC 含接受点 $f$。若分量只有 $f$，所需循环就是它的自环；若有至少两个顶点，强连通性给出从 $f$ 到另一个顶点再返回 $f$ 的非空闭合游走。先沿有限初始路径到达 $f$，然后无限重复这段游走，就得到接受运行。这同时证明有限 stem 加有限非空 loop 总能作为非空性的证书，但不意味着所有接受运行都最终周期。

对广义 Büchi 集合 $F_1,\dots ,F_m$，判据改成同一个可达循环 SCC 与每个 $F_j$ 相交。必要性可看运行无限访问的顶点集合：有限图中，所有只出现有限次的顶点最终消失；剩余顶点之间由运行的后缀相互连通，并包含每个接受集的一个代表。充分性则在 SCC 内依次连接各集合的代表，再回到起点，重复这个闭合游走。连接过程可能重复顶点，因此不要求一条简单环同时经过所有代表；不同 SCC 分别命中不同集合仍然不够。

若接受集合家族为空，接受义务真值为空合取，但无限运行仍需可达正长度循环。也可以先用计数器把广义条件退化为普通 Büchi；计数器须记录一整轮义务的完成，具体接口见转换页。

在共享例中加入公平条件 ​

把 $w\to g$ 命名为动作 serve。它只在 $w$ 使能。路径 $r{w}^{\omega }$ 从位置 $1$ 起持续使能 serve，却从未执行，因此违反 serve 的弱公平。系统无限路径或者最终永留 $w$，或者无限次到达 $g$ 并经 $r$ 重返 $w$。弱公平恰好排除前一类，所以在这个系统内，它等价于 justice 条件 $GFgrant$。

公平反例必须同时违反规格并满足公平假设。给积添加 $F_J=\{G_z\}$，同时保留原接受集 $F_A=\{R_b,W_b\}$；没有一个可达 SCC 同时命中两者，故公平反例语言为空。不能用 $F_J$ 替换 $F_A$，也不能取两者并集，因为那都会把两个必须共同满足的条件改掉。公平性约束公理库公平性约束Fairness constraint · Weak fairness · Strong fairness以弱公平、强公平等条件排除持续忽略可执行动作的不合理无限执行。进一步解释为什么一般动作公平不能未经编码直接换成这个状态 justice 条件。

把线性成本的输入说清楚 ​

设已经生成的可达积有 $N$ 个顶点、$E$ 条边。普通 Büchi 的 SCC 分解与接受标记检查使用 $O(N+E)$ 时间；若邻接表已物化，图本身占 $O(N+E)$ 空间，额外数组和搜索栈占 $O(N)$。只按需生成后继时可以不保存全部边，但不能因此把物化图的总存储也写成 $O(N)$。

若系统有 $n$ 个状态、$e$ 条边，自动机有 $k$ 个状态，每次 $\delta (q,a)$ 最多返回 $d$ 个后继，则 $N\le nk$、$E\le ekd$。这些计数默认标签测试和单个后继生成成本受控；复杂 guard 或大状态编码还应计入实际成本。通用 LTL 转换可产生 $2^{O(|\phi |)}$ 个状态，因此“对积线性”并非“对公式线性”。

广义接受条件还需要读入集合标记。若有 $m$ 个接受集合，其顶点成员记录总数为 $B$，直接在 SCC 中汇总的时间可写为 $O(N+E+m+B)$；稠密记录时 $B$ 可达 $Nm$。证书打印另计实际输出长度，串接多个接受代表得到的游走也不保证最短。按需搜索、SCC 搜索与普通 Büchi 的 nested DFS 都应保持各自不变量，不能把两个普通 DFS 随意嵌套。

自动机路线的结论仍然相对于输入模型。无限数据需要有限抽象时，积 lasso 可能需要进一步检查具体可行性；采用偏序约简时，也需证明保留所检查的时序性质与相关循环条件。这些步骤不改变本页最基本的检查链：语言正确、标签同步、循环闭合、接受义务满足。