2025-11-23T10:46:16.032830

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

Phalakarn, Pruekprasert, Hasuo

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.

academic

確率的パリティゲームのほぼ確実および正の勝利のための戦略テンプレート：許容的かつ弾性的な制御に向けて

基本情報

論文ID: 2409.08607
タイトル: Strategy Templates for Almost-Sure and Positive Winning of Stochastic Parity Games towards Permissive and Resilient Control
著者: Kittiphon Phalakarn, Sasinee Pruekprasert, Ichiro Hasuo
分類: eess.SY cs.LO cs.SY
発表時期: 2024年9月 (arXiv v2: 2025年10月16日)
論文リンク: https://arxiv.org/abs/2409.08607

要旨

確率的ゲームは多くの応用において基礎的な役割を果たしており、特にサイバーフィジカルシステム(CPS)の制御において、コントローラと環境がゲーム参加者としてモデル化される。従来のアルゴリズムは通常、コントローラを開発するための単一の勝利戦略を決定することを目的としている。しかし、CPS制御およびその他の領域では、追加の制約が発生した場合にシステムが適応でき、実行時の変化に対して弾性を保つことができるため、許容的なコントローラが重要である。本研究は、戦略テンプレートの概念を決定性ゲームから確率的ゲームに一般化し、これらのテンプレートは無限数の勝利戦略を捕捉でき、システム変化に対する効率的な戦略適応を可能にする。我々は2つの勝利基準(ほぼ確実な勝利と正の確率での勝利)および5つの勝利目標(安全性、到達可能性、Büchi、co-Büchi、パリティ)に焦点を当てる。

研究背景と動機

問題背景

従来の方法の限界: 従来のゲーム求解アルゴリズムは通常、単一の勝利戦略のみを探索し、戦略の許容性(permissiveness)を考慮しない
実際の応用要件: サイバーフィジカルシステム制御では、追加の制約と実行時の変化に適応するための許容的なコントローラが必要である
弾性制御の要件: システムは障害または環境変化に直面した場合、堅牢性を維持する必要がある

研究動機

既存の戦略テンプレート概念は決定性ゲームにのみ適用可能であり、確率的ゲームへの対応が不足している
無限数の勝利戦略を捕捉でき、戦略の迅速な適応をサポートするフレームワークが必要である
CPS制御などの実際の応用では、許容性と弾性が重要な要件である

核心的貢献

ほぼ確実な勝利戦略テンプレートアルゴリズム: 5つの勝利目標(安全性、到達可能性、Büchi、co-Büchi、パリティ)に対するほぼ確実な勝利戦略テンプレート構築アルゴリズムを提案
正の確率での勝利戦略テンプレート: 正の確率での勝利基準下での戦略テンプレート構築および組合せアルゴリズムを開発
戦略テンプレート比較フレームワーク: 許容性とサイズに基づくテンプレート比較の議論を提供
戦略抽出方法: 与えられたテンプレートから勝利戦略を抽出する新しい方法を提案し、勝利目標と許容性のバランスを取る

方法の詳細

タスク定義

確率的ゲームの定義: G = (V, E, (V□, V○, V△))、ここで：

Vは頂点集合、Eは辺集合
V□、V○、V△はそれぞれEvenプレイヤー、Oddプレイヤー、Randomプレイヤーの頂点を表す
「2.5」プレイヤーゲームと呼ばれ、2つの主要プレイヤーと1つのランダムプレイヤーを含む

戦略テンプレートの定義: T = (P, L, C)、ここで：

P ⊆ E□は禁止辺集合
L ⊆ 2^E□はアクティブグループ集合
C ⊆ E□は共アクティブ辺集合

モデルアーキテクチャ

1. ほぼ確実な勝利戦略テンプレート構築

安全性目標(G X):

SafetyTemplate(G, X):
1. W□ ← νY.(X ∩ (Pre□(Y) ∪ Pre(Y)))
2. P ← Edges□(W□, V \ W□)
3. return (P, ∅, ∅)

到達可能性目標(F X):

ReachabilityTemplate(G, X):
1. A ← Attr'(X)
2. W□ ← Attr'□(A)
3. P ← Edges□(W□, V \ W□)
4. C ← Edges□(W□ \ A, W□ \ A)
5. return (P, ∅, C)

Büchi目標(GF X): LiveGroups関数を通じてアクティブグループを構築し、パスが目標集合を無限回訪問することを保証する。

パリティ目標:

確率的ゲームを決定性ゲームに約減(Reduceアルゴリズムを使用)
決定性ゲームの戦略テンプレートを構築
確率的ゲームのテンプレートに変換

2. 正の確率での勝利戦略テンプレート構築

PositiveTemplate(G, φ):
1. W□、W○およびほぼ確実な勝利テンプレートT^(a)を計算
2. W? ← V \ (W□ ∪ W○)
3. P^(p) ← P^(a) ∪ Edges□(W?, W○)
4. C^(p) ← C^(a) ∪ Edges□(W?, W?)
5. return T^(p) = (P^(p), L^(p), C^(p))