Synthesizing flexible winning strategies in uncertain games for better control
Towards Actionable Strategy Certificates in Stochastic Parity Games
Computer Science and Game Theory
Summary
Stochastic parity games involve making decisions in situations with both chance and opponents, aiming to meet complex goals. The authors introduce Actionable Strategy Certificates (ASCerts), which represent many possible ways to win without fixing a single strict strategy. These certificates help ensure strategies keep the system safe with a certain probability, making them more trustworthy. Their method allows strategies to be created, adapted, and used more efficiently, especially in uncertain and challenging environments. They show how this works through an example where strategies can adjust during operation.
stochastic parity gameswinning strategyquantitative objectivesActionable Strategy Certificatesstochastic invariantsalmost-sure winningruntime adaptationstrategy synthesisprobability safetygame theory
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.