Abstract
A central computational problem for analyzing and model checking various classes of infinitestate recursive probabilistic systems (including quasibirthdeath processes, multitype branching processes, stochastic contextfree grammars, probabilistic pushdown automata and recursive Markov chains) is the computation of termination probabilities, and computing these probabilities in turn boils down to computing the least fixed point(LFP) solution of a corresponding monotone polynomial system (MPS) of equations, denoted x=P(x).
It was shown in [Etessami and Yannakakis 2009] that a decomposed variant of Newton’s method converges monotonically to the LFP solution for any MPS that has a nonnegative solution. Subsequently, [Esparza et al. 2010] 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 ([Etessami et al. 2010; Etessami et al. 2012]).
However, prior to this paper, for arbitrary (not necessarily stronglyconnected) 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 worstcase upper bounds, as a function of both the input encoding size P, and ε >0, on the number of iterations required for decomposed Newton’s method (even with rounding) to converge to within additive error ε > 0 of q* , for an arbitrary MPS with LFP solution q*. Our upper bounds are essentially optimal in terms of several important parameters of the problem.
Using our upper bounds, and building on prior work, we obtain the first Ptime algorithm (in the standard Turing model of computation) for quantitative model checking, to within arbitrary desired precision, of discretetime QBDs and (equivalently) probabilistic 1counter automata, with respect to any (fixed) ωregular or LTL property.
It was shown in [Etessami and Yannakakis 2009] that a decomposed variant of Newton’s method converges monotonically to the LFP solution for any MPS that has a nonnegative solution. Subsequently, [Esparza et al. 2010] 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 ([Etessami et al. 2010; Etessami et al. 2012]).
However, prior to this paper, for arbitrary (not necessarily stronglyconnected) 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 worstcase upper bounds, as a function of both the input encoding size P, and ε >0, on the number of iterations required for decomposed Newton’s method (even with rounding) to converge to within additive error ε > 0 of q* , for an arbitrary MPS with LFP solution q*. Our upper bounds are essentially optimal in terms of several important parameters of the problem.
Using our upper bounds, and building on prior work, we obtain the first Ptime algorithm (in the standard Turing model of computation) for quantitative model checking, to within arbitrary desired precision, of discretetime QBDs and (equivalently) probabilistic 1counter automata, with respect to any (fixed) ωregular or LTL property.
Original language  English 

Article number  30 
Number of pages  33 
Journal  Journal of the ACM 
Volume  62 
Issue number  4 
DOIs  
Publication status  Published  11 Sep 2015 
Fingerprint
Dive into the research topics of 'Upper Bounds for Newton's Method on Monotone Polynomial Systems, and Ptime Model Checking of Probabilistic OneCounter Automata'. Together they form a unique fingerprint.Profiles

Kousha Etessami
 School of Informatics  Personal Chair in Algorithms, Games, Logic and Complexity
 Laboratory for Foundations of Computer Science
 Foundations of Computation
Person: Academic: Research Active