一句话：揭示概率下推自动机证书存在性与期望终止时间的联系，并给出正几乎必然终止的易验证证明。
本文研究概率下推自动机（pPDA）定量性质上下界的证书，即简洁且易于验证的证明。作者建立证书存在性与 pPDA 期望终止时间之间的紧密而简单的联系，并通过分析底层多项式方程系统雅可比矩阵的谱半径等内在性质，说明它们直接决定期望运行时间。作为推论，对于“pPDA 是否以有限期望时间终止”这一正几乎必然终止问题，总存在易于检查的证明。
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?
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{abs-2304-09997,
title = {On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata},
author = {Tobias Winkler and Joost-Pieter Katoen},
booktitle = {LICS},
year = {2023},
doi = {10.1109/lics56636.2023.10175714}
}