On the algebraic analysis of runtime distribution of probabilistic programs

We present an algebraic method for analysing probabilistic programs with counters and discrete states, Generalised Constant Probability (GCP) programs. We define the operational semantics of GCP in terms of the runs of probabilistic one-counter automata (pOC), a type of probabilistic pushdown automata. We characterise the resulting (sub-)probability generating function (pgf) Δ(z) as an algebraic function, representable via the roots of a kernel polynomial associated with the program. Next, we provide algorithms that, leveraging this information, compute under mild algebraic conditions the dominant singularities and the exact radius of convergence of Δ(z), leading to an exact asymptotic expansion and to exponential bounds for its coefficients. Our approach is sound for GCP programs and complete for the single-state subclass.