Table of Contents
Fetching ...

Non-cooperative rational synthesis problem for probabilistic strategies

So Koide, Yoshiaki Takata, Hiroyuki Seki

TL;DR

NCRSP is shown to be undecidable even for pure finite-state strategies and terminal reachability objectives, and NCRSP_>, which is a variant of NCRSP, is shown to be undecidable even for pure finite-state strategies and terminal reachability objectives.

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.

Non-cooperative rational synthesis problem for probabilistic strategies

TL;DR

NCRSP is shown to be undecidable even for pure finite-state strategies and terminal reachability objectives, and NCRSP_>, which is a variant of NCRSP, is shown to be undecidable even for pure finite-state strategies and terminal reachability objectives.

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.
Paper Structure (14 sections, 11 theorems, 6 equations, 4 figures, 1 table)

This paper contains 14 sections, 11 theorems, 6 equations, 4 figures, 1 table.

Key Result

Proposition 1

Let ${\cal{M}}$ be an MDP with a player $i$. There exists a stationary strategy $\tau$ for player $i$ that satisfies: $\forall E\in \mathrm{EC}_{\cal{M}},\forall v\in E$, $Pr^{\tau}_{v}(\{\pi\in V^{\omega}\mid \mathit{inf}(\pi)=E\})=1.$

Figures (4)

  • Figure 1: An SMG for which the answer of Stationary-Positional-NCRSP is yes and that of Pure-NCRSP is no with $\mu =1$
  • Figure 2: An SMG for which the answer of Pure-NCRSP is yes and that of Stationary-Positional-NCRSP is no with $\mu =1$
  • Figure 3: An SMG for which the answer of Stationary-NCRSP is yes and that of Stationary-Positional-NCRSP is no with $\mu =1$
  • Figure 4: An SMG for which the answer of Stationary-Positional-NCRSP is yes and that of Stationary-NCRSP is no with $\mu =1$

Theorems & Definitions (19)

  • Proposition 1
  • Proposition 2: C75
  • Theorem 3
  • proof
  • Example 4
  • Example 5
  • Example 6
  • Example 7
  • Proposition 8: JC88
  • Theorem 9
  • ...and 9 more