Upper Bounds for Newton’s Method on Monotone Polynomial Systems, and P-Time Model Checking of Probabilistic One-Counter Automata

摘要

A central computational problem for analyzing and model checking variousclasses of infinite-state recursive probabilistic systems (includingquasi-birth-death processes, multi-type branching processes, stochasticcontext-free grammars, probabilistic pushdown automata and recursive Markovchains) is the computation of {em termination probabilities}, and computingthese probabilities in turn boils down to computing the {em least fixed point}(LFP) solution of a corresponding {em monotone polynomial system} (MPS) ofequations, denoted x=P(x). It was shown by Etessami & Yannakakis that a decomposed variant of Newton'smethod converges monotonically to the LFP solution for any MPS that has anon-negative solution. Subsequently, Esparza, Kiefer, & Luttenberger obtainedupper bounds on the convergence rate of Newton's method for certain classes ofMPSs. More recently, better upper bounds have been obtained for special classesof MPSs. However, prior to this paper, for arbitrary (not necessarilystrongly-connected) MPSs, no upper bounds at all were known on the convergencerate of Newton's method as a function of the encoding size |P| of the inputMPS, x=P(x). In this paper we provide worst-case upper bounds, as a function of both theinput encoding size |P|, and epsilon > 0, on the number of iterations requiredfor decomposed Newton's method (even with rounding) to converge within additiveerror epsilon > 0 of q^*, for any MPS with LFP solution q^*. Our upper boundsare essentially optimal in terms of several important parameters. Using our upper bounds, and building on prior work, we obtain the firstP-time algorithm (in the standard Turing model of computation) for quantitativemodel 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.