Jan-Christoph Kassing: Analyzing Termination and Expected Runtime Complexity for Probabilistic Term Rewriting

 

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 behavior into efficient random algorithms which produce correct results with a high probability. The Rabin-Miller primality test, Freivalds’ matrix multiplication, and the random pivot selection in Hoare’s quicksort algorithm are prime examples. These kinds of algorithms can be elegantly expressed as probabilistic programs.

Determining runtime and 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 within a finite number of expected steps. 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.

There are approaches amenable to automation, but most current techniques only focus on programs on numbers and disregard programs operating on data structures such as lists or trees. In contrast, in the non-probabilistic setting, many powerful and automatic approaches have been developed to analyze termination and complexity of these types of programs using an automatic analysis of term rewriting systems.
The project “Analyzing Termination and Expected Runtime Complexity for Probabilistic Term Rewriting” deals with the challenging question of how to automatically determine the respective properties of probabilistic programs dealing with data structures. 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 adaption of this analysis technique to the probabilistic case, to develop a fully automated technique for the termination analysis of PTRSs. We have already created an adaption of the dependency pair framework to automatically analyze innermost AST, where we only consider rewrite sequences that follow an innermost evaluation strategy. Currently, we are investigating different ideas from the non-probabilistic framework on how to increase the effectiveness and applicability of our newly developed framework.