Strategy Templates for Almost-Sure and Positive Winning of Stochastic Parity Games towards Permissive and Resilient Control

TL;DR

This paper extends the concept of strategy templates to stochastic games, enabling the creation of adaptable, permissive controllers for cyber-physical systems that can handle various winning conditions.

Contribution

It introduces algorithms for constructing and extracting strategies from templates in stochastic games, broadening the applicability of permissive controllers to more complex scenarios.

Findings

Algorithms for template construction for multiple winning criteria

Method for extracting strategies from templates

Enhanced adaptability and resilience in control strategies

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\"uchi, co-B\"uchi, 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.