- Abstract:
-
We introduce Recursive Markov Decision Processes (RMDPs) and Recursive Simple Stochastic Games (RSSGs), and study the decidability and complexity of algorithms for their analysis and verification. These models extend Recursive Markov Chains (RMCs), introduced in [EY05a, EY05b] as a natural model for verification of probabilistic procedural programs and related systems involving both recursion and probabilistic behavior. RMCs define a class of denumerable Markov chains with a rich theory generalizing that of stochastic context-free grammars and multi-type branching processes, and they are also intimately related to probabilistic pushdown systems. RMDPs & RSSGs extend RMCs with one controller or two adversarial players, respectively. Such extensions are useful for modeling nondeterministic and concurrent behavior, as well as modeling a system s interactions with an environment. We provide upper and lower bounds for deciding, given an RMDP (or RSSG) A and probability p, whether player 1 has a strategy to force termination at a desired exit with probability at least p. We also address qualitative termination, where p=1, and model checking questions.
- Links To Paper
- 1st Link
- Bibtex format
- @InProceedings{EDI-INF-RR-0656,
- author = {
Kousha Etessami
and Mihalis Yannakakis
},
- title = {Recursive Markov Decison Processes and Recursive Stochastic Games},
- book title = {Proceedings of ICALP 2005 (International Colloquium on Automata, Languages and Programming)},
- publisher = {Springer},
- year = 2005,
- volume = {3580},
- pages = {891-903},
- doi = {10.1007/11523468_72},
- url = {http://www.springerlink.com/(1vjgshiiyn4zbr45fhez3v55)/app/home/contribution.asp?referrer=parent&backto=issue,72,118;journal,252,2376;linkingpublicationresults,1:105633,1},
- }
|
