安全博弈与反应式综合

安全策略靠闭包维持 ​

对每个 $v\in W\cap V_C$，从 $W=F(W)$ 可知至少有一个后继仍在 $W$，任取一个作为 $\sigma (v)$。对每个 $v\in W\cap V_E$，同一等式保证它的每个后继都在 $W$。在其他控制器顶点任取合法选择，即可把 $\sigma$ 补成整个图上的位置策略。

从任意 $v_0\in W$ 出发，若当前 $v_k\in W$，控制器的一步由策略留在 $W$，环境的一步由全部后继的闭包留在 $W$。对执行长度归纳，任意环境策略产生的每个 $v_k$ 都在 $W\subseteq S$。所以 $W\subseteq \mathrm{Win}$，而且同一个 $\sigma$ 同时适用于所有获胜初态。

这也说明“待在安全状态”为什么不够：某个状态眼下安全，却可能让环境下一步直接进入坏状态。迭代删除的正是这种无法持续兑现的安全承诺；稳定后留下的区域才有逐步维持安全的能力。

失败策略靠秩严格下降 ​

为了证明删掉的状态确实无法挽救，从坏状态向后生长集合：

环境只需有一条边通往已知失败状态，就能主动选择它；控制器要到所有选择都已失败时才被加入。具体地，令 $A(X)$ 表示上式中两个前驱集合的并，德摩根律给出 $V\setminus W_{i+1}=B\cup A(V\setminus W_i)$。从 $L_0=B$ 出发，这个序列单调增长：首步包含 $B$，此后由 $A$ 的单调性归纳。因而 $B\cup A(L_i)=L_i\cup A(L_i)$，与写出的增长规则一致，逐层得到 $L_i=V\setminus W_i$。因此稳定集 $L$ 恰为 $V\setminus W$。

为 $v\in L$ 定义首次加入的层数

若 $r(v)=k>0$ 且 $v\in V_E$，它首次加入 $L_k$ 时至少有一个后继属于 $L_{k-1}$，环境固定选择这样的后继。若 $v\in V_C$，首次加入规则保证它的所有后继都属于 $L_{k-1}$。因而不论控制器怎样选择，只要当前秩为正，下一步的秩都严格变小。

非负整数不能无限严格下降，所以从 $v\in L$ 出发，环境的这个位置策略迫使执行至多经过 $r(v)$ 步到达秩零，即进入 $B$。反策略在 $B$ 以及其余环境顶点任意补全即可；坏状态一旦被访问，安全目标已经失败。于是 $L\cap \mathrm{Win}=\varnothing$，结合获胜策略便完成 $W=\mathrm{Win}$ 的双向证明。

获胜策略只要求在 $W$ 内闭合，失败反策略却必须推动秩下降。随便选一条仍在 $L$ 内的边可能不断绕圈，并不能证明最终到达坏状态。闭包证书与进度证书承担的是不同的证明责任。

Büchi 获胜侧：每次到达后重新开始下降 ​

先证明每个 $Z_j$ 都满足两条全图条件：环境顶点的全部后继在 $Z_j$，控制器顶点至少有一个后继在 $Z_j$。初始 $V$ 显然满足。删除环境吸引域 $D_j$ 后，补集性质保证剩余环境顶点的全部 $Z_j$ 内后继仍在补集，剩余控制器顶点有一个后继在补集；配合上一轮环境的全图闭包，便完成归纳。因此每个非空诱导子图确实总有后继，没有把死端上的空全称误当作能力。

结束时 $W={\mathrm{Attr}}_{C,W}(F\cap W)$。在 $W\setminus F$ 的控制器顶点，固定选一条使最终吸引秩严格下降的边；在 $W\cap F$ 的控制器顶点，固定任选一条留在 $W$ 的边。环境的任何选择都留在 $W$；在非目标环境顶点，所有后继的秩都严格更低。

所以从任意 $W$ 内初态有限步就能访问 $F$。每次访问后，下一步仍在 $W$，同一论证再次生效。若声称某次是最后一次访问，则之后不断下降的非负整数秩导致矛盾。这就证明同一个位置策略从整个 $W$ 获胜；不能把证明停在“第一次能到达”。

Büchi 失败侧：外层编号最终稳定 ​

每个被删顶点唯一属于某轮 $D_j$。在该轮正吸引秩的环境顶点，选择一条更低秩边；在秩零区域 $X_j$ 的环境顶点，选择一条仍在 $X_j$ 的边。后者存在，因为 $X_j$ 是控制器吸引域的补集。每个顶点只有一个删除轮次，故这些选择合并成一个位置策略，不需要运行时记忆当前轮次。

