The Non-Cooperative Rational Synthesis Problem for Subgame Perfect Equilibria and omega-regular Objectives

TL;DR

This paper investigates the complexity of rational synthesis in multi-player graph games with omega-regular objectives, providing algorithms and complexity bounds for different fixed parameters and objectives.

Contribution

It introduces a complexity analysis and algorithms for the rational synthesis problem under subgame perfect equilibria with omega-regular objectives, extending prior work to more general game settings.

Findings

The problem is in 2ExpTime for general cases.

Fixed number of environment players reduces complexity to ExpTime.

For fixed players and reachability objectives, a polynomial-time algorithm is available.

Abstract

This paper studies the rational synthesis problem for multi-player games played on graphs when rational players are following subgame perfect equilibria. In these games, one player, the system, declares his strategy upfront, and the other players, composing the environment, then rationally respond by playing strategies forming a subgame perfect equilibrium. We study the complexity of the rational synthesis problem when the players have {\omega}-regular objectives encoded as parity objectives. Our algorithm is based on an encoding into a three-player game with imperfect information, showing that the problem is in 2ExpTime. When the number of environment players is fixed, the problem is in ExpTime and is NP- and coNP-hard. Moreover, for a fixed number of players and reachability objectives, we get a polynomial algorithm.