Reachability in Stochastic Timed Games
| Authors | |
|---|---|
| Year of publication | 2009 |
| Type | Article in Proceedings |
| Conference | Automata, Languages and Programming, 36th Internatilonal Colloquium, ICALP 2009, Rhodes, greece, July 5-12, 2009,Proceedings, Part II |
| MU Faculty or unit | |
| Citation | |
| Doi | http://dx.doi.org/10.1007/978-3-642-02930-1_9 |
| Field | Informatics |
| Keywords | timed systems stochastic systems verification |
| Description | 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). |
| Related projects: |