The Complexity of Concurrent Rational Synthesis

TL;DR

This paper explores the complexity of rational synthesis in concurrent games with various objectives, introducing a game-theoretic algorithm that improves understanding of decidability and computational complexity.

Contribution

It presents a new game-theoretic algorithm for rational synthesis, establishing decidability and complexity results for multiple objectives in concurrent games.

Findings

Reachability, safety, Büchi, and co-Büchi are PSpace-complete.

Muller, Streett, and Rabin are PSpace-hard and in ExpTime.

New complexity bounds for rational synthesis problems.

Abstract

In this paper, we investigate the rational synthesis problem for concurrent game structure for a variety of objectives ranging from reachability to Muller condition. We propose a new algorithm that establishes the decidability of the non cooperative rational synthesis problem that relies solely on game theoretic technique as opposed to previous approaches that are logic based. Thanks to this approach, we construct a zero-sum turn-based game that can be adapted to each one of the afore mentioned objectives thus obtain new complexity results. In particular, we show that reachability, safety, B\"uchi, and co-B\"uchi conditions are PSpace-complete, Muller, Street, and Rabin are PSpace-hard and in ExpTime.