Promt: Probably the Best Moment to Terminate

Uncertainty is everywhere - whether it concerns software, economy, health, or a global pandemic. In times of uncertainty, the only plausible way to act is relying on probabilities, allowing us to minimize the many "what-ifs" of tomorrow. Probabilistic programs emerged to capture a variety of possible outcomes and not necessarily only worst-case scenarios of the digital applications of cybersecurity, AI, cyber physical systems, and many others.

Promt opens new grounds and studies fundamental algorithmic questions related to probabilistic programs, most of these questions being open for many decades. We are motivated by applications of computer-aided verification and are interested in modeling, deciding, and automating the termination analysis of probabilistic programs, ensuring that these programs behave as expected. 

Promt dramatically alters the algorithmic theory of probabilistic termination and provides easy-to-use tool support for certifying termination of probabilistic loops. We model probabilistic choices via nested control flow with nondeterminism, in connections to control theory. We determine conditions under which probabilistic termination is decidable or as hard as open problems, such as the Skolem problem from number theory. We automate the reasoning for probabilistic termination by summarizing loop semantics as (probabilistic) recurrences in tight connections with probabilistic bound computation.

Our results are  supported by the development of our probabilistic analyzer Polar, minimizing expert knowledge requirements and lowering entry barriers to use termination analysis in the pipeline of probabilistic software development.

The complementary expertise of our PIs in cyber-physical systems, algorithmic verification, and automated reasoning places us in a unique position to achieve major breakthroughs in probabilistic termination. We request funding for 3 PhD students and foresee close collaborations with MPI-SWS, RWTH Aachen and Saarland University.