Solving Qualitative Multi-Objective Stochastic Games

TL;DR

The paper advances the theory of two-player stochastic games by classifying when qualitative multi-objective objectives are determinate and by pinpointing the computational complexity for winner determination across natural fragments. Through reductions to nonstochastic reachability and the introduction of goal unfolding, it shows that conjunctions and positive Boolean combinations of $AS$ or $NZ$ qualitative objectives are $PSPACE$-complete to decide, while full Boolean combinations are not determined and are $NEXPTIME$-hard. It also provides memory bounds for winning strategies, proving that exponential memory suffices for several determined subclasses, which underpins the $NEXPTIME$ membership results. Collectively, the work broadens the complexity landscape for stochastic games in the multi-objective, qualitative setting and links determinacy with logics featuring partially-ordered quantification, with implications for rational verification and assume-guarantee reasoning in probabilistic systems.

Abstract

Many problems in compositional synthesis and verification of multi-agent systems -- such as rational verification and assume-guarantee verification in probabilistic systems -- reduce to reasoning about two-player multi-objective stochastic games. This motivates us to study the problem of characterizing the complexity and memory requirements for two-player stochastic games with Boolean combinations of qualitative reachability and safety objectives. Reachability objectives require that a given set of states is reached; safety requires that a given set is invariant. A qualitative winning condition asks that an objective is satisfied almost surely (AS) or (in negated form) with non-zero (NZ) probability. We study the determinacy and complexity landscape of the problem. We show that games with conjunctions of AS and NZ reachability and safety objectives are determined, and determining the winner is PSPACE-complete. The same holds for positive boolean combinations of AS reachability and safety, as well as for negations thereof. On the other hand, games with full Boolean combinations of qualitative objectives are not determined, and are NEXPTIME-hard. Our hardness results show a connection between stochastic games and logics with partially-ordered quantification. Our results shed light on the relationship between determinacy and complexity, and extend the complexity landscape for stochastic games in the multi-objective setting.

Figures (5)

• Figure 1: Example stochastic game.
• Figure 2: Example game where a winning strategy requires memory other than visited target sets.
• Figure 3: Example game where winning strategies require memory other than the set of visited states.
• Figure 4: Example construction for a DQBF formula $\Phi = \forall x_1, x_2, x_3 \exists y_{1, S_1}\exists y_{2, S_2}\exists y_{3, S_3} \phi$ where $S_1 = \{x_1, x_2\}$, $S_2 = \{x_2, x_3\}$, $S_3 = \{x_1, x_3\}$. Each node annotated with a variable represents the module for that variable.
• Figure 5: Construction for the module of a variable $y_k$ on branch $j$. In a module for a variable $x_k$, the node $s_{x_k, j}$ is instead controlled by player 2.

Theorems & Definitions (17)

• Definition 1: Stochastic Games
• Definition 2: Strategies
• Proposition 1: Determinacy
• Definition 3: restricted game
• Theorem 1
• lemma 1: Conjunction of nonzero
• lemma 2: Conjunction of $AS$
• lemma 3: Conjunction of AS and one NZ reachability
• lemma 4: Conjunction of AS and NZ reachability
• lemma 5: Almost sure safety