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üchi, co-Büchi, 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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Winning Strategy Templates for Stochastic Parity Games Towards Permissive and Resilient Control

  • Kittiphon Phalakarn,
  • Sasinee Pruekprasert,
  • Ichiro Hasuo

摘要

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üchi, co-Büchi, 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.