We present a novel method to compute \emph{permissive winning strategies} in two-player games over finite graphs with $ \omega $-regular winning conditions. Given a game graph $G$ and a parity winning condition $\Phi$, we compute a \emph{winning strategy template} $\Psi$ that collects an infinite number of winning strategies for objective $\Phi$ in a concise data structure. We use this new representation of sets of winning strategies to tackle two problems arising from applications of two-player games in the context of cyber-physical system design -- (i) \emph{incremental synthesis}, i.e., adapting strategies to newly arriving, \emph{additional} $\omega$-regular objectives $\Phi'$, and (ii) \emph{fault-tolerant control}, i.e., adapting strategies to the occasional or persistent unavailability of actuators. The main features of our strategy templates -- which we utilize for solving these challenges -- are their easy computability, adaptability, and compositionality. For \emph{incremental synthesis}, we empirically show on a large set of benchmarks that our technique vastly outperforms existing approaches if the number of added specifications increases. While our method is not complete, our prototype implementation returns the full winning region in all 1400 benchmark instances, i.e., handling a large problem class efficiently in practice.

翻译：我们提出了一种新颖的方法，用于计算有限图上的二玩家游戏中具有 $ \omega $-正则获胜条件的*宽松获胜策略*。给定一个游戏图 $G$ 和一个 Parity 获胜条件 $\Phi$，我们计算一个*获胜策略模板* $\Psi$，该模板以简洁的数据结构收集目标 $\Phi$ 的无限多个获胜策略。我们利用这种新的获胜策略集合表示法，来解决在信息物理系统设计背景下由二玩家游戏应用所引发的两个问题——(i) *增量综合*，即调整策略以适应新到达的、*额外的* $\omega$-正则目标 $\Phi'$，以及 (ii) *容错控制*，即调整策略以适应执行器偶尔或持续不可用的情况。我们的策略模板的主要特点——我们利用这些特点来解决上述挑战——在于其易计算性、适应性和组合性。对于*增量综合*，我们在大量基准测试上通过实验表明，当添加的规约数量增加时，我们的技术远远优于现有方法。虽然我们的方法并不完备，但我们的原型实现在所有 1400 个基准测试实例中均返回了完整的获胜区域，即在实践中高效处理了一大类问题。