从 $D_j$ 出发，在这个环境策略下有两种情况。若控制器走出 $Z_j$，就进入某个更早删除的 $D_i$，其中 $i<j$。若留在 $Z_j$，正吸引秩严格下降；进入 $X_j$ 后，控制器的所有子图内后继都在 $X_j$，环境也留在那里。又因为 $F\cap Z_j\subseteq Y_j$，有 $X_j\cap F=\varnothing$。

于是沿执行，删除轮次只可能不变或严格变小，永远不会跳到更晚轮次或最终保留集。有限次下降后它稳定；此后吸引秩下降到零，执行永远留在一个不含 $F$ 的 $X_j$。之前只是有限前缀，因而全执行至多有限次访问 $F$。这证明被删除区域全部由环境获胜，与上一节一起得到准确分区和双方位置策略。

这里保留了“可能走到更早删除层”的分支。仅在诱导子图内证明环境能到 $X_j$，却忽略控制器原图里的出界边，会留下策略证明的缺口。

六个状态逐层求解 ​

取控制器顶点 $V_C=\{s,a,c\}$，环境顶点 $V_E=\{e,f,b\}$，唯一坏状态为 $b$。完整后继表如下；表外没有其他边。

图中圈定的 $W=\{s,a\}$ 是完整获胜区域。粗实线表示控制器的获胜选择，粗虚线表示环境的下降选择；其余细边仍是博弈中的合法选择。节点旁的 $r$ 标出首次进入失败集合的层数，形状标出行动归属。

每轮同时根据上一轮集合更新，结果为：

第一轮 $f$ 被加入，因为环境可直接选 $f\to b$；第二轮 $e$ 被加入，因为环境可选 $e\to f$；第三轮 $c$ 被加入，因为它唯一的后继 $e$ 已失败。虽然 $s$ 也有边进入 $e$，控制器仍能选择 $s\to a$，故 $s$ 不被删除。

综合得到 $\sigma (s)=a$、$\sigma (a)=a$。失败侧的秩为 $r(b)=0,r(f)=1,r(e)=2,r(c)=3$；环境选择 $e\to f$、$f\to b$，从 $c$ 出发便强制执行 $c\to e\to f\to b$，恰在三步后到达坏状态。

从 $e$ 存在安全路径 $e\to a\to a\to \cdots$，但选择 $e\to a$ 的是环境，控制器无法要求它配合。因此存在安全路径并不意味着存在安全策略。另一方面，若事先给定控制器 $\sigma (s)=e$，环境可产生 $s\to e\to f\to b$；这个控制器验证失败，仍不妨碍综合找到另一个成功的控制器。

八状态例子：一次能到达仍然会被删除 ​

下面是独立于上面六状态安全图的 Büchi 图。令 $F=\{g,f\}$，完整的八点十三边为：

逐轮在剩余子图上重新计算，得到：

首轮 $s$ 能选 $s\to f$ 到达目标，$r$ 的两种选择也都能到目标，所以它们暂时位于 $Y_0$。但 $f$ 由环境控制，可选 $f\to t$，以后永不到目标；删除 $f,t$ 后，$s$ 只剩非目标自环，$r$ 能被环境送到 $s$，第二轮便一起删除。

最终吸引秩为 $r(g)=0$、$r(v)=r(p)=1$、$r(u)=2$。控制器选择 $g\to u,v\to g,p\to g$；环境在 $u$ 不论选 $g$ 还是 $v$，都会很快回到 $g$。失败反策略为 $f\to t,r\to s$：控制器在 $s$ 若永远自环就从不访问目标；若选择 $s\to f$，只得到一次目标访问，再进入 $t$。这里 $s\to f$ 正是从第二个删除层跳到第一个删除层。

若只要求待在安全集 $\{s\}$，$s\to s$ 已是成功控制器；但若目标集不含 $s$，同一自环绝不满足 Büchi 条件。安全闭包保证不出错，反复到达还需要每次离开目标后的进度证书。

适用的模型范围 ​

总后继假设保证每次行动后还能继续执行，也排除了死端上全称条件的真空成立问题。如果允许死端，必须先约定无法行动的一方是否输、有限执行是否安全，或明确补自环；不同约定可能改变获胜区域。

这里处理完整观测、轮流行动的安全目标与单个 Büchi 目标。部分观测、同时行动、随机转移、多个响应义务等需要另行定义；不能把安全算法直接用于活性，也不能仅因两者都有位置策略就省去各自的正确性证明。

从全图扫描到线性队列算法 ​

直接逐轮扫描全部边计算 $W_{i+1}$，最多进行 $O(|V|)$ 轮，每轮用 $O(|V|+|E|)$ 时间。在每个顶点都有后继的显式图上 $|E|\ge |V|$，故总时间为 $O(|V||E|)$。失败集合的增长方向允许进一步避免反复扫描。

预先建立每个顶点的反向邻接表 $\mathrm{Pred}(u)$。令每个控制器顶点的计数器 $\mathrm{remaining}(v)=|\mathrm{Succ}(v)|$。把全部坏状态标为失败，赋秩零，放入先进先出队列；其余状态未标记。重复以下步骤，直到队列为空：

1. 弹出 $u$，依次处理每条入边 $v\to u$；若 $v$ 已标记失败，跳过它。
2. 若 $v\in V_E$，立即标记 $v$，记录反策略边 $v\to u$，赋 $r(v)=r(u)+1$，并将 $v$ 入队。
3. 若 $v\in V_C$，将 $\mathrm{remaining}(v)$ 减一。减到零时，标记 $v$，赋 $r(v)=r(u)+1$，并将 $v$ 入队。

对尚未标记的控制器顶点，计数器始终等于其尚未被弹出处理的后继数；这里的“尚未处理”包括已经入队但还没弹出的后继。每条边只在其目标弹出时扣一次，因此计数归零恰好表示所有后继都已有失败证书。环境顶点在第一次遇到失败后继时就得到所需的存在性见证。标记时即禁止重复入队，保证每个顶点只处理一次。

先进先出队列按非递减秩弹出：初始队列全是零；处理秩 $k$ 的顶点时只会新增秩 $k+1$ 的顶点，且把它们放在队尾。因此环境顶点第一次见到的是其失败后继的最小秩；控制器计数归零时处理的是其后继的最大秩。这恰好实现层数递推

所以队列给出的就是逐轮集合中的首次加入秩，而非任意编号。终止时未标记的环境顶点没有失败后继，未标记的控制器顶点至少还有一个未标记后继；这些顶点构成安全闭包。标记顶点则都有下降证书，故算法的输出与上面证明的 $W,L$ 完全一致。最后扫描获胜控制器顶点的出边，为各顶点选一个仍在 $W$ 的后继，即得到控制策略。

建立反向邻接表、处理队列与提取策略合计耗时 $O(|V|+|E|)$，空间也是 $O(|V|+|E|)$。这个尺度针对已经展开的显式图；若图由布尔变量或程序紧凑表示，显式状态数可能随描述长度指数增长。

Büchi 算法的成本与证书 ​

一个吸引域可用上面的反向邻接表和计数器计算，只需交换玩家角色并把目标初始化为零层。在每轮重建剩余子图后，两次吸引计算都是 $O(|V|+|E|)$；至多 $|V|$ 次删除，故总时间为 $O(|V||E|)$，这是总后继显式图下的直接上界。按轮释放工作数组，只为每个顶点保存其删除轮次、局部秩和策略边，空间为 $O(|V|+|E|)$。这个实现界没有声称是最优算法。

独立检查者可重放各轮集合，核验吸引层的存在/全称前驱条件；最终侧检查闭包及非目标秩下降，删除侧检查进入更早层或在本层下降、零层避开 $F$。因此输出包括能支撑无限行为论证的有限证书，而不只是一个获胜顶点列表。

综合输出的是可控不变式 ​

一个集合 $J\subseteq S$ 若满足 $J\subseteq \mathrm{CPre}(J)$，便是可控不变集：控制器在自己的顶点有保留安全的选择，环境的全部选择都不能离开它。任意这样的 $J$ 都包含于 $W$：从 $J\subseteq W_0$ 出发，若 $J\subseteq W_i$，则 $J\subseteq S\cap \mathrm{CPre}(J)\subseteq W_{i+1}$。所以 $W$ 也是最大的可控不变集。

普通归纳不变式公理库不变式与归纳不变式Invariant · Inductive invariant · Strengthened invariant区分所有可达状态上成立的性质与由初始性和一步闭包直接证明的归纳不变式。要求对系统全部转移封闭，可控不变集则只需对被选择的控制器边及全部环境边封闭。在例子中，$W$ 允许控制器原本有一条 $s\to e$ 的出界边，因为综合策略不选它。固定获胜策略后，删去未被选择的控制器边，保留所有环境边，此时 $W$ 就成为所得转移系统的普通归纳不变式。

模型检查公理库模型检查问题Model checking problem · Model checking给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。检查给定控制器是否满足 $\mathrm{\forall }\tau :\mathrm{Safe}(v,\sigma ,\tau )$；综合则求解 $\mathrm{\exists }\sigma \mathrm{\forall }\tau :\mathrm{Safe}(v,\sigma ,\tau )$，并输出这个 $\sigma$。给定允许初态集合 $I$，可实现性等价于 $I\subseteq W$；否则任取 $I\cap L$ 中的初态，下降秩和环境反策略就给出不可实现证书。两类输出都可独立检查：获胜侧检查闭包，失败侧检查坏状态和严格下降的边条件。