Reactive Synthesis Without Regret

TL;DR

This paper introduces algorithms for computing strategies in two-player infinite-duration games that minimize regret, ensuring better performance against unpredictable or limited adversaries in verification scenarios.

Contribution

It presents novel algorithms for regret-minimizing strategies in infinite games, covering unrestricted, positional, and word strategy adversaries, and relates these to existing problems.

Findings

Algorithms for regret-minimizing strategies against various adversaries.

Strategies guarantee minimal regret in infinite-duration games.

Connections established with related problems in the literature.

Abstract

Two-player zero-sum games of infinite duration and their quantitative versions are used in verification to model the interaction between a controller (Eve) and its environment (Adam). The question usually addressed is that of the existence (and computability) of a strategy for Eve that can maximize her payoff against any strategy of Adam. In this work, we are interested in strategies of Eve that minimize her regret, i.e. strategies that minimize the difference between her actual payoff and the payoff she could have achieved if she had known the strategy of Adam in advance. We give algorithms to compute the strategies of Eve that ensure minimal regret against an adversary whose choice of strategy is (i) unrestricted, (ii) limited to positional strategies, or (iii) limited to word strategies. We also establish relations between the latter version and other problems studied in the literature.