Non-cooperative rational synthesis problem for probabilistic strategies

TL;DR

This paper investigates the decidability and complexity of the non-cooperative rational synthesis problem for probabilistic strategies, revealing various complexity results and decidability boundaries under different strategy restrictions.

Contribution

It provides new complexity classifications and decidability results for NCRSP with probabilistic strategies, including cases with stationary, positional, and memory-restricted strategies.

Findings

NCRSP for stationary strategies and Muller objectives is in 3-EXPTIME.

NCRSP with positional environment strategies is NEXPSPACE solvable.

NCRSP_> is undecidable even for pure finite-state strategies.

Abstract

We study the decidability and complexity of non-cooperative rational synthesis problem (abbreviated as NCRSP) for some classes of probabilistic strategies. We show that NCRSP for stationary strategies and Muller objectives is in 3-EXPTIME, and if we restrict the strategies of environment players to be positional, NCRSP becomes NEXPSPACE solvable. On the other hand, NCRSP_>, which is a variant of NCRSP, is shown to be undecidable even for pure finite-state strategies and terminal reachability objectives. Finally, we show that NCRSP becomes EXPTIME solvable if we restrict the memory of a strategy to be the most recently visited t vertices where t is linear in the size of the game.