实时自动机、Kleene代数与奇偶游戏求解算法

### 实时自动机、Kleene代数与奇偶游戏求解算法 #### 实时自动机与Kleene代数 在实时自动机和实数集的Kleene代数相关研究中，定义了一些重要的集合。设 $T_0$ 和 $T_f$ 如下： - $T_0 = \{[S, S′, a] \in Q | \varnothing\neq S \subseteq Q_0, a \in V \} \cup\{[\varnothing, \varnothing, a] | \forall q \in Q_0, \lambda(q) \neq a\}$ - $T_f = \{[S, S′, a] \in Q | S′ \cap F \neq \varnothing, a \in V \}$ 有定理表明 $T Rec(V )$ 在补运算下是封闭的。证明过程基于构造的自动机 $C$，其中每个信号都与一个从 $T_0$ 开始的唯一运行相关联。接受 $Sig(S) \setminus L(B)$ 的自动机是通过对 $C$ 的终态集取补得到的。 此外，实时自动机（RTAs）存在一种范式，即每个RTA都等价于这样一个RTA：由停滞转换组成的任何回路都是在标记为点区间的状态处的循环，停滞步骤只能从循环状态开始，并且任何不同停滞步骤的链最多有两个转换。 下面总结相关要点： | 要点 | 描述 | | ---- | ---- | | $T_0$ 定义 | 由满足特定条件的三元组构成，包含非空子集和特定标记情况 | | $T_f$ 定义 | 由终态集与特定集合有交集的三元组构成 | | $T Rec(V )$ 封闭性 | 在补运算下封闭，通过自动机终态集取补证明 | | RTA范式 | 回路、停滞步骤有特定限制 | #### 奇偶游戏概述 奇偶游戏是由两名玩家（玩家 $\square$ 和玩家 $\bigcirc$）在一个为顶点分配整数优先级的图上进行的无限路径形成游戏。游戏规则如下： - **游戏图**：一个奇偶图 $G = (V, E, p)$ 由有向图 $(V, E)$ 和优先级函数 $p : V \to [d]$ 组成，其中 $d \in \mathbb{N}$。奇偶游戏 $\Gamma = (V, E, p, (V_{\square}, V_{\bigcirc}))$ 由奇偶图 $G$ 和顶点集 $V$ 的划分 $(V_{\square}, V_{\bigcirc})$ 构成。为方便起见，假设所有游戏图的每个顶点至少有一条出边，且本文只考虑有限游戏图。 - **游戏过程**：两名玩家通过沿边移动令牌在游戏图中形成无限路径。若令牌在 $V_{\square}$ 中的顶点上，玩家 $\square$ 移动令牌；若在 $V_{\bigcirc}$ 中的顶点上，玩家 $\bigcirc$ 移动令牌。最终形成的无限路径 $\pi = \langle v_1, v_2, v_3, \cdots \rangle$ 称为一次游戏。 - **胜负判定**：设 $Inf(\pi)$ 表示在 $p(v_1), p(v_2), p(v_3), \cdots$ 中无限次出现的优先级集合。若 $\min(Inf(\pi))$ 为偶数，则玩家 $\square$ 获胜；否则玩家 $\bigcirc$ 获胜。 以下是奇偶游戏的流程： ```mermaid graph LR A[开始游戏] --> B[放置令牌在初始顶点] B --> C{令牌在 V_□ 顶点?} C -- 是 --> D[玩家 □ 移动令牌] C -- 否 --> E[玩家 ○ 移动令牌] D --> F{是否继续游戏?} E --> F F -- 是 --> C F -- 否 --> G[检查 Inf(π) 最小优先级奇偶性] G -- 偶数 --> H[玩家 □ 获胜] G -- 奇数 --> I[玩家 ○ 获胜] ``` #### 策略相关定义 - **策略