Winning Strategy Templates for Stochastic Parity Games towards Permissive and Resilient Control
Stochastic games play an important role for many purposes such as the control of cyber-physical systems (CPS), where the controller and the environment are modeled as players. Conventional algorithms typically solve the game for a single winning strategy in order to develop a controller. However, in applications such as CPS control, permissive controllers are crucial as they allow the controlled system to adapt if additional constraints need to be imposed and also remain resilient to system changes at runtime. In this work, we generalize the concept of permissive winning strategy templates, introduced by Anand et al. at TACAS and CAV 2023 for deterministic games, to encompass stochastic games. These templates represent an infinite number of winning strategies and can adapt strategies to system changes efficiently. We focus on five key winning objectives -- safety, reachability, B\"uchi, co-B\"uchi, and parity -- and present algorithms to construct templates for each objective. In addition, we propose a novel method to extract a winning strategy from a template and provide discussions on template comparison.
Code (0)
등록된 구현이 없습니다.
Methods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Predicting Winning Regions in Parity Games via Graph Neural Networks (Extended Abstract)
Solving parity games is a major building block for numerous applications in reactive program verification and synthesis. While they can be solved efficiently in practice, no known approach has a polynomial worst-case run…
Symbolic Control for Stochastic Systems via Finite Parity Games
We consider the problem of computing the maximal probability of satisfying an omega-regular specification for stochastic nonlinear systems evolving in discrete time. The problem reduces, after automata-theoretic construc…
Guessing Winning Policies in LTL Synthesis by Semantic Learning
We provide a learning-based technique for guessing a winning strategy in a parity game originating from an LTL synthesis problem. A cheaply obtained guess can be useful in several applications. Not only can the guessed s…
Evolving winning strategies for Nim-like games
An evolutionary approach for computing the winning strategy for Nim-like games is proposed in this paper. The winning strategy is computed by using the Multi Expression Programming (MEP) technique - a fast and efficient …
Solving Random Parity Games in Polynomial Time
We consider the problem of solving random parity games. We prove that parity games exibit a phase transition threshold above $d_P$, so that when the degree of the graph that defines the game has a degree $d > d_P$ then t…