Promt: Probably the Best Moment to Terminate

Promt is a WWTF funded project, aiming to answer fundamental algorithmic questions related to verification of probabilistic programs. It is a joint project between IST Austria and the FORSYTE and TrustCPS groups from TU Wien. The project is split into three workpackages, each led by a principal investigator from one of the groups.

Workpackages

Controlling Termination

Lead: Ezio Bartocci

Termination of probabilistic loops can be certified through proof rules that require finding expressions that satisfy certain conditions.

Synthesizing such expressions is undecidable in general and current approaches can fail even for simple programs. We will develop “relaxed” proof rules for termination for certain classes of programs, and develop new synthesis techniques.

Ruling Hardness

Lead: Krishnendu Chatterjee

For some classes of probabilistic systems termination is a (semi-)decidable property. These decidable fragments are, however, limited in their expresivity. When allowing more expressive program models it can become possible to encode for example the Skolem-Problem in the program.

We will study the decidability/hardness of termination of more expressive probabilistic programs, in particular also focusing on certificates for those programs.

Moments to Terminate

Lead: Laura Kovács

For programs with restricted control flow it is possible to compute the Moments of program variables, and thus the expected value of polynomial expressions algebraically. Those expressions can in some cases be used to analyze the termination behavior of programs.

We will study systematically when and how Moment-computability can be leveraged in termination analysis, for example through concentration inequalities.