Stochastic Games with Disjunctions of Multiple Objectives (Technical Report)

TL;DR

This paper studies stochastic games with disjunctive objectives, providing complexity bounds and a new algorithm for approximating Pareto optimal thresholds in multi-objective control scenarios.

Contribution

It introduces the dual disjunctive problem in stochastic games, extends the theoretical understanding with new bounds, and proposes a novel value iteration algorithm.

Findings

New lower and upper bounds for disjunctive queries in stochastic games.

A novel value iteration-style algorithm for Pareto threshold approximation.

Extended analysis of strategy and computational complexity.

Abstract

Stochastic games combine controllable and adversarial non-determinism with stochastic behavior and are a common tool in control, verification and synthesis of reactive systems facing uncertainty. Multi-objective stochastic games are natural in situations where several - possibly conflicting - performance criteria like time and energy consumption are relevant. Such conjunctive combinations are the most studied multi-objective setting in the literature. In this paper, we consider the dual disjunctive problem. More concretely, we study turn-based stochastic two-player games on graphs where the winning condition is to guarantee at least one reachability or safety objective from a given set of alternatives. We present a fine-grained overview of strategy and computational complexity of such \emph{disjunctive queries} (DQs) and provide new lower and upper bounds for several variants of the problem, significantly extending previous works. We also propose a novel value iteration-style algorithm for approximating the set of Pareto optimal thresholds for a given DQ.