Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Synthesizing Permissive Winning Strategy Templates for Parity Games

Ashwani Anand, Satya Prakash Nayak, Anne-Kathrin Schmuck

TL;DR

The paper tackles the synthesis of permissive winning strategies for two-player $\omega$-regular parity games, with a focus on enabling incremental adaptation and fault-tolerant control in CPS. It introduces strategy templates that decompose winning behavior into safety, live-group, and co-live components, allowing a compact, adaptable representation of many winning strategies. The authors provide algorithms to construct these templates for safety, Büchi, co-Büchi, and parity objectives, with complexity matching standard game solvers and ensuring conflict-free templates for straightforward strategy extraction. Empirical evaluation with the PeSTel prototype demonstrates strong performance on generalized parity benchmarks, particularly for incremental objectives, and shows practical local handling of edge failures in CPS contexts, underscoring the approach’s scalability and applicability to real-world systems.

Abstract

We present a novel method to compute \emph{permissive winning strategies} in two-player games over finite graphs with $ ω$-regular winning conditions. Given a game graph $G$ and a parity winning condition $Φ$, we compute a \emph{winning strategy template} $Ψ$ that collects an infinite number of winning strategies for objective $Φ$ 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} $ω$-regular objectives $Φ'$, 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.

Synthesizing Permissive Winning Strategy Templates for Parity Games

TL;DR

The paper tackles the synthesis of permissive winning strategies for two-player -regular parity games, with a focus on enabling incremental adaptation and fault-tolerant control in CPS. It introduces strategy templates that decompose winning behavior into safety, live-group, and co-live components, allowing a compact, adaptable representation of many winning strategies. The authors provide algorithms to construct these templates for safety, Büchi, co-Büchi, and parity objectives, with complexity matching standard game solvers and ensuring conflict-free templates for straightforward strategy extraction. Empirical evaluation with the PeSTel prototype demonstrates strong performance on generalized parity benchmarks, particularly for incremental objectives, and shows practical local handling of edge failures in CPS contexts, underscoring the approach’s scalability and applicability to real-world systems.

Abstract

We present a novel method to compute \emph{permissive winning strategies} in two-player games over finite graphs with -regular winning conditions. Given a game graph and a parity winning condition , we compute a \emph{winning strategy template} that collects an infinite number of winning strategies for objective 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} -regular objectives , 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.
Paper Structure (5 sections, 1 theorem, 3 equations, 2 figures)

This paper contains 5 sections, 1 theorem, 3 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Computation of Winning Strategy Templates
  4. Safety Templates
  5. Live-Group Templates

Key Result

theorem \@thmcountertheorem

Let $\mathcal{G}=(G,\mathbf{G} U)$ be a safety game with winning region $\mathcal{W}_0$ and $S = \{ {(u} ,{v)\in E\mid \left(u\in V^0\cap \mathcal W_0\right) \wedge \left(v \notin \mathcal W_0\right)} \}$. Then is a winning strategy template for the game $\mathcal{G}$ which is also maximally permissive.

Figures (2)

  • Figure 1: Experimental results over 1400 generalized parity games comparing the performance of our tool PeSTel against the state-of-the-art generalized parity solver GenZielchatterjee2007:generalizedparitygames. Data points give the average execution time (in ms) over all instances with the same number of parity objectives. Left: all objectives are given upfront. Right: objectives are added one-by-one. See \ref{['sec:experiments']} for more details on those experiments.
  • Figure 2: A two-player game graph with $\text{Player}~1$ (squares) and $\text{Player}~0$ (circles) vertices, different winning conditions $\Phi_i$, and corresponding winning strategy templates $\Psi_i$.

Theorems & Definitions (1)

  • theorem \@thmcountertheorem: bernet2002:permissiveStrategies