Checking LTL Properties of Recursive Markov Chains

Abstract We present algorithms for the qualitative and quantita-tive model checking of Linear Temporal Logic (LTL) properties for Recursive Markov Chains (RMCs). RecursiveMarkov Chains are a natural abstract model of procedural probabilistic programs and related systems involving recur-sion and probability. For the qualitative problem ("Given a RMC A and an LTL formula ', do the computationsof A satisfy ' almost surely?") we present an algorithmthat runs in polynomial space in A and exponential timein '. For several classes of RMCs, including RMCs withone exit (a special case that corresponds to well-studied probabilistic systems, e.g., multi-type branching processesand stochastic context-free grammars) the algorithm runs in polynomial time in A and exponential time in '. On theother hand, we also prove that the problem is EXPTIMEhard, and hence it is EXPTIME-complete. For the quan-titative problem ("does the probability that a computation of A satisfies ' exceed a given threshold p?", or approxi-mate the probability within a desired precision) we present an algorithm that runs in polynomial space in A and expo-nential space in '. For linearly-recursive RMCs, we cancompute the exact probability in time polynomial in A andexponential in '. These results improve by one exponential,in both the qualitative and quantitative case, the complexity that one would obtain if one first translated the LTL formulato a B"uchi automaton and then applied the model checking algorithm for B"uchi automata from [11]. Our results com-bine techniques developed in [10, 11] for analysis of RMCs, and in [6] for LTL model checking of flat Markov Chains,and extend them with new techniques