Actionable certificates enable flexible winning strategies in uncertain games
Towards Actionable Strategy Certificates in Stochastic Parity Games
Computer Science and Game Theory
Summary
Winning in complex games with chance and decisions can be tough to guarantee. The authors create a new way to represent many possible winning strategies using small, clear certificates that prove safety with high probability. This approach allows easier strategy creation, adjustment, and use even during play in uncertain and competitive settings. They show how this method works on a real example and provide a basic software tool for it.
What this means in practice
- •For control engineers: Generate flexible control strategies for systems operating in uncertain, adversarial environments with guarantees on maintaining safety.
- •For software developers: Extract and adapt strategies at runtime for decision-making software facing unpredictable or competitive scenarios.
Authors
Christel Baier, Diane Cauquil, Calvin Chau, Sascha Klüppelholz, Anne-Kathrin Schmuck
Abstract
We propose a new approach for synthesizing large sets of winning strategies in stochastic parity games (2.5-player games) with quantitative objectives. Instead of computing a single, fully specified winning strategy, we introduce Actionable Strategy Certificates (ASCerts) as a local and permissive representation of a large class of system player winning strategies. To this end, we extend known certificates for stochastic invariants to the setting of games. Our certificates prove that synthesized strategies remain within a safe region of the game with probability at least $λ\in [0,1]$. As such, the certificates enhance the trustworthiness of synthesized strategies. The crux of our approach is to reinterpret and leverage the certificates as concise, local, and permissive representation of (possibly infinitely many) strategies. By carefully combining our certificates for stochastic invariants with strategy templates for almost-sure winning, we obtain a novel local representation of quantitatively winning strategies in stochastic parity games. This enables efficient synthesis, adaptation, and runtime strategy extraction, making ASCerts well suited for logical control in uncertain and adversarial environments. We provide a proof-of-concept implementation and demonstrate the potential of applying ASCerts in runtime adaptation on a case study.