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

Basic Information

• Paper ID: 2409.08607
• Title: Strategy Templates for Almost-Sure and Positive Winning of Stochastic Parity Games towards Permissive and Resilient Control
• Authors: Kittiphon Phalakarn, Sasinee Pruekprasert, Ichiro Hasuo
• Classification: eess.SY cs.LO cs.SY
• Publication Date: September 2024 (arXiv v2: October 16, 2025)
• Paper Link: https://arxiv.org/abs/2409.08607

Abstract

Stochastic games play a foundational role in diverse applications, particularly in cyber-physical systems (CPS) control, where controllers and environments are modeled as game participants. Traditional algorithms typically aim to determine a single winning strategy for controller development. However, in CPS control and other domains, permissive controllers are crucial as they enable system adaptation when additional constraints emerge and maintain resilience to runtime changes. This work generalizes the concept of strategy templates from deterministic games to stochastic games, enabling templates to capture infinitely many winning strategies and allow efficient strategy adaptation to system variations. We focus on two winning criteria (almost-sure winning and positive winning) and five winning objectives (safety, reachability, Büchi, co-Büchi, and parity).

Research Background and Motivation

Problem Background

1. Limitations of Traditional Approaches: Conventional game-solving algorithms typically seek only a single winning strategy without considering strategy permissiveness
2. Practical Application Requirements: In cyber-physical systems control, permissive controllers are needed to accommodate additional constraints and runtime variations
3. Resilience Control Requirements: Systems must maintain robustness when facing failures or environmental changes

Research Motivation

• Existing strategy template concepts apply only to deterministic games, lacking support for stochastic games
• A framework is needed that can capture infinitely many winning strategies to support rapid strategy adaptation
• In practical applications such as CPS control, permissiveness and resilience are critical requirements

Core Contributions

1. Almost-Sure Winning Strategy Template Algorithms: Proposes construction algorithms for almost-sure winning strategy templates across five winning objectives (safety, reachability, Büchi, co-Büchi, and parity)
2. Positive Winning Strategy Templates: Develops construction and composition algorithms for strategy templates under positive winning criteria
3. Strategy Template Comparison Framework: Provides template comparison discussions based on permissiveness and size
4. Strategy Extraction Methods: Proposes novel methods for extracting winning strategies from given templates, balancing winning objectives and permissiveness

Methodology Details

Task Definition

Stochastic Game Definition: Stochastic game G = (V, E, (V□, V○, V△)), where:

• V is the set of vertices, E is the set of edges
• V□, V○, V△ represent vertices controlled by Even player, Odd player, and Random player respectively
• Referred to as "2.5-player" games, containing two main players and one random player

Strategy Template Definition: T = (P, L, C), where:

• P ⊆ E□ is the set of disabled edges
• L ⊆ 2^E□ is the set of active groups
• C ⊆ E□ is the set of co-active edges

Model Architecture

1. Almost-Sure Winning Strategy Template Construction

Safety Objective (G X):

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

Reachability Objective (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 Objective (GF X): Constructs active groups via the LiveGroups function to ensure paths visit the target set infinitely often.

Parity Objective:

1. Reduces stochastic game to deterministic game (using Reduce algorithm)
2. Constructs strategy template for deterministic game
3. Converts template back to stochastic game template

2. Positive Winning Strategy Template Construction

PositiveTemplate(G, φ):
1. Compute W□, W○ and almost-sure winning template 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))

Technical Innovations

1. Extended Set Operations: Introduces new set operators considering the Random player, such as Pre△(X', X) and Attr'□(X)
2. Template Composition Algorithm: Proposes conflict detection mechanism with recomputation when template conflicts occur
3. Parameterized Strategy Extraction: Uses parameters α and β to balance permissiveness and goal achievement speed
4. Positive Winning Extension: First extension of strategy templates to positive winning criteria

Experimental Setup

Theoretical Verification

The paper primarily verifies algorithm correctness through theoretical proofs, including:

• Correctness theorems for various template construction algorithms
• Permissiveness theorems for strategy extraction methods
• Correctness proofs for template composition algorithms

Complexity Analysis

• Worst-case runtime of strategy construction algorithms matches standard algorithms
• Template composition and strategy extraction can be executed efficiently at runtime

Experimental Results

Theoretical Results

Theorems 10-14: Prove correctness of strategy template construction algorithms for various winning objectives

• SafetyTemplate constructs templates that are almost-surely winning for G X
• ReachabilityTemplate constructs templates that are almost-surely winning for F X
• Similar results apply to other objectives

Theorem 18: PositiveTemplate constructs templates that are both almost-surely and positively winning

Theorem 27: Parameterized extraction method is more permissive than the original Extract method

Permissiveness Analysis

Proposition 22: If P ⊇ P', L ⊇ L', C ⊇ C', then T is not more permissive than T'

Proposition 23: If T is not more permissive than T' and T' is winning, then T is also winning

Practical Application Potential

The paper indicates that based on deterministic game experimental results, strategy templates achieve at least 2x acceleration in incremental synthesis and effectively reduce recomputation in fault-tolerant control even when 30% of choices are disabled.

Related Work

Classical Permissiveness Theory

• Ramadge and Wonham (1987) formally introduced permissiveness in supervisory control
• Bernet et al. proved existence of maximally permissive strategies in parity games

Strategy Template Development

• Anand et al. introduced strategy templates for deterministic games at TACAS and CAV 2023
• This work is the first to extend strategy templates to stochastic games

Stochastic Game Solving

• Chatterjee et al.'s reduction method for stochastic parity games
• Banerjee et al.'s set operators for stochastic games

Conclusions and Discussion

Main Conclusions

1. Successfully extends strategy template concepts from deterministic to stochastic games
2. Provides a comprehensive algorithmic framework covering two winning criteria and five winning objectives
3. Novel strategy extraction methods improve permissiveness while maintaining correctness

Limitations

1. Positive winning strategies do not guarantee optimal probability
2. Algorithm implementation and experimental validation remain incomplete
3. Considers only finite-state games

Future Directions

1. Construct templates maintaining identical permissiveness but smaller size
2. Extend to objectives defined by metric temporal logic (MTL) formulas
3. Apply to real-time systems

In-Depth Evaluation

Strengths

1. Significant Theoretical Contribution: First extension of strategy templates to stochastic games with complete theoretical framework
2. Reasonable Algorithm Design: Cleverly leverages existing set operations and reduction techniques
3. Broad Application Prospects: Significant practical implications for cyber-physical systems control
4. Mathematical Rigor: Provides complete correctness proofs

Weaknesses

1. Lack of Experimental Validation: Primarily theoretical work lacking practical implementation and performance evaluation
2. Optimality Issues: Positive winning strategies do not guarantee optimality
3. Insufficient Complexity Analysis: Analysis of practical computational complexity is relatively brief

Impact

1. Academic Value: Provides new tools and methods for stochastic game theory
2. Practical Value: Provides theoretical foundation for permissive controller design
3. Extensibility: Provides solid foundational framework for subsequent research

Applicable Scenarios

1. Robust control of cyber-physical systems
2. Adaptive automated systems
3. Multi-objective control system design
4. Fault-tolerant control systems

References

The paper cites 35 related references, primarily covering:

• Foundational game theory literature
• Supervisory control theory
• Strategy template related work
• Stochastic game solving algorithms
• Linear temporal logic and model checking

Overall Assessment: This is a high-quality theoretical research paper that successfully extends the strategy template concept from deterministic to stochastic games, providing important theoretical foundations for permissive and resilient control. Although lacking experimental validation, its theoretical contributions are significant and have important implications for advancing related fields.