Upper bounds for Newton's method on monotone polynomial systems, and P-time model checking of probabilistic one-counter automata

DOI10.1145/2789208zbMATH Open1426.68177arXiv1302.3741OpenAlexW2143473941MaRDI QIDQ3177734FDOQ3177734

Mihalis Yannakakis, Alistair Stewart, Kousha Etessami

Publication date: 2 August 2018

Published in: Journal of the ACM (Search for Journal in Brave)

Abstract: A central computational problem for analyzing and model checking various classes of infinite-state recursive probabilistic systems (including quasi-birth-death processes, multi-type branching processes, stochastic context-free grammars, probabilistic pushdown automata and recursive Markov chains) is the computation of {em termination probabilities}, and computing these probabilities in turn boils down to computing the {em least fixed point} (LFP) solution of a corresponding {em monotone polynomial system} (MPS) of equations, denoted x=P(x). It was shown by Etessami & Yannakakis that a decomposed variant of Newton's method converges monotonically to the LFP solution for any MPS that has a non-negative solution. Subsequently, Esparza, Kiefer, & Luttenberger obtained upper bounds on the convergence rate of Newton's method for certain classes of MPSs. More recently, better upper bounds have been obtained for special classes of MPSs. However, prior to this paper, for arbitrary (not necessarily strongly-connected) MPSs, no upper bounds at all were known on the convergence rate of Newton's method as a function of the encoding size |P| of the input MPS, x=P(x). In this paper we provide worst-case upper bounds, as a function of both the input encoding size |P|, and epsilon > 0, on the number of iterations required for decomposed Newton's method (even with rounding) to converge within additive error epsilon > 0 of q^*, for any MPS with LFP solution q^*. Our upper bounds are essentially optimal in terms of several important parameters. Using our upper bounds, and building on prior work, we obtain the first P-time algorithm (in the standard Turing model of computation) for quantitative model checking, to within desired precision, of discrete-time QBDs and (equivalently) probabilistic 1-counter automata, with respect to any (fixed) omega-regular or LTL property.

Full work available at URL: https://arxiv.org/abs/1302.3741

Recommendations

• Convergence thresholds of Newton's method for monotone polynomial equations
• Computing the least fixed point of positive polynomial systems
• COMPUTING LEAST FIXED POINTS OF PROBABILISTIC SYSTEMS OF POLYNOMIALS
• Approximative Methods for Monotone Systems of Min-Max-Polynomial Equations
• Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations

zbMATH Keywords

model checkingprobability

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (7)

• Model Checking Temporal Properties of Recursive Probabilistic Programs
• A Polynomial Time Algorithm for Computing Extinction Probabilities of Multitype Branching Processes
• Polynomial Time Algorithms for Branching Markov Decision Processes and Probabilistic Min(Max) Polynomial Bellman Equations
• Shortest Paths in One-Counter Systems
• Efficient Analysis of Probabilistic Programs with an Unbounded Counter
• Certificates for probabilistic pushdown automata via optimistic value iteration
• Approximative Methods for Monotone Systems of Min-Max-Polynomial Equations

This page was built for publication: Upper bounds for Newton's method on monotone polynomial systems, and P-time model checking of probabilistic one-counter automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3177734)