Reachability in Recursive Markov Decision Processes
Reachability in Recursive Markov Decision Processes
复制标题
递归马尔可夫决策过程中的可达性
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
A. Kucera
中科院分区：
文献类型：
--
作者：
T. Brázdil;V. Brozek;Vojtěch Forejt;A. Kucera
考虑一类由无状态下推自动机生成的无限状态马尔可夫决策过程。此类对应于BPA系统生成的图上的$1 frac{1}{2}$-玩家游戏或（等效）1-出口递归状态机。一个扩展的可达性目标由两组安全和终端栈配置S和T指定，其中S和T的成员资格仅取决于栈顶符号。问题是是否存在一个合适的策略，使得通过仅通过安全配置的路径到达终端配置的概率等于（或不同于）给定的x ∈{0，1}。我们证明了定性扩展可达性问题是在多项式时间内可判定的，并且存在获胜策略的所有配置的集合是有效正则的。更准确地说，这个集合可以用一个具有固定数量控制状态的确定性有限状态自动机来表示。这个结果是Etessami和Yannakakis最近的一个定理的推广，该定理说，1-出口RMDPs的定性终止（正好对应于我们的$1 frac{1}{2}$-玩家BPA游戏）在多项式时间内是可判定的。有趣的是，扩展的可达性目标的获胜策略的性质是完全不同的终止，并需要新的观察，以获得结果。作为应用，我们给出了$1 frac{1}{2}$-player BPA博弈模型检验问题的EXPTIME-完备性和定性PCTL公式。
We consider a class of infinite-state Markov decision processes generated by stateless pushdown automata. This class corresponds to $1 frac{1}{2}$-player games over graphs generated by BPA systems or (equivalently) 1-exit recursive state machines. An extended reachability objective is specified by two sets S and T of safe and terminal stack configurations, where the membership to S and T depends just on the top-of-the-stack symbol. The question is whether there is a suitable strategy such that the probability of hitting a terminal configuration by a path leading only through safe configurations is equal to (or different from) a given x ∈{0,1}. We show that the qualitative extended reachability problem is decidable in polynomial time, and that the set of all configurations for which there is a winning strategy is effectively regular. More precisely, this set can be represented by a deterministic finite-state automaton with a fixed number of control states. This result is a generalization of a recent theorem by Etessami & Yannakakis which says that the qualitative termination for 1-exit RMDPs (which exactly correspond to our $1 frac{1}{2}$-player BPA games) is decidable in polynomial time. Interestingly, the properties of winning strategies for the extended reachability objectives are quite different from the ones for termination, and new observations are needed to obtain the result. As an application, we derive the EXPTIME-completeness of the model-checking problem for $1 frac{1}{2}$-player BPA games and qualitative PCTL formulae.