Reachability in Stochastic Timed Games

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 11 2 -player games and ask whether the player can ensure that the probability of reaching the set is =1 (or >0, =0).

• Type: Conference
• Year: 2009
• Where: ICALP
• Authors: Patricia Bouyer, Vojtech Forejt
• Keywords: Continuous-Time Markov Decision, ICALP 2009, Stochastic Timed Games, Theoretical Computer Science, Two-player Timed Games