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).

REFERENCES

• 1: Steven Abney , David McAllester , Fernando Pereira, Relating probabilistic grammars and automata, Proceedings of the 37th annual meeting of the Association for Computational Linguistics on Computational Linguistics, p.542-549, June 20-26, 1999, College Park, Maryland [doi>10.3115/1034678.1034759]
• 2: Eric Allender , Peter Burgisser , Johan Kjeldgaard-Pedersen , Peter Bro Miltersen, On the Complexity of Numerical Analysis, Proceedings of the 21st Annual IEEE Conference on Computational Complexity, p.331-339, July 16-20, 2006 [doi>10.1109/CCC.2006.30]
• 3: Rajeev Alur , Michael Benedikt , Kousha Etessami , Patrice Godefroid , Thomas Reps , Mihalis Yannakakis, Analysis of recursive state machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.4, p.786-818, July 2005 [doi>10.1145/1075382.1075387]
• 4: Rajeev Alur , Kousha Etessami , Mihalis Yannakakis, Analysis of Recursive State Machines, Proceedings of the 13th International Conference on Computer Aided Verification, p.207-220, July 18-22, 2001
• 5: Rajeev Alur , Mihalis Yannakakis, Model checking of hierarchical state machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.273-303, May 2001 [doi>10.1145/503502.503503]
• 6: E. M. Arkin , C. H. Papadimitriou , M. Yannakakis, Modularity of cycles and paths in graphs, Journal of the ACM (JACM), v.38 n.2, p.255-274, April 1991 [doi>10.1145/103516.103517]
• 7: Athreya, K. B., and Ney, P. E. 1972. Branching processes. Springer-Verlag, Berlin, Germany.
• 8: Athreya, K. B., and Vidyashankar, A. N. 2001. Branching processes. In Stochastic Processes: Theory and Methods. Handbook of Statist., vol. 19. North-Holland, Amsterdam, the Netherlands, 35--53.
• 9: Balcer, Y., and Veinott, A. F. 1973. Computing a graph's period quadratically by node condensation. Disc. Math. 4, 295--303.
• 10: Saugata Basu , Richard Pollack , Marie-Françoise Roy, On the combinatorial and algebraic complexity of quantifier elimination, Journal of the ACM (JACM), v.43 n.6, p.1002-1045, Nov. 1996 [doi>10.1145/235809.235813]
• 11: Saugata Basu , Richard Pollack , Marie-Françoise Roy, Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics), Springer-Verlag New York, Inc., Secaucus, NJ, 2006
• 12: Michael Benedikt , Patrice Godefroid , Thomas W. Reps, Model Checking of Unrestricted Hierarchical State Machines, Proceedings of the 28th International Colloquium on Automata, Languages and Programming,, p.652-666, July 08-12, 2001
• 13: Alberto Bertoni , Giancarlo Mauri , Nicoletta Sabadini, A characterization of the class of functions computable in polynomial time on Random Access Machines, Proceedings of the thirteenth annual ACM symposium on Theory of computing, p.168-176, May 11-13, 1981, Milwaukee, Wisconsin, United States [doi>10.1145/800076.802470]
• 14: Lenore Blum , Felipe Cucker , Michael Shub , Steve Smale, Complexity and real computation, Springer-Verlag New York, Inc., Secaucus, NJ, 1997
• 15: T. L. Booth , R. A. Thompson, Applying Probability Measures to Abstract Languages, IEEE Transactions on Computers, v.22 n.5, p.442-450, May 1973 [doi>10.1109/T-C.1973.223746]
• 16: Ahmed Bouajjani , Javier Esparza , Oded Maler, Reachability Analysis of Pushdown Automata: Application to Model-Checking, Proceedings of the 8th International Conference on Concurrency Theory, p.135-150, July 01-04, 1997
• 17: Tomas Brazdil , Javier Esparza , Antonin Kucera, Analysis and Prediction of the Long-Run Behavior of Probabilistic Sequential Programs with Recursion (Extended Abstract), Proceedings of the 46th Annual IEEE Symposium on Foundations of Computer Science, p.521-530, October 23-25, 2005 [doi>10.1109/SFCS.2005.19]
• 18: Brázdil, T., Kučera, A., and Stražovský, O. 2005b. Decidability of temporal properties of probabilistic pushdown automata. In Proceedings of the 22nd Symposium on Theoretical Aspects of Computer Science (STACS).
• 19: John Canny, Some algebraic and geometric computations in PSPACE, Proceedings of the twentieth annual ACM symposium on Theory of computing, p.460-469, May 02-04, 1988, Chicago, Illinois, United States [doi>10.1145/62212.62257]
• 20: Zhiyi Chi , Stuart Geman, Estimation of probabilistic context-free grammars, Computational Linguistics, v.24 n.2, June 1998
• 21: Durbin, R., Eddy, S. R., Krogh, A., and Mitchison, G. 1999. Biological Sequence Analysis: Probabilistic models of Proteins and Nucleic Acids. Cambridge Univ., Press, Cambridge, MA.
• 22: Javier Esparza , David Hansel , Peter Rossmanith , Stefan Schwoon, Efficient Algorithms for Model Checking Pushdown Systems, Proceedings of the 12th International Conference on Computer Aided Verification, p.232-247, July 15-19, 2000
• 23: Esparza, J., Kiefer, S., and Luttenberger, M. 2008. Convergence thresholds of Newton's method for monotone polynomial equations. In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science (STACS). 289--300.
• 24: Javier Esparza , Antonin Kucera , Richard Mayr, Model Checking Probabilistic Pushdown Automata, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, p.12-21, July 13-17, 2004 [doi>10.1109/LICS.2004.23]
• 25: Javier Esparza , Antonin Kucera, Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, p.117-126, June 26-29, 2005 [doi>10.1109/LICS.2005.39]
• 26: Kousha Etessami , Dominik Wojtczak , Mihalis Yannakakis, Quasi-Birth-Death Processes, Tree-Like QBDs, Probabilistic 1-Counter Automata, and Pushdown Systems, Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems, p.243-253, September 14-17, 2008 [doi>10.1109/QEST.2008.35]
• 27: Etessami, K., and Yannakakis, M. 2005a. Algorithmic verification of recursive probabilistic state machines. In Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 253--270.
• 28: Etessami, K., and Yannakakis, M. 2005b. Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. In Proceedings of the 22nd Symposium on Theoretical Aspects of Computer Science (STACS). 340--352.
• 29: Etessami, K., and Yannakakis, M. 2005c. Recursive Markov decision processes and recursive stochastic games. In Proceedings of the 32nd International Colloquium on Automata, Languages, and Programming (ICALP). 891--903.
• 30: Etessami, K., and Yannakakis, M. 2006a. Efficient analysis of classes of recursive Markov decision processes and stochastic games. In Proceedings of the 23rd Symposium on Theoretical Aspects of Computer Science (STACS). 634--645.
• 31: Etessami, K., and Yannakakis, M. 2006b. Recursive concurrent stochastic games. In Proceedings of the 33rd International Colloquium on Automata, Languages, and Programming (ICALP). 324--335.
• 32: Kousha Etessami , Mihalis Yannakakis, On the Complexity of Nash Equilibria and Other Fixed Points (Extended Abstract), Proceedings of the 48th Annual IEEE Symposium on Foundations of Computer Science, p.113-123, October 21-23, 2007 [doi>10.1109/FOCS.2007.48]
• 33: Everett, C. J., and Ulam, S. 1948. Multiplicative systems, Part I., II, and III. Tech. Rep. 683,690,707, Los Alamos Scientific Laboratory.
• 34: Ronald Fagin , Anna R. Karlin , Jon Kleinberg , Prabhakar Raghavan , Sridhar Rajagopalan , Ronitt Rubinfeld , Madhu Sudan , Andrew Tomkins, Random walks with “back buttons” (extended abstract), Proceedings of the thirty-second annual ACM symposium on Theory of computing, p.484-493, May 21-23, 2000, Portland, Oregon, United States [doi>10.1145/335305.335362]
• 35: M. R. Garey , R. L. Graham , D. S. Johnson, Some NP-complete geometric problems, Proceedings of the eighth annual ACM symposium on Theory of computing, p.10-22, May 03-05, 1976, Hershey, Pennsylvania, United States [doi>10.1145/800113.803626]
• 36: Grenander, U. 1976. Lectures on Pattern Theory, Vol. 1. Springer-Verlag.
• 37: Grötschel, M., Lovász, L., and Schrijver, A. 1993. Geometric Algorithms and Combinatorial Optimization, 2nd ed. Springer-Verlag, Berlin, Germany.
• 38: Haccou, P., Jagers, P., and Vatutin, V. A. 2005. Branching Processes: Variation, Growth, and Extinction of Populations. Cambridge Univ. Press, Cambridge, UK.
• 39: Harris, T. E. 1963. The Theory of Branching Processes. Springer-Verlag, Berlin, Germany.
• 40: John E. Hopcroft , Rajeev Motwani , Rotwani , Jeffrey D. Ullman, Introduction to Automata Theory, Languages and Computability, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 41: Roger A. Horn , Charles R. Johnson, Matrix analysis, Cambridge University Press, New York, NY, 1985
• 42: Jagers, P. 1975. Branching Processes with Biological Applications. Wiley, New York.
• 43: Valentine Kabanets , Russell Impagliazzo, Derandomizing polynomial identity tests means proving circuit lower bounds, Proceedings of the thirty-fifth annual ACM symposium on Theory of computing, June 09-11, 2003, San Diego, CA, USA [doi>10.1145/780542.780595]
• 44: Karlin, S. 1966. A First Course in Stochastic Processes. Academic Press, Orlando, FL.
• 45: Stefan Kiefer , Michael Luttenberger , Javier Esparza, On the convergence of Newton's method for monotone systems of polynomial equations, Proceedings of the thirty-ninth annual ACM symposium on Theory of computing, June 11-13, 2007, San Diego, California, USA [doi>10.1145/1250790.1250822]
• 46: Kimmel, M., and Axelrod, D. E. 2002. Branching processes in biology. Springer-Verlag, Berlin, Germany.
• 47: Kolmogorov, A. N., and Sevastyanov, B. A. 1947. The calculation of final probabilities for branching random processes. Dokaldy 56, 783--786. (Russian).
• 48: Lancaster, P., and Tismenetsky, M. 1985. The Theory of Matrices, 2nd ed. Academic Press, Orlando, FL.
• 49: Latouche, G., and Ramaswami, V. 1999. Introduction to Matrix Analytic Methods in Stochastic Modeling. ASA-SIAM series on statistics and applied probability.
• 50: Christopher D. Manning , Hinrich Schütze, Foundations of statistical natural language processing, MIT Press, Cambridge, MA, 1999
• 51: Mode, C. J. 1971. Multitype Branching Processes. Theory and Applications. Modern Analytic and Computational Methods in Science and Mathematics, No. 34. American Elsevier.
• 52: Nederhof, M. J., and Satta, G. 2008. Computing partition functions of PCFGs. Res. Lang. Computat. 6, 2, 139--162.
• 53: Neuts, M. F. 1981. Matrix-Geometric Solutions in Stochastic Models:an algorithmic approach. Johns Hopkins Univ. Press, Baltimore, MD.
• 54: James M. Ortega , Werner C. Rheinboldt, Iterative solution of nonlinear equations in several variables, Society for Industrial and Applied Mathematics, Philadelphia, PA, 2000
• 55: James Renegar, On the computational complexity and geometry of the first-order theory of the reals. Part III: quantifier elimination, Journal of Symbolic Computation, v.13 n.3, p.329-352, March 1992
• 56: Reps, T. 1998. Program analysis via graph reachability. Inf. Softw. Tech. 40, 11-12, 701--726.
• 57: Sakakibara, Y., Brown, M., Hughey, R., Mian, I., Sjolander, K., Underwood, R., and Haussler, D. 1994. Stochastic context-free grammars for tRNA modeling. Nuc. Acids Res. 22, 23, 5112--5120.
• 58: Arnold Schönhage, On the Power of Random Access Machines, Proceedings of the 6th Colloquium, on Automata, Languages and Programming, p.520-529, July 16-20, 1979
• 59: Sevastyanov, B. A. 1951. The theory of branching processes. Uspehi Mathemat. Nauk 6, 47--99. (Russian).
• 60: Stewart, I. 1989. Galois Theory, 2nd ed. Chapman & Hall, London, UK.
• 61: Stoer, J., and Bulirsch, R. 1993. Introduction to Numerical Analysis. Springer-Verlag, Berlin, Germany.
• 62: Prasoon Tiwari, A problem that is easier to solve on the unit-cost algebraic RAM, Journal of Complexity, v.8 n.4, p.393-397, Dec. 1992 [doi>10.1016/0885-064X(92)90003-T]
• 63: Wojtczak, D., and Etessami, K. 2007. Premo: An analyzer for probabilistic recursive models. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 66--71.
• 64: Mihalis Yannakakis , Kousha Etessami, Checking LTL Properties of Recursive Markov Chains, Proceedings of the Second International Conference on the Quantitative Evaluation of Systems, p.155, September 19-22, 2005 [doi>10.1109/QEST.2005.8]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY

Additional Classification:
  G. Mathematics of Computing
  G.1 NUMERICAL ANALYSIS
      G.1.5 Roots of Nonlinear Equations
          Subjects: Systems of equations
  G.3 PROBABILITY AND STATISTICS
      Subjects: Stochastic processes

General Terms:
Algorithms, Theory, Verification

Keywords:
Newton's method, Recursive Markov chains, monotone nonlinear systems, multi-type branching processes, stochastic context-free grammars