Eleanore Meyer: Automated Complexity Analysis of Probabilistic Programs

 

In recent years, the study of probabilistic programs and methods to ensure their correctness has been an active field of research. Probabilistic programs are classical programs that are enriched with a notion of probabilistic choice. Such programs may then for instance branch on the outcome of a coin flip or assign a value that is sampled according to a probability distribution to a program variable.

One of the most important correctness properties of programs is their termination behaviour.
When compared to classical programs the termination behaviour of their probabilistic counterparts is much more nuanced.
One distinguishes between almost surely terminating (AST) programs, i.e., programs that terminate with probability 1 and positively almost surely terminating (PAST) programs that are characterised by the finiteness of their expected time to termination.

In this project, we focus on the development of algorithms and techniques for the automated computation of (non-trivial) bounds on the expected time to termination.
Such bounds can be interpreted as a measure of the efficiency of the analysed programs.
Moreover, a finite bound guarantees the analysed program to satisfy PAST as well as AST (since PAST implies AST). Probabilistic ranking functions, a variant of ranking functions adapted for probabilistic programs based on the theory of ranking supermartingales (RSM), present a natural way to obtain bounds on the expected time to termination.

In recently published work [TACAS '21], we introduced the concept of expected sizes of program variables. Moreover, we presented a novel modular approach for the computation of (upper) bounds on the expected time to termination in a fully automated fashion by combining bounds on the expected time to termination for parts of the program with bounds on the expected variable sizes.

In ongoing work we are looking at possible improvements to the expressiveness of probabilistic ranking functions to extend the applicability of our approach. While lexicographic variants of RSMs already exist, there is, to the best of our knowledge, no equivalent of so-called multiphase-linear ranking functions (MΦRFs).
In recently published work, we have already integrated the nonprobabilistic version of MΦRFs into our automated complexity analysis tool KoAT to greatly improve its strength.

For deterministic programs there are classes of non-trivial loops for which termination is known to be decidable. Another area of interest is to investigate whether similar classes, which would allow the decidability of AST, exist in the case of probabilistic programs.