From local to global determinacy in concurrent graph games

TL;DR

This paper introduces a new class of concurrent graph games with stronger determinacy properties, based on the concept of determined local interactions, extending existing results to more complex, concurrent settings.

Contribution

It defines determined game forms and shows that if all local interactions are determined, the entire game is strongly determined, advancing the understanding of determinacy in concurrent games.

Findings

Games with determined local interactions are fully determined.

Determinacy extends from local interactions to entire concurrent games.

The approach generalizes existing results for turn-based games.

Abstract

In general, finite concurrent two-player reachability games are only determined in a weak sense: the supremum probability to win can be approached via stochastic strategies, but cannot be realized. We introduce a class of concurrent games that are determined in a much stronger sense, and in a way, it is the larger class with this property. To this end, we introduce the notion of \emph{local interaction} at a state of a graph game: it is a \emph{game form} whose outcomes (i.e. a table whose entries) are the next states, which depend on the concurrent actions of the players. By definition, a game form is \emph{determined} iff it always yields games that are determined via deterministic strategies when used as a local interaction in a Nature-free, one-shot reachability game. We show that if all the local interactions of a graph game with Borel objective are determined game forms, the game itself is determined: if Nature does not play, one player has a winning strategy; if Nature plays, both players have deterministic strategies that maximize the probability to win. This constitutes a clear-cut separation: either a game form behaves poorly already when used alone with basic objectives, or it behaves well even when used together with other well-behaved game forms and complex objectives. Existing results for positional and finite-memory determinacy in turn-based games are extended this way to concurrent games with determined local interactions (CG-DLI).