Stochastic Timed Games Revisited
S. Akshay, Patricia Bouyer, Shankara Narayanan Krishna, Lakshmi Manasa, Ashutosh Trivedi.
MFCS 2016 : 8:1-8:14
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½-player, 1½-player, and ½-player games where the ½ symbolizes the presence of the stochastic “nature” player. For STGs with reachability objectives it is known that 1½-player one-clock STGs are decidable for qualitative objectives, and that 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½ player four-clock STGs, and even under the time-bounded restriction for 2½-player five-clock STGs. We also obtain a class of 1½, 2½ player STGs for which the quantitative reachability problem is decidable.