Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Existence of Reactive Strategies Resilient to Delay

Martin Fränzle, Paul Kröger, Sarah Winter, Martin Zimmermann

TL;DR

This paper analyzes two infinite-game models for reactive synthesis under delay: games under delayed control, where both players face information delays, and delay games, where lookahead is granted to the controller. It proves tight, polynomial-time reductions between the models for sure-winning strategies, enabling transfer of complexity and delay bounds across safety, reachability, parity, and LTL conditions, and establishing exponential decisive delays. The work further reveals fundamental distinctions in randomized and probabilistic settings, showing that almost-sure or probability-driven outcomes can diverge between the two frameworks, and demonstrates that controller-win probabilities can densely fill the interval [0,1] for ω-regular winning conditions. The results refine the understanding that delayed-control games are not determined in general and highlight a nuanced landscape where determinacy, randomness, and lookahead interact in intricate ways with practical implications for synthesis under delay.

Abstract

We compare games under delayed control and delay games, two types of infinite games modelling asynchronicity in reactive synthesis. In games under delayed control both players suffer from partial informedness due to symmetrically delayed communication, while in delay games, the protagonist has to grant lookahead to the alter player. Our first main result, the interreducibility of the existence of sure winning strategies for the protagonist, allows to transfer known complexity results and bounds on the delay from delay games to games under delayed control, for which no such results had been known. We furthermore analyse existence of randomized strategies that win almost surely, where this correspondence between the two types of games breaks down. In this setting, some games surely won by the alter player in delay games can now be won almost surely by the protagonist in the corresponding game under delayed control, showing that it indeed makes a difference whether the protagonist has to grant lookahead or both players suffer from partial informedness. These results get even more pronounced when we finally address the quantitative goal of winning with a probability in $[0,1]$. We show that for any rational threshold $θ\in [0,1]$ there is a game that can be won by the protagonist with exactly probability $θ$ under delayed control, while being surely won by alter in the delay game setting. All these findings refine our original result that games under delayed control are not determined.

On the Existence of Reactive Strategies Resilient to Delay

TL;DR

This paper analyzes two infinite-game models for reactive synthesis under delay: games under delayed control, where both players face information delays, and delay games, where lookahead is granted to the controller. It proves tight, polynomial-time reductions between the models for sure-winning strategies, enabling transfer of complexity and delay bounds across safety, reachability, parity, and LTL conditions, and establishing exponential decisive delays. The work further reveals fundamental distinctions in randomized and probabilistic settings, showing that almost-sure or probability-driven outcomes can diverge between the two frameworks, and demonstrates that controller-win probabilities can densely fill the interval [0,1] for ω-regular winning conditions. The results refine the understanding that delayed-control games are not determined in general and highlight a nuanced landscape where determinacy, randomness, and lookahead interact in intricate ways with practical implications for synthesis under delay.

Abstract

We compare games under delayed control and delay games, two types of infinite games modelling asynchronicity in reactive synthesis. In games under delayed control both players suffer from partial informedness due to symmetrically delayed communication, while in delay games, the protagonist has to grant lookahead to the alter player. Our first main result, the interreducibility of the existence of sure winning strategies for the protagonist, allows to transfer known complexity results and bounds on the delay from delay games to games under delayed control, for which no such results had been known. We furthermore analyse existence of randomized strategies that win almost surely, where this correspondence between the two types of games breaks down. In this setting, some games surely won by the alter player in delay games can now be won almost surely by the protagonist in the corresponding game under delayed control, showing that it indeed makes a difference whether the protagonist has to grant lookahead or both players suffer from partial informedness. These results get even more pronounced when we finally address the quantitative goal of winning with a probability in . We show that for any rational threshold there is a game that can be won by the protagonist with exactly probability under delayed control, while being surely won by alter in the delay game setting. All these findings refine our original result that games under delayed control are not determined.
Paper Structure (20 sections, 16 theorems, 4 equations, 9 figures, 1 table)

This paper contains 20 sections, 16 theorems, 4 equations, 9 figures, 1 table.

Table of Contents

  1. Introduction
  2. Games under Delayed Control
  3. Delay Games
  4. On Player Names
  5. Our Contributions
  6. Preliminaries
  7. Games under Delayed Control
  8. Delay Games
  9. Games under Delayed Control vs. Delay Games
  10. omega-Automata
  11. From Games under Delayed Control to Delay Games and Back
  12. Results
  13. Safety
  14. Reachability
  15. Parity
  16. ...and 5 more sections

Key Result

Lemma 3.3

Let $\mathcal{G}$ be a game and $\delta \ge 0$ even. Controller wins $\mathcal{G}$ under delay $\delta$ if and only if Player $I$ wins $\Gamma\!_{k}(\overline{L(\mathcal{G})})$ for $k = \frac{\delta}{2}$.

Figures (9)

  • Figure 1: The game for \ref{['example:gameunderdelayedcontrol']}. Controller wins all plays that never visit the black vertex. Note that we have $\Sigma_c =\{a,b\}$ and $\Sigma_e = \{u,u'\}$.
  • Figure 2: The safety automaton accepting the winning condition $L(\mathcal{G})$ obtained by applying \ref{['trans:controltodelaygame']} to the game from \ref{['example:gameunderdelayedcontrol']}. A run is accepting if it does not visit the black state.
  • Figure 3: The game under delayed control obtained by applying \ref{['trans:delaygametocontrol']} to the delay game from \ref{['example:delaygame']}. All incoming edges to vertex $j$ are labeled by action $j$, all incoming edges to vertex $j'$ are labeled by action $j'$.
  • Figure 4: A safety game that environment does not win under any delay, but Player $O$ wins the associated delay game with $k \ge 1$. The initial state is marked by an arrow and the unsafe vertices are black. Note that both players have the actions $h$ and $t$ available.
  • Figure 5: The relation between games under delayed control and delay games with Borel winning conditions. The upper ellipsis contains pairs $(\mathcal{G}, \delta)$ consisting of a game $\mathcal{G}$ under delayed control and a fixed delay $\delta$; the lower one contains delay games $\Gamma\!_{k}(L)$ for some fixed $k$. The arrows represent the two transformations described in \ref{['sec:transformation']}.
  • ...and 4 more figures

Theorems & Definitions (44)

  • Remark 2.1
  • Remark 2.2
  • Example 2.3
  • Remark 2.4
  • Remark 2.5
  • Example 2.6
  • Remark 2.7
  • Remark 2.8
  • Example 3.2
  • Lemma 3.3
  • ...and 34 more