Reachability in stochastic timed games

Abstract

We define stochastic timed games, which extend two-player timed games with probabilities (following a recent approach by Baier et al), and which extend in a natural way continuous-time Markov decision processes. We focus on the reachability problem for these games, and ask whether one of the players has a strategy to ensure that the probability of reaching a fixed set of states is equal to (or below, resp. above) a certain number r, whatever the second player does. We show that the problem is undecidable in general, but that it becomes decidable if we restrict to single-clock 1 1/2-player games and ask whether the player can ensure that the probability of reaching the set is =1 (or >0, =0). © 2009 Springer Berlin Heidelberg.