Tobias Winkler: Programming and Verifying Uncertain Phenomena

 

In recent years, programming languages have been enhanced with probabilistic constructs, allowing programmers to write statements like “Flip a fair coin, if heads comes up then increment variable x by 1” or “If two processes A and B are in the same state, then process B crashes with probability 5%”. It is important to understand that this extra randomness does not present a contradiction to the unambiguous nature of programming languages: Instead of yielding a predetermined output like classical programs, a probabilistic program typically results in a predetermined probability distribution over possible outputs. The following are important use cases of probabilistic programs:

Randomized Algorithms are traditional algorithms extended with coin flips to increase performance or enable realizability of certain computational tasks. The latter is especially the case for computations distributed among several agents [1]. Such algorithms are meant to be actually implemented and run on a physical machine, often using a pseudo-random number generator.

Probabilistic Model Checking aims at verifying behavioural properties of processes involving randomness. The process under consideration is usually modelled by means of a probabilistic program. Often, the purpose of the program is not to be actually executed but to describe the process of interest in a precise mathematical manner. Application areas include verification of randomised—often distributed— algorithms (internal randomness), systems making decisions in an uncertain environment (external randomness), biological processes and many more. A distinguishing feature of model checking is that the program at hand is typically (but not always) finite-state. This enables exact algorithmic solvability (decidability) of almost all properties of interest by constructing a finite low-level model of the process such as a continuous- or discrete-time Markov chain, a Markov Decision Process, a stochastic game and others. See [2] for an overview of the field.

Probabilistic Programming (e.g. [3]) is a relatively new paradigm that aims to automate statistical inference. Similar to model checking, programs of the corresponding languages are not meant to be run directly but rather to describe a process in which unknown events may occur. The purpose of a Probabilistic Programming System is to automatically infer the likelihood of those events given observations about the outcome (or intermediate stages) of the process. It can, thus, be seen as an automated approach to Bayesian statistics, and it generalizes traditional graphical models such as Bayesian networks. Languages for Probabilistic Programming typically support continuous probability distributions and have additional primitives for observations. In general, inference can only be done approximately, using sampling based approaches.

These three directions are closely related. Moreover, program verification is key in all of them: While this is obvious for Randomised Algorithms and Probabilistic Model Checking, it turns out that verification and inference mostly coincide in the case of Probabilistic Programming.

The aim of my research is twofold:

1. To help foster a common theoretical basis for the three areas: More specifically I am interested in the development of new verification logics in the spirit of classical Hoare logic and weakest precondition transformers [4,5] to facilitate and systemize the verification tasks mentioned above. This is closely related to program semantics—mathematical definitions of the meaning of a program—as different approaches to semantics lead to different verification rules. Together with my co-authors, we have recently proposed Weighted Programming as a generalization of probabilistic programs which facilitates encoding a range of mathematical programs (beyond Bayesian inference) as program verification tasks and thus allows to apply standard techniques such as loop invariants [13].
2. Contributions to the ample field of Probabilistic Model Checking, more concretely:
   1. Stochastic games. Such games arise from controlled stochastic processes, additionally faced with unquantifiable uncertain external events, i.e., events whose occurrence cannot be described be means of probabilities, e.g. because relevant statistical data is unavailable. I have investigated the two-player turn-based variant of such games under various non-standard multi-objectives [8,9,10].
   2. Recursive stochastic processes. These are naturally described by imperative probabilistic languages allowing (mutually) recursive function calls. I work on Model Checking finite-state versions of such programs, so called Probabilistic Pushdown Automata [7]. In particular, I am interested in verifying temporal properties [11] and proving termination.
   3. Program rewriting. Another direction where I have done some work is to rewrite probabilistic programs prior to Model Checking with the aim of simplifying the latter task, in particular by decreasing the size of the resulting finite-state model [12].

References

• 1] Ted Herman. Probabilistic Self-Stabilization. Inf. Process. Lett. 35(2), p. 63-67 (1990)
  [2] Joost-Pieter Katoen. The Probabilistic Model Checking Landscape. LICS 2016, p. 31-45 (2016)
  [3] Andrew D. Gordon et al. Probabilistic Programming. FOSE 2014, p. 167-181 (2014)
  [4] Annabelle McIver and Carrol Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science, Springer 2005, ISBN 978-0-387-40115-7 (2005)
  [5] Benjamin L. Kaminski. Advanced weakest precondition calculi for probabilistic programs. PhD Thesis (RWTH Aachen University), Germany, (2019)
  [6] Taolue Chen et al. On Stochastic Games with Multiple Objectives. MFCS 2013, p. 266-277 (2013)
  [7] Javier Esparza et al. Model Checking Probabilistic Pushdown Automata. LICS 2004, p. 12-21 (2004)
  [8] C. Chatterjee, J.-P. Katoen, M. Weininger, T. Winkler. Stochastic Games with Lexicographic Reachability-Safety Objectives. CAV 2020.
  [9] P. Ashok, C. Chatterjee,J. Kretinsky, M. Weininger, T. Winkler. Approximating Values of Generalized-Reachability Stochastic Games. LICS 2020.
  [10] T. Winkler and M. Weininger. Stochastic Games with Disjunctions of Multiple Objectives. GandALF 2021.
  [11] T. Winkler, C. Gehnen, J.-P. Katoen. Model Checking Temporal Properties of Probabilistic Recursive Programs. FoSSaCS 2022.
  [12] T. Winkler, J. Lehmann, J.-P. Katoen. Out of Control: Reducing probabilistic Models by Control-State Elimination. VMCAI 2022.
  [13] K. Batz, A. Gallus, B. Kaminski, J.-P. Katoen, T. Winkler. Weighted Programming - A Programming Paradigm for Specifying Mathematical Models. OOPSLA 2022.