  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?

Formal Languages and Automata Theory;Logic in Computer Science