qest logo

Jorge Júlvez
University of Cambridge, UK

Flexible nets

Monday, August 31.  10:30 – 13:30

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.

Jorge Júlvez is associate professor at the Department of Computer Science and Systems Engineering in the University of Zaragoza. Jorge received his M.S. and Ph.D. degrees in computer science engineering in 1998 and 2005 from the University of Zaragoza. His Ph.D. was related to the study of qualitative and quantitative properties of continuous Petri nets. In 2005 he joined, as a PostDoc researcher, the Department of Software in the Technical University of Catalonia, where he spent three years. As a researcher, he has visited the Department of Electrical and Electronic Engineering in the University of Cagliari, the Department of Information Engineering in the University of Siena, the SYSTeMS Research group in the University of Ghent, and the Computing Laboratory in the University of Oxford. In 2014, Jorge moved to the Cambridge Systems Biology Centre were he spent four years, two of them as a Marie Curie fellow. Jorge’s research interests are in the development of modeling formalisms and computational methods to model, analyse and optimize dynamic systems.


Benjamin Kaminski (University College London, UK)
Joost-Pieter Katoen (RWTH Aachen University, DE)
Christoph Matheja (ETH Zürich, AT)

Verifying Probabilistic Programs

Monday, August 31.  15:00 – 18:00

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.

Joost-Pieter Katoen is a full professor at the RWTH Aachen University (DE). He is the head of the Software Modeling and Verification (MOVES) group in that university, and also part-time associated to the Formal Methods & Tools group at the University of Twente (NL). Since 2013 Prof. Katoen holds a distinguished professorship at RWTH Aachen University, and he is a member of the Academia Europaea.

Benjamin Kaminski is a lecturer at the Programming Principles, Logic and Verification Group at University College London. Before that he carried out his PhD in the MOVES group headed by Prof. Katoen. Benjamin was associated with the DFG Research Training Group "Uncertainty and Randomness in Algorithms, Verification, and Logic,&qhot; where he was a steering committee member.

Christoph Matheja is a postdoctoral researcher in the Programming Methodology Group headed by Peter Müller at ETH Zürich. Previously, he was a Ph.D. student in the Software Modeling and Verification Group at RWTH Aachen University under the supervision of Prof. Katoen. Christoph defended his Ph.D. thesis titled "Automated Reasoning and Randomization in Separation Logic" in January 2020.