[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]
|
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).
|