Access Restriction

Author Stewart, Alistair ♦ Etessami, Kousha ♦ Yannakakis, Mihalis
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©2015
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Probability ♦ Model checking
Abstract A central computational problem for analyzing and model checking various classes of infinite-state recursive probabilistic systems (including quasi-birth-death processes, multitype branching processes, stochastic context-free 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 $\textit{x}=\textit{P}(\textit{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, 2012]. However, prior to this article, 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, $\textit{x}=\textit{P}(\textit{x}).$ In this article, we provide worst-case upper bounds, as a function of both the input encoding size |P|, and $\textit{ε}$ > 0, on the number of iterations required for decomposed Newton’s method (even with rounding) to converge to within additive error $\textit{ε}$ > 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 P-time algorithm (in the standard Turing model of computation) for quantitative model checking, to within arbitrary desired precision, of discrete-time QBDs and (equivalently) probabilistic 1-counter automata, with respect to any (fixed) $\textit{ω}-regular$ or LTL property.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2015-09-11
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 62
Issue Number 4
Page Count 33
Starting Page 1
Ending Page 33

Open content in new tab

   Open content in new tab
Source: ACM Digital Library