Probabilistic pushdown automata (pPDA) are a natural operational model for a variety of recursive discrete stochastic processes. In this paper, we study certificates - succinct and easily verifiable proofs - for upper and lower bounds on various quantitative properties of a given pPDA. We reveal an intimate, yet surprisingly simple connection between the existence of such certificates and the expected time to termination of the pPDA at hand. This is established by showing that certain intrinsic properties, like the spectral radius of the Jacobian of the pPDA's underlying polynomial equation system, are directly related to expected runtimes. As a consequence, we obtain that there always exist easy-to-check proofs for positive almost-sure termination: does a pPDA terminate in finite expected time?

翻译：概率下推自动机（pPDA）是多种递归离散随机过程的一种自然操作模型。本文研究了针对给定pPDA的多种定量性质上下界的证书——即简洁且易于验证的证明。我们揭示了此类证书的存在性与pPDA当前期望终止时间之间一种紧密且出人意料的简单联系。这一结论通过证明某些内在性质（如pPDA底层多项式方程系统的雅可比矩阵的谱半径）与期望运行时间直接相关而得以建立。由此，我们得出：对于正向几乎必然终止性（即pPDA是否在有限期望时间内终止？），总存在易于检验的证明。