“对有限、完整信息、轮流行动且每顶点至少有一个后继的奇偶博弈，存在不交分区”
形式陈述
奇偶博弈将奇偶接受条件放到双方轮流选择的有向图上。这里选择允许自环、以端点关系区分后继的有限变体：顶点集
在v∈Vᵢ时由玩家i选下一个顶点。一次play为无限路径v₀v₁…；min-even规定最小无限出现优先级为偶数时Even胜，否则Odd胜。总后继假设保证极大play不会因死路提前停止。
策略σᵢ可根据整段有限历史选合法后继。Even从v获胜，含义为
Odd获胜则反向量化并要求奇数。若策略只依赖当前顶点，称位置策略。本页先允许历史策略；有限奇偶博弈确实可以只用位置策略，是需要另外证明的定理，不能偷偷放入获胜定义。
直觉
自动机可以凭“存在一条好运行”接受输入；对抗系统还得考虑谁控制那些边。一个好循环上若有环境顶点，环境可能选择另一条边离开，或永远留在更坏的子环。
安全与Büchi博弈分别关注不碰坏状态、反复到达一个目标。多优先级奇偶条件允许不同层次的长期要求相互覆盖：反复出现0能压过1，但在0只出现有限次时，1又能压过2。求解需要保留这份优先级顺序。
例子与边界
六顶点完整后继表
下面给出全部顶点和边，表外没有其他选择。
| 顶点 | 行动者 | 优先级 | 后继 |
|---|---|---|---|
| s | Even | 2 | a,c |
| a | Odd | 1 | a,b |
| b | Even | 0 | a |
| c | Odd | 2 | c,d |
| d | Even | 1 | b,e |
| e | Odd | 2 | e |
存在接受循环a→b→a，其优先级集{1,0}的最小值是0。但从a，Odd可以固定选择a→a，使最小无限优先级为1。从b也只能先走到a；即使初态出现一次0，后面a永留1仍然失败。因此a、b属于Odd获胜区。
Even可以固定选择s→c、d→e。由c出发，Odd若永远选择c→c，长期优先级为2，Even胜；若某次选c→d，Even立即去e，此后只见2，仍胜。d上的1只出现一次。于是s、c、d、e都由Even获胜。
反过来，若Even在s选择a，或在d选择b，Odd的a自环就能获胜。这不仅给出一条成功路径，也把同一策略下环境的全部长期选择分成了两类。
“偶数出现无限次”为什么仍不够
在循环优先级{1,2}中，偶数2无限出现，但更小的1也无限出现，结果是Odd胜。若把所有偶数顶点并为一个Büchi目标，这条循环会被错误接受。
本例中c的2自环却确实接受，虽然它从不访问优先级0。把“必须反复访问最小偶色0”作为替代条件，也会错误删掉c的合法策略。奇偶目标同时需要访问频率与数值顺序。
检查固定位置策略仍要看所有循环
固定Even位置策略以后，只删除Even未选择的边，Odd的所有边都保留。可借强连通分量分析剩余图，但不能只看每个大SCC的最小优先级，也不能只检查底部SCC。
一个含0与1的大SCC里可能藏着1自环；Odd可以永远绕这个小环而不访问0。一般判据是：从指定初态可达的每一个正长度循环，其最小优先级都为偶数。若存在奇最小循环，Odd能沿一条到达路径和该循环反复选择，构成反例；反之，有限图中的失败无限路径会在其最小无限奇色附近给出这样的回返循环。
要真正用 SCC 完成这个判据，先在固定策略后的全图中求初态可达集
必须先求全图可达集，再删除低优先级顶点：到坏循环的有限前缀可以经过更小的偶色，它不改变该循环的长期结果。这个逐奇色 SCC 检查保留了大分量内部的坏子环，不是只看原图每个 SCC 的最低色。
推论与应用
位置确定性将获胜定义中的任意历史策略压缩成每顶点一个选择，并给双方完整获胜分区。这使控制器与反策略都能作为有限对象交付。
Zielonka算法通过吸引域与较小子博弈计算分区；小进展度量则用按优先级截断的有限元组构造局部证书。二者都实现本页有限、总后继、min-even 图上的获胜区计算，但维护的信息不同。Zielonka 同时返回双方位置策略；小进展度量直接提取 Even 策略，若还要 Odd 策略，须按该算法页交换双方与优先级后再运行，或另作反策略提取。
应用于反应式综合时，还要说明环境先给输入还是控制器先给输出。改变顶点归属或回合顺序，就改变可用信息与策略能力，不能只保留同一张无归属图来比较实现性。
参考资料
- Sebastian Muskalla, Games with Perfect Information，§6：完整信息奇偶博弈、历史策略、有限前缀无关；本页采用min-even
- Marcin Jurdziński, “Small Progress Measures for Solving Parity Games”, STACS, 2000，§2：min-parity图、固定策略与循环判据