Synthesizing Permissive Winning Strategy Templates for Parity Games

Abstract

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.