Recursive Markov Decision Processes and Recursive Stochastic Games

被引:16
作者
Etessami, Kousha [1 ]
Yannakakis, Mihalis [2 ]
机构
[1] Univ Edinburgh, Sch Informat, LFCS, Edinburgh EH8 9YL, Midlothian, Scotland
[2] Columbia Univ, Dept Comp Sci, New York, NY 10027 USA
基金
美国国家科学基金会;
关键词
Algorithms; Theory; Verification; Recursive stochastic processes; Markov decision processes; stochastic games; multitype branching processes; stochastic context-free grammars; MODEL CHECKING; MONOTONE SYSTEMS; COMPLEXITY; REACHABILITY; OPTIMIZATION; GRAMMARS; TIME;
D O I
10.1145/2699431
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
We introduce Recursive Markov Decision Processes (RMDPs) and Recursive Simple Stochastic Games (RSSGs), which are classes of (finitely presented) countable-state MDPs and zero-sum turn-based (perfect information) stochastic games. They extend standard finite-state MDPs and stochastic games with a recursion feature. We study the decidability and computational complexity of these games under termination objectives for the two players: one player's goal is to maximize the probability of termination at a given exit, while the other player's goal is to minimize this probability. In the quantitative termination problems, given an RMDP (or RSSG) and probability p, we wish to decide whether the value of such a termination game is at least p (or at most p); in the qualitative termination problem we wish to decide whether the value is 1. The important 1-exit subclasses of these models, 1-RMDPs and 1-RSSGs, correspond in a precise sense to controlled and game versions of classic stochastic models, including multitype Branching Processes and Stochastic Context-Free Grammars, where the objective of the players is to maximize or minimize the probability of termination (extinction). We provide a number of upper and lower bounds for qualitative and quantitative termination problems for RMDPs and RSSGs. We show both problems are undecidable for multi-exit RMDPs, but are decidable for 1-RMDPs and 1-RSSGs. Specifically, the quantitative termination problem is decidable in PSPACE for both 1-RMDPs and 1-RSSGs, and is at least as hard as the square root sum problem, a well-known open problem in numerical computation. We show that the qualitative termination problem for 1-RMDPs (i.e., a controlled version of branching processes) can be solved in polynomial time both for maximizing and minimizing 1-RMDPs. The qualitative problem for 1-RSSGs is in NP boolean AND coNP, and is at least as hard as the quantitative termination problem for Condon's finite-state simple stochastic games, whose complexity remains a well known open problem. Finally, we show that even for 1-RMDPs, more general (qualitative and quantitative) model-checking problems with respect to linear-time temporal properties are undecidable even for a fixed property.
引用
收藏
页数:69
相关论文
共 76 条
  • [1] ON THE COMPLEXITY OF NUMERICAL ANALYSIS
    Allender, Eric
    Buergisser, Peter
    Kjeldgaard-Pedersen, Johan
    Miltersen, Peter Bro
    [J]. SIAM JOURNAL ON COMPUTING, 2009, 38 (05) : 1987 - 2006
  • [2] Analysis of recursive state machines
    Alur, R
    Benedikt, M
    Etessami, K
    Godefroid, P
    Reps, T
    Yannakakis, M
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005, 27 (04): : 786 - 818
  • [3] Alur R., 1995, Proceedings of the Twenty-Seventh Annual ACM Symposium on the Theory of Computing, P363, DOI 10.1145/225058.225161
  • [4] [Anonymous], STOC
  • [5] [Anonymous], 2002, HDB MARKOV DECISION
  • [6] [Anonymous], 2002, Branching Processes in Biology, DOI DOI 10.1007/B97371
  • [7] [Anonymous], 1992, INF COMPUT
  • [8] [Anonymous], NATO ASI SERIES
  • [9] [Anonymous], 2004, Branching processes
  • [10] Model checking for a probabilistic branching time logic with fairness
    Baier, C
    Kwiatkowska, M
    [J]. DISTRIBUTED COMPUTING, 1998, 11 (03) : 125 - 155