问题定义
对于由 环境（可以看作是整个场景中不可控制的部分） 和 系统（一般来说就是你希望生成的程序）组成的双人博弈的场景，我们将其抽象为 8 元组：
- $\mathcal{X}$：由环境控制的变量集合
- $\mathcal{Y}$：由系统控制的变量集合
- $\mathcal{V} = \mathcal{X} \cup \mathcal{Y}$
- $\theta_e$：关于环境的，初始成立的断言，由 $\mathcal{X}$ 中的变量组成
- $\theta_s$：关于系统的，初始成立的断言，由 $\mathcal{Y}$ 中的变量组成
- $\rho_e: (\Sigma_V, \Sigma_X) \rightarrow \text{bool}$：用于选择 环境 的下一个动作的断言函数， 其中 第一个参数 输入当前 所有（环境与系统的）变量的取值， 第二个参数 输入环境可能采取的动作， 若 $\rho_e(s, x) = \text{true}$，说明 在所有当前变量的值为 $s$ 的情况下，环境可以采取动作 $x$
- $\rho_s: (\Sigma_V, \Sigma_X, \Sigma_Y) \rightarrow \text{bool}$：用于选择 系统 的下一个动作的断言函数， 其中 第一个参数 输入当前 所有（环境与系统的）变量的取值， 第二个参数 输入 环境这时采取的动作， 第三个参数 输入 系统可能采取的动作， 若 $\rho_s(s, x, y) = \text{true}$，说明 在所有当前变量的值为 $s$ 且 环境采取动作 $x$ 的情况下，系统可以采取动作 $y$
- $\varphi$：一个 LTL 公式，定义了（对于系统来说的）胜利条件
算法的目标是，找到一个函数 $f: (M, \Sigma_V, \Sigma_X) \rightarrow (M, \Sigma_X)$， 使得：
- 若 $\rho_e(s,s_X) = \text{true}$，那么 $\rho_s(s,s_X,\text{snd}(f(m,s,s_X))) = \text{true}$，
- 从某个状态 $s$ 出发时，所有符合 $f$ 的 对局（状态序列）都是系统胜利（$(s_0, s_1, \cdots) \models \varphi$）的。
其中的 $M$ 是一个记忆空间，包含初始值 $m_0$。
这篇论文解决的问题是 Generalized Reactivity(1) 博弈，即 $\varphi$ 形如 $$ \varphi = \bigwedge_{i=1}^{m} \mathbf{G}(\mathbf{F}(J_i^e)) \rightarrow \bigwedge_{j=1}^{n} \mathbf{G}(\mathbf{F}(J_j^s)) $$ 的情况，其中 $J_i^e$ 和 $J_j^s$ 是布尔函数，分别表示 环境 和 系统 要保证/实现的 liveness 条件。
算法
必须的概念
μ-calculus
In theoretical computer science, the modal μ-calculus (Lμ, sometimes just μ-calculus, although this can have a more general meaning) is an extension of propositional modal logic (with many modalities) by adding the least fixed point operator μ and the greatest fixed point operator ν, thus a fixed-point logic. - Modal μ-calculus, Wikipedia
简单来说就是往一阶 propositional logic 中添加了 定点运算符 $\mu$ 和 $\nu$ 和 扩展运算符 $[-]$ 和 $\langle - \rangle$。
语法如下：
$$ \varphi ::= v \mid \neg \varphi \mid X \mid \varphi \vee \varphi \mid \varphi \wedge \varphi \mid [\varphi] \mid \langle \varphi \rangle \mid \mu X \varphi \mid \nu X \varphi $$
一个公式 $\phi$ 被解释为 $G$ 中状态集合 $Σ$ 中使 $\phi$ 成立的状态集合，记为 $[[\phi]]_G^E$，其中 $G$ 是游戏结构，$E: \text{Map}\langle\text{Var}, 2 ^ Σ\rangle$ 将每个关系变量1映射到一组状态。
除了常见 propositional logic 的符号以外几个运算符的（指称）语义：
-
$[[X]]_G^E = E[X]$
-
$[[ [\varphi] ]]_G^E$ 表示，系统可以强迫 $[[\varphi]]_G^E$ 成立的状态集合。
-
$[[ \langle \varphi \rangle ]]_G^E$ 表示，环境可以强迫 $[[\varphi]]_G^E$ 成立的状态集合。
-
$ [[ \mu X \varphi ]]_G^E $ 表示，在有限步之内能够使得 $\varphi$ 成立的状态集合
$[[ \mu X \varphi ]]_G^E = \bigcup_{i} S_i $ where $S_0 = \emptyset$ and $S_{i+1} = [[ \varphi ]]_G^{E[X \leftarrow S_i]}$
-
$ [[ \nu X \varphi ]]_G^E $ 表示，从现在开始能够一直使得 $\varphi$ 成立的状态集合。
$[[ \nu X \varphi ]]_G^E = \bigcap_{i} S_i $ where $S_0 = \Sigma$ and $S_{i+1} = [[ \varphi ]]_G^{E[X \leftarrow S_i]}$
要求解的公式
最终要求解的公式是：
$$ \varphi_{gr} = \nu \begin{bmatrix} Z_1 \\ Z_2 \\ \vdots \\ Z_n \end{bmatrix} \begin{bmatrix} \mu Y (\bigvee_{i=1}^{m} \nu X ((J_1^s \wedge [Z_2]) \vee [Y] \vee (\neg J_i^e \wedge [X]))) \\ \mu Y (\bigvee_{i=1}^{m} \nu X ((J_2^s \wedge [Z_3]) \vee [Y] \vee (\neg J_i^e \wedge [X]))) \\ \vdots \\ \mu Y (\bigvee_{i=1}^{m} \nu X ((J_n^s \wedge [Z_1]) \vee [Y] \vee (\neg J_i^e \wedge [X]))) \end{bmatrix} $$
最外层的 $\nu Z$ 和内部的 $Z_{i+1 \text{mod} n}$ 表示，如果系统满足了当前的 $J_i$，则可以转而去尝试满足下一个 $J_{i+1}$。
中间的 $\mu Y$ 保证了后面的 $\bigvee_{i=1}^{m} \nu X ((J_1^s \wedge [Z_2]) \vee [Y] \vee (\neg J_i^e \wedge [X]))$ 部分会在有限步内结束。
最里面的 $\nu X$ 和内部的 $\neg J_i^e \wedge [X]$ 表示，若环境没有满足某个 $J^e$，则系统可以不前进。
求解
论文中给出了利用 BDD 求解的代码：
BDD calculate_win() {
BDD Z = TRUE;
// 外层 νZ 的 fixpoint 迭代
for (Fix fZ = new Fix(); fZ.advance(Z);) {
mem.clear();
// for each system goal （J^s_j）
for (int j = 1; j <= sys.numJ(); j++) {
BDD Y = FALSE;
// 中层 μY 的 fixpoint 迭代
for (Fix fY = new Fix(); fY.advance(Y);) {
// 构造起始集合：要么已经满足 J^s_j 并进入下一个阶段 Z_{j⊕1}，要么已在 Y 中
BDD start = sys.Ji(j).and(cox(Z)).or(cox(Y));
Y = FALSE;
for (int i = 1; i <= env.numJ(); i++) { // 遍历每个环境假设 J^e_i
BDD X = Z;
// 最内层 νX 的 fixpoint 迭代
for (Fix fX = new Fix(); fX.advance(X);) {
// 如果环境没有满足 J^e_i，系统可以“停在 X”；否则必须通过 start 推进
X = start.or(env.Ji(i).not().and(cox(X)));
}
// 存储第 j 个目标、第 i 个假设下的 X 集合
mem.addX(j, i, X);
// 把所有 X 累加进 Y，构建 μY
Y = Y.or(X);
}
// 存储 Y（表示目标 j 可在有限步内达成的状态集）
mem.addY(j, Y);
}
// 将最新的 Y 作为下一轮外层 Z 的输入（推进 νZ）
Z = Y;
}
}
return Z;
}
其中 cox(x) 是 $[x]$ 的实现。
提取策略
void build_symbolic_controller() {
ctrl = new FDS("symbolic_controller");
Zn = ctrl.newBDDDomain("Zn", 1, sys.numJ());
// 联合环境与系统的转移关系
BDD tr12 = sys.trans().and(env.trans());
// 当子目标 J^s_j 被满足，就将 Zn 轮换至下一个目标（j → j ⊕ 1）
for (int j = 1; j <= sys.numJ(); j++) {
BDD rho1 = (Zn.eq(j)) // 当前记忆状态是 j（正在处理第 j 个目标）
.and(Z) // 当前状态在 Z 中
.and(sys.Ji(j)) // 当前满足系统目标 J^s_j
.and(tr12) // 当前转移合法
.and(next(Z)) // 下一状态仍要在区域 Z 中
.and(next(Zn).eq((j % sys.numJ()) + 1)); // 下一状态将 Zn 切换到 j⊕1
// 将该转移加入控制器的转移关系
ctrl.disjunctTrans(rho1);
}
// 从当前状态 mY[j][r] 推进到更接近目标的状态 mY[j][r']，直到最终达成目标
for (int j = 1; j <= sys.numJ(); j++) {
BDD low = mem.Y(j, 1); // r=1 表示最接近达成目标的状态
for (int r = 2; r <= mem.maxr(j); r++) { // 从上层往下找
BDD rho2 = (Zn.eq(j)) // 当前是目标 j
.and(mem.Y(j, r)) // 当前距离目标还有 r 步
.and(low.not()) // 下一“层”不能是当前这一“层”（r′ < r）
.and(tr12) // 合法转移
.and(next(low)) // 下一状态进入更低“层”（r'）
.and(next(Zn).eq(j)); // Zn 不变，仍处于当前目标
low = low.or(mem.Y(j, r)); // 更新“已知的低层”集合
ctrl.disjunctTrans(rho2); // 加入控制器
}
}
// 如果环境违背假设 J^e_i，系统可以不推进
for (int j = 1; j <= sys.numJ(); j++) {
BDD low = FALSE;
for (int r = 2; r <= mem.maxr(j); r++) {
for (int i = 1; i <= env.numJ(); i++) {
BDD rho3 = (Zn.eq(j)) // 当前子目标 j
.and(mem.X(j, r, i)) // 当前在环境假设 i 的推进层 X
.and(low.not()) // 下一层需下降
.and(env.Ji(i).not()) // 环境违反假设 J^e_i
.and(tr12) // 转移合法
.and(next(mem.X(j, r, i))) // 下一状态继续在 X（即维持）
.and(next(Zn).eq(j)); // Zn 不变
low = low.or(mem.X(j, r, i)); // 更新低层状态集合
ctrl.disjunctTrans(rho3); // 加入转移
}
}
}
}
关系变量一般代表了一个需要求解的状态集合。