Algorithmic Verification of Recursive Probabilistic State Machines

Recursive Markov Chains (RMCs) ([EY05]) 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 multi-type branching (stochastic) processes. In this paper, we study the problem of model checking an RMC against a given

ω

-regular specification. Namely, given an RMC

A

and a Büchi automaton

B

, we wish to know the probability that an execution of

A

is accepted by

B

. 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). Among these, we show that qualitative model checking for general RMCs can be decided in PSPACE in |

A

| and EXPTIME in |

B

|, and when

A

is either a single-exit RMC or when the total number of entries and exits in

A

is bounded, it can be decided in polynomial time in |

A

|. We then show that quantitative model checking can also be done in PSPACE in |

A

|, and in EXPSPACE in |

B

|. When

B

is deterministic, all our complexities in |

B

| come down by one exponential.

For lower bounds, we show that the qualitative model checking problem, even for a fixed RMC, is EXPTIME-complete. On the other hand, even for reachability analysis, we showed in [EY05] that our PSPACE upper bounds in

A

can not be improved upon without a breakthrough on a well-known open problem in the complexity of numerical computation.