概率下推自动机的乐观值迭代证书
摘要：基于概率的推下自动机（pPDA）是一个用于具有过程和递归的离散概率程序的标准模型。在pPDA中，许多数量特性被表征为多项式方程系统的最小不动点。本文研究了证明这些数量在一定范围内的问题。为此，我们首先确定了易于检查证明最小不动点边界的多项式系统。其次，我们提出了一种完备且可靠的乐观价值迭代算法，用于计算这样的证书。第三，我们展示了如何将多项式系统的证书转化为各种数量pPDA属性的证书。实验表明，我们的算法为许多复杂的示例程序以及具有超过$10^4$个产生式规则的随机上下文无关文法计算出简洁的证书。
作者：Tobias Winkler, Joost-Pieter Katoen
论文ID：2301.08657
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-02-28