On the algebraic analysis of runtime distribution of probabilistic programs

Michele Boreale; Luisa Collodi; Alessandro Pompa Di Gregorio

On the algebraic analysis of runtime distribution of probabilistic programs

Formal Languages and Automata Theory 2026-07-02 v1

Authors: Michele Boreale , Luisa Collodi , Alessandro Pompa Di Gregorio

Abstract

We present an algebraic method for analyzing probabilistic programs with counters and discrete states, Generalized Constant Probability (GCP) programs. We define the operational semantics of GCP in terms of the runs of a type of probabilistic pushdown automata (pPDAs). We characterize the resulting (sub-)probability generating function (pgf) $\Delta(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 $\Delta(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.

Cite

@article{arxiv.2607.01856,
  title  = {On the algebraic analysis of runtime distribution of probabilistic programs},
  author = {Michele Boreale and Luisa Collodi and Alessandro Pompa Di Gregorio},
  journal= {arXiv preprint arXiv:2607.01856},
  year   = {2026}
}