Oxford logo
[BF09a] P. Bouyer and V. Forejt. Reachability in Stochastic Timed Games. In S. Albers, A. Marchetti-Spaccamela, Y. Matias, S. E. Nikoletseas and W. Thomas (editors), Automata, Languages and Programming, 36th International Colloquium, ICALP 2009, Rhodes, greece, July 5-12, 2009, Proceedings, Part II, volume 5556 of Lecture Notes in Computer Science, pages 103-114, Springer. 2009. [pdf] [bib]
Downloads:  pdf pdf (248 KB)  bib bib
Notes: The original publication is available at link.springer.com.
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½-player games and ask whether the player can ensure that the probability of reaching the set is =1 (or >0, =0).

QAV:

Home

People

Projects

Publications