Reachability in Stochastic Timed Games
Reachability in Stochastic Timed Games
复制标题
随机定时游戏中的可达性
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Vojtěch Forejt
中科院分区：
文献类型：
--
作者：
P. Bouyer;Vojtěch Forejt
我们定义了随机计时对策，它用概率(遵循Baier等人最近的方法)扩展了两人计时对策，并以自然的方式扩展了连续时间马尔可夫决策过程。我们关注这些游戏的可达性问题，并询问其中一个玩家是否有策略来确保达到固定状态集的概率等于(或低于)。上图)某个数字r，无论第二个玩家做什么。我们证明了这个问题在一般情况下是不可决定的，但如果我们限制在单时钟1$FRAC{1}{2}$玩家游戏中，并询问玩家是否能确保到达集合的概率=1(或>；0，=0)，那么这个问题就是可决定的。
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$frac{1}{2}$-player games and ask whether the player can ensure that the probability of reaching the set is =1 (or >0, =0).