Lab for Foundations of Computer Science
University of Edinburgh
4pm Tuesday 25th October 2005
Room 2511, JCMB, King's Buildings
We will 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), which we introduced earlier 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 multi-type Branching Processes, and they are also intimately related to probabilistic Pushdown Systems. RMDPs & RSSGs extend RMCs with one controller and two adversarial players, respectively. Such extensions are useful for modeling nondeterministic and concurrent behavior, as well as for modeling a system's interactions with an environment.
We provide a number of strong 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 questions, where p=1, as well as model checking questions.
Time permitting, we will briefly describe some potential applications of RMDPs in population biology and computational biology.
(This talk describes joint work with Mihalis Yannakakis (Columbia U.). It partly describes work that appeared in a paper at ICALP'05, and also more recent work that appears in a submitted paper.)