Reachability in Stochastic Timed Games

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BOUYER Patricia FOREJT Vojtěch

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

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.