ABSTRACT. This tutorial introduces Flexible Nets, a novel modelling formalism for dynamic systems that can account for a number of parameter uncertainties and that facilitates the performance evaluation, optimization and control of the modelled systems. A Flexible Net is composed of two nets, an event net that captures how the processes of the system produce changes in its state, and an intensity net that models how the state induces speeds in the processes. These nets have three types of vertices: places (that model the state), transitions (that model processes), and handlers (that model the relationships between the state and the processes). Handlers can be equipped with inequalities in order to model system uncertainties, and optionally with piecewise linear functions to account for nonlinear dynamics. After introducing the main features of Flexible Nets, several net examples, including a resource allocation system, a partially observed system, and a biological system, will be presented together with some of the analysis, optimization and control possibilities that can be used. The last part of the tutorial will introduce the open-source Python tool fnyzer for the analysis of Flexible Nets.

[presentation video: part 1—Introduction, part 2—Intensity Nets, part 3—Guarded Flexible Nets, part 4—Tool fnyzer].

ABSTRACT. Probabilistic programs enrich computation with randomization by allowing ordinary programs to (a) sample from probability distributions and (b) condition such distributions on some observed evidence. They are finite representations of potentially infinite-state Markov chains.

Randomization in computation has been around at least since Rabin introduced probabilistic automata in the early 1960s. Its importance has been ever-growing since then. Randomization is an important tool for the design and analysis of efficient algorithms, serves as a tie-breaker in distributed protocols, and is ubiquitous in cybersecurity. At the moment, probabilistic programs are receiving fast-growing attention in artificial intelligence, where they serve as a powerful modeling formalism that is both more expressive and more accessible than classical graphical models.

In light of the increasing deployment of probabilistic systems, their correctness is paramount. Establishing the correctness of probabilistic systems, however, is notoriously difficult. Even the notion of correctness itself becomes blurred: A program that produces correct results with high probability may be perfectly adequate.

In this tutorial, we will give an in-depth introduction to the foundations of quantitative verification of probabilistic programs:

1. We present deductive techniques for verifying quantitative properties, such as both correctness and termination probabilities or expected runtimes. These techniques work directly on source-code level without explicitly constructing any Markov chain.
2. We discuss invariant-style reasoning for (potentially unbounded) probabilistic loops—the main cause of infinite state spaces.
3. We apply our techniques to automatically analyze expected simulation times of Bayesian networks—a popular graphical model in artificial intelligence.

[presentation video: part 1—Introduction, part 2—Weakest Preconditions, part 3—Reasoning about Loops, part 4—Expected Runtimes, part 5—Completeness & Bayesian Networks, part 6—Extensions].