• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Computer aided verification >Upper Bounds for Newton's Method on Monotone Polynomial Systems, and P-Time Model Checking of Probabilistic One-Counter Automata
【24h】

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

机译：牛顿法在单调多项式系统上的上界和概率一计数器自动机的P时间模型检验

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

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 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 by Etessami and 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, and 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 ∈ ＞ 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 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) ω-regular or LTL property.
机译：分析和检查各种类型的无限状态递归概率系统（包括准出生死亡过程，多类型分支过程，随机上下文无关文法，概率下推自动机和递归马尔可夫链）的中心计算问题是计算终止概率的计算，然后计算这些概率归结为计算方程的单调多项式系统（MPS）的最小不动点（LFP）解，表示为x = P（x）。 Etessami和Yannakakis证明，对于具有非负解的任何MPS，牛顿方法的分解变体都单调收敛到LFP解。随后，Esparza，Kiefer和Luttenberger获得了某些类MPS的牛顿法收敛速度的上限。最近，对于特殊类别的MPS已经获得了更好的上限。但是，在此之前，对于任意（不一定是强连接的）MPS，牛顿法的收敛速度与编码大小| P |的函数完全没有上限。输入MPS的x = P（x）。在本文中，我们提供了最坏情况的上限，作为输入编码大小| P |和∈＞ 0的函数，用于分解牛顿法（即使使用舍入法）收敛到加法误差内所需的迭代次数对于具有LFP解q〜*的任意MPS，q〜*的∈＞ 0。就问题的几个重要参数而言，我们的上限基本上是最佳的。利用我们的上限并在先前的工作基础上，我们获得了第一个P时间算法（在标准图灵计算模型中），用于在任意期望的精度内对离散时间QBD和（等效）概率1进行定量模型检查关于任何（固定）ω-常规或LTL属性的自动计数器。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号