Simple Stochastic Games with Almost-Sure Energy-Parity Objectives are in NP and coNP

TL;DR

This paper proves that the problem of determining almost-sure energy-parity objectives in stochastic games is decidable and belongs to the complexity class NP ∩ coNP, combining quantitative and qualitative conditions.

Contribution

It establishes that the almost-sure energy-parity problem is in NP ∩ coNP, providing new complexity bounds for these combined objectives in stochastic games.

Findings

The problem is decidable.

It belongs to NP ∩ coNP.

Results apply to both existence of strategies and minimal energy levels.

Abstract

We study stochastic games with energy-parity objectives, which combine quantitative rewards with a qualitative $\omega$-regular condition: The maximizer aims to avoid running out of energy while simultaneously satisfying a parity condition. We show that the corresponding almost-sure problem, i.e., checking whether there exists a maximizer strategy that achieves the energy-parity objective with probability $1$ when starting at a given energy level $k$, is decidable and in $NP \cap coNP$. The same holds for checking if such a $k$ exists and if a given $k$ is minimal.