Model Checking of Recursive Probabilistic Systems

Recursive Markov Chains (RMCs) are a natural abstract model of procedural
probabilistic programs and related systems involving recursion and probability.
They succinctly define a class of denumerable Markov chains that generalize several other stochastic models, and they are equivalent in a precise sense to probabilistic Pushdown Systems. In this paper, we study the problem of model checking an RMC against an ω-regular specification, given in terms of a B¨uchi automaton or a Linear Temporal Logic (LTL) formula. Namely, given an RMC A and a property we wish to know the probability that an execution of A satisfies the property. We establish a number of strong upper bounds, as well as lower bounds, both for qualitative problems (is the probability = 1, or = 0?), and for quantitative problems (is the probability ≥ p?, or, approximate the probability to within a desired precision). The complexity upper bounds we obtain for automata and LTL properties are similar, although the algorithms are different.

We present algorithms for the qualitative model checking problem that run in
polynomial space in the size |A| of the RMC and exponential time in the size of
the property (the automaton or the LTL formula). For several classes of RMCs,
including single-exit RMCs (a class that encompasses some well-studied stochastic models, e.g., stochastic context-free grammars) the algorithm runs in polynomial time in |A|. For the quantitative model checking problem, we present algorithms that run in polynomial space in the RMC and exponential space in the property. For the class of linearly recursive RMCs we can compute the exact probability in time polynomial in the RMC and exponential in the property. For deterministic automata specifications, all our complexities in the specification come down by one exponential.

For lower bounds, we show that the qualitative model checking problem, even for a fixed RMC, is already EXPTIME-complete. On the other hand, even for simple reachability analysis, we showed in [EY05a] that our PSPACE upper bounds in A can not be improved substantially without a breakthrough on a well-known open problem in the complexity of numerical computation.