Laboratory for Foundations
of Computer Science
School of Informatics
University of Edinburgh
2:45pm 11 June 2004 (after Javier)
Room 2511, JCMB, King's Buildings
A recursive markov chain (RMC) is a recursive state machine (RSM) whose non-terminating nodes have out-edges labeled by probabilities that sum to 1. This naturally defines an infinite state markov chain on the global states of the underlying RSM.
We provide algorithms for, and study the computational complexity of, computing the probability of eventually reaching a given state of the RMC from another given state. As with ordinary probabilistic state machines, such algorithms are a core building block for model checking these probabilistic systems.
Joint work with Mihalis Yannakakis.