Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Concurrent Permissive Strategy Templates

Ashwani Anand, Christel Baier, Calvin Chau, Sascha Klüppelholz, Ali Mirzaei, Satya Prakash Nayak, Anne-Kathrin Schmuck

TL;DR

This work extends permissive strategy templates from turn-based to concurrent games to address the synchronous interactions typical in cyber-physical systems. It introduces ConSTels, a concisely encoded, randomized strategy template framework for concurrent Safety, Büchi, and Co-Büchi objectives, derived via symbolic fixed-point methods and organized into safety, live-group, and co-live templates. Offline, ConSTels enable incremental synthesis by composing templates for simple objectives into non-conflicting templates for complex ones; online, they support runtime adaptation by adjusting action probabilities while preserving correctness. A prototype tool demonstrates feasibility on 171 converted SYNTCOMP benchmarks and showcases potential for offline compositional synthesis and online optimization in CPS, albeit with performance trade-offs due to concurrency complexity.

Abstract

Two-player games on finite graphs provide a rigorous foundation for modeling the strategic interaction between reactive systems and their environment. While concurrent game semantics naturally capture the synchronous interactions characteristic of many cyber-physical systems (CPS), their adoption in CPS design remains limited. Building on the concept of permissive strategy templates (PeSTels) for turn-based games, we introduce concurrent (permissive) strategy templates (ConSTels) -- a novel representation for sets of randomized winning strategies in concurrent games with Safety, Büchi, and Co-Büchi objectives. ConSTels compactly encode infinite families of strategies, thereby supporting both offline and online adaptation. Offline, we exploit compositionality to enable incremental synthesis: combining ConSTels for simpler objectives into non-conflicting templates for more complex combined objectives. Online, we demonstrate how ConSTels facilitate runtime adaptation, adjusting action probabilities in response to observed opponent behavior to optimize performance while preserving correctness. We implemented ConSTel synthesis and adaptation in a prototype tool and experimentally show its potential.

Concurrent Permissive Strategy Templates

TL;DR

This work extends permissive strategy templates from turn-based to concurrent games to address the synchronous interactions typical in cyber-physical systems. It introduces ConSTels, a concisely encoded, randomized strategy template framework for concurrent Safety, Büchi, and Co-Büchi objectives, derived via symbolic fixed-point methods and organized into safety, live-group, and co-live templates. Offline, ConSTels enable incremental synthesis by composing templates for simple objectives into non-conflicting templates for complex ones; online, they support runtime adaptation by adjusting action probabilities while preserving correctness. A prototype tool demonstrates feasibility on 171 converted SYNTCOMP benchmarks and showcases potential for offline compositional synthesis and online optimization in CPS, albeit with performance trade-offs due to concurrency complexity.

Abstract

Two-player games on finite graphs provide a rigorous foundation for modeling the strategic interaction between reactive systems and their environment. While concurrent game semantics naturally capture the synchronous interactions characteristic of many cyber-physical systems (CPS), their adoption in CPS design remains limited. Building on the concept of permissive strategy templates (PeSTels) for turn-based games, we introduce concurrent (permissive) strategy templates (ConSTels) -- a novel representation for sets of randomized winning strategies in concurrent games with Safety, Büchi, and Co-Büchi objectives. ConSTels compactly encode infinite families of strategies, thereby supporting both offline and online adaptation. Offline, we exploit compositionality to enable incremental synthesis: combining ConSTels for simpler objectives into non-conflicting templates for more complex combined objectives. Online, we demonstrate how ConSTels facilitate runtime adaptation, adjusting action probabilities in response to observed opponent behavior to optimize performance while preserving correctness. We implemented ConSTel synthesis and adaptation in a prototype tool and experimentally show its potential.
Paper Structure (15 sections, 16 theorems, 53 equations, 4 figures, 2 algorithms)

This paper contains 15 sections, 16 theorems, 53 equations, 4 figures, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Overview and Problem Statement
  4. Computing Winning Strategy Templates
  5. Preliminaries
  6. Concurrent Safety Templates
  7. Concurrent Live-Group Templates
  8. Concurrent Co-Live Templates
  9. Conflict-freeness and Strategy Extraction
  10. Composition of Strategy Templates
  11. Experiments
  12. Algorithms
  13. Formal Proofs of the Results
  14. Additional Proofs of Completeness of Algorithms
  15. Non-maximally permissiveness examples for templates

Key Result

theorem thmcountertheorem

Let $(\gamegraph, \Box \targetSet)$ be a concurrent safety game with $\wino=\wino(\Box\targetSet)$ and Then $\templatesafe(\funcSafe)$ is (almost surely) winning in $(\gamegraph, \Box \targetSet)$ and maximally permissive.

Figures (4)

  • Figure 1: Motivating Example. Left: Two robots, $\robotC$ and $\robotE$, moving in a grid world. $\robotC$ must enter a green region alone to fulfill a task. Both robots can move either clockwise ($\clockwise$) or anti-clockwise ($\anticlockwise$). Right: Concurrent game graph capturing the synchronous strategic interaction of $\robotC$ and $\robotE$.
  • Figure 2: Conflict analysis.
  • Figure 3: Expected steps to reach $S_e$.
  • Figure 4: A Büchi game, where $\targetSet = \{C\}$ is the goal set.

Theorems & Definitions (31)

  • definition thmcounterdefinition
  • theorem thmcountertheorem
  • definition thmcounterdefinition
  • theorem thmcountertheorem
  • definition thmcounterdefinition
  • theorem thmcountertheorem
  • remark thmcounterremark
  • definition thmcounterdefinition
  • theorem thmcountertheorem
  • theorem thmcountertheorem
  • ...and 21 more