Dominik Meier: Termination and Complexity Analysis of Probabilistic Programs


Using random actions or selections is a very useful ingredient for the development of algorithms. It is typically used to change deterministic algorithms with bad worst-case behaviour into efficient random algorithms which produce correct results with a high probability. The Rabin-Miller primality test, Freivalds’ matrix multiplication, andthe random pivot selection in Hoare’s quicksort algorithm are prime examples. These kinds of algorithms can be elegantly expressed as probabilistic programs. Determining runtimeand termination in the probabilistic case is a difficult problem with often unintuitive results. In the probabilistic case there are multiple notions of termination. Two of the most important ones are Almost Sure Termination (AST), i.e., the program terminates with probability 1, and (Strong) Positive Almost Sure Termination (PAST), i.e., the program terminates with a finite number of expected steps.
While PAST is theoretically harder, AST is often considered more difficult to prove. Whereas in the deterministic case a single diverging infinite run leads to non-termination and infinite runtime, this is not the case for either notion of termination in the probabilistic case.
The project “Termination and Complexity Analysis of Probabilistic Programs” deals with the challenging question of how to automatically determine the respective properties of probabilistic programs. There are approaches amenable to automation, but current techniques usually only focus on programs on numbers and disregard programs operating on data structures such as lists or trees. In contrast, in the non-probabilistic case, many powerful approaches have been developed to analyze termination and complexity of term rewriting systems automatically. Therefore, the focus of the project is on analyzing probabilistic term rewriting systems (PTRSs). Due to better properties regarding modularity, AST will be considered as the main notion of termination.
There are some results for PTRSs which use polynomial and matrix orders to determine PAST, but as with the non-probabilistic case, these techniques alone are not very powerful. The key idea for termination analysis in the classical case was the introduction of dependency pairs and the resulting possibility of a modular analysis of a term rewriting system. Therefore, one of the goals of this project is the adaptation of this analysis technique to the probabilistic case, in order to develop a fully automated technique for the termination analysis of PTRSs. Currently, in the project after having reviewed the state-of-the-art literature key challenges and requirements have been identified. Further, there has been significant progress in adapting the dependency pair technique to the probabilistic case.