基于乐观值迭代的概率下推自动机证明
Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration
摘要：
概率下推自动机（probabilitypushdownautomata，pPDA）是离散概率程序的标准模型，它具有过程和递归的特点.在pPDA中，许多定量性质都被刻画为多项式方程组的最小不动点。在本文中，我们研究的问题，证明这些量位于一定的范围内。为此，我们首先描述了多项式系统，承认易于检查的证书验证其最小不动点的界限。其次，我们提出了一个健全的和完整的乐观值迭代算法计算这样的证书。第三，我们将展示如何证书多项式系统可以转移到证书的各种定量pPDA属性。实验表明，我们的算法计算简洁的证书，几个复杂的例子程序，以及随机上下文无关文法与$> 10^4$产生式规则。
英文摘要：
Probabilistic pushdown automata (pPDA) are a standard model for discrete probabilistic programs with procedures and recursion. In pPDA, many quantitative properties are characterized as least fixpoints of polynomial equation systems. In this paper, we study the problem of certifying that these quantities lie within certain bounds. To this end, we first characterize the polynomial systems that admit easy-to-check certificates for validating bounds on their least fixpoint. Second, we present a sound and complete Optimistic Value Iteration algorithm for computing such certificates. Third, we show how certificates for polynomial systems can be transferred to certificates for various quantitative pPDA properties. Experiments demonstrate that our algorithm computes succinct certificates for several intricate example programs as well as stochastic context-free grammars with $> 10^4$ production rules.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
