Strategy Templates for Almost-Sure and Positive Winning of Stochastic Parity Games towards Permissive and Resilient Control
Kittiphon Phalakarn, Sasinee Pruekprasert, Ichiro Hasuo
TL;DR
The paper addresses the need for permissive, resilient controllers in stochastic settings by extending strategy templates from deterministic two-player games to stochastic parity games. It develops algorithms to construct almost-sure and positive winning templates for five SG objectives (safety, reachability, Büchi, co-Büchi, parity), and introduces composition and strategy-extraction techniques, alongside a formal analysis of template permissiveness and size. The work leverages LTL specifications, set-operator tools, and gadget-based reductions to deterministic parity games, enabling modular, incremental synthesis and runtime adaptation. It also introduces positive winning templates and a framework for composing templates, providing practical pathways for fault tolerance and dynamic constraint handling in CPS. Overall, the approach aims to make strategy synthesis in stochastic environments more scalable, modular, and robust for real-world control applications.
Abstract
Stochastic games are fundamental in various applications, including the control of cyber-physical systems (CPS), where both controller and environment are modeled as players. Traditional algorithms typically aim to determine a single winning strategy to develop a controller. However, in CPS control and other domains, permissive controllers are essential, as they enable the system to adapt when additional constraints arise and remain resilient to runtime changes. This work generalizes the concept of (permissive winning) strategy templates, originally introduced by Anand et al. at TACAS and CAV 2023 for deterministic games, to incorporate stochastic games. These templates capture an infinite number of winning strategies, allowing for efficient strategy adaptation to system changes. We focus on two winning criteria (almost-sure and positive winning) and five winning objectives (safety, reachability, Büchi, co-Büchi, and parity). Our contributions include algorithms for constructing templates for each winning criterion and objective and a novel approach for extracting a winning strategy from a given template. Discussions on comparisons between templates and between strategy extraction methods are provided.