Approximating Values of Generalized-Reachability Stochastic Games

TL;DR

This paper introduces an algorithm to approximate the Pareto frontier in generalized-reachability stochastic games, providing a practical method for multi-objective analysis despite the open decidability problem.

Contribution

It presents an anytime approximation algorithm for the Pareto frontier in complex stochastic games with multiple reachability objectives.

Findings

Algorithm effectively approximates the Pareto frontier

Provides error bounds and can be stopped at any time

Advances analysis of multi-objective stochastic games

Abstract

Simple stochastic games are turn-based 2.5-player games with a reachability objective. The basic question asks whether one player can ensure reaching a given target with at least a given probability. A natural extension is games with a conjunction of such conditions as objective. Despite a plethora of recent results on the analysis of systems with multiple objectives, the decidability of this basic problem remains open. In this paper, we present an algorithm approximating the Pareto frontier of the achievable values to a given precision. Moreover, it is an anytime algorithm, meaning it can be stopped at any time returning the current approximation and its error bound.