Stochastic Timed Games Revisited

TL;DR

This paper investigates the decidability boundaries of stochastic timed games with reachability objectives, showing undecidability results for certain clock configurations and identifying classes where the problem remains decidable.

Contribution

It refines the understanding of decidability in stochastic timed games by establishing new undecidability results and identifying decidable subclasses.

Findings

Quantitative reachability is undecidable for 1.5-player four-clock STGs.

Time-bounded restrictions do not resolve undecidability for 2.5-player five-clock STGs.

A specific class of STGs with certain parameters has decidable quantitative reachability.

Abstract

Stochastic timed games (STGs), introduced by Bouyer and Forejt, naturally generalize both continuous-time Markov chains and timed automata by providing a partition of the locations between those controlled by two players (Player Box and Player Diamond) with competing objectives and those governed by stochastic laws. Depending on the number of players---$2$, $1$, or $0$---subclasses of stochastic timed games are often classified as $2\frac{1}{2}$-player, $1\frac{1}{2}$-player, and $\frac{1}{2}$-player games where the $\frac{1}{2}$ symbolizes the presence of the stochastic "nature" player. For STGs with reachability objectives it is known that $1\frac{1}{2}$-player one-clock STGs are decidable for qualitative objectives, and that $2\frac{1}{2}$-player three-clock STGs are undecidable for quantitative reachability objectives. This paper further refines the gap in this decidability spectrum. We show that quantitative reachability objectives are already undecidable for $1\frac{1}{2}$ player four-clock STGs, and even under the time-bounded restriction for $2\frac{1}{2}$-player five-clock STGs. We also obtain a class of $1\frac{1}{2}$, $2\frac{1}{2}$ player STGs for which the quantitative reachability problem is decidable.