Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations

Abstract

We define Recursive Markov Chains (RMCs), a class of finitely presented denumerable Markov chains, and we study algorithms for their analysis. Informally, an RMC consists of a collection of finite-state Markov chains with the ability to invoke each other in a potentially recursive manner. RMCs offer a natural abstract model for probabilistic programs with procedures. They generalize, in a precise sense, a number of well-studied stochastic models, including Stochastic Context-Free Grammars (SCFG) and Multi-Type Branching Processes (MT-BP). We focus on algorithms for reachability and termination analysis for RMCs: what is the probability that an RMC started from a given state reaches another target state, or that it terminates? These probabilities are in general irrational, and they arise as (least) fixed point solutions to certain (monotone) systems of nonlinear equations associated with RMCs. We address both the qualitative problem of determining whether the probabilities are 0, 1 or in-between, and the quantitative problems of comparing the probabilities with a given bound, or approximating them to desired precision. We show that all these problems can be solved in PSPACE using a decision procedure for the Existential Theory of Reals. We provide a more practical algorithm, based on a decomposed version of multi-variate Newton's method, and prove that it always converges monotonically to the desired probabilities. We show this method applies more generally to any monotone polynomial system. We obtain polynomial-time algorithms for various special subclasses of RMCs. Among these: for SCFGs and MT-BPs (equivalently, for 1-exit RMCs) the qualitative problem can be solved in P-time; for linearly recursive RMCs the probabilities are rational and can be computed exactly in P-time. We show that our PSPACE upper bounds cannot be substantially improved without a breakthrough on long standing open problems: the square-root sum problem and an arithmetic circuit decision problem that captures P-time on the unit-cost rational arithmetic RAM model. We show that these problems reduce to the qualitative problem and to the approximation problem (to within any nontrivial error) for termination probabilities of general RMCs, and to the quantitative decision problem for termination (extinction) of SCFGs (MT-BPs).