The Doctoral College on Resilient Embedded Systems and the TU Wien Informatics Doctoral School invite to a talk by guest professor Joost-Pieter Katoen.

Public Lecture

Abstract

Markov chains are central in performance and dependability analysis, whereas Markov decision processes are key in stochastic decision making and planning in AI. A standard assumption in these models is that all probabilities are precisely known a priori. In many cases, this assumption is too severe. System quantities such as component fault rates, molecule reaction rates, packet loss ratios, etc. are often not, or at best partially, known.

This talk surveys the analysis of parametric probabilistic models whose transitions are labelled with functions over a finite set of parameters. These models are symbolic representations of uncountably many concrete probabilistic models, each obtained by instantiating the parameters.

We consider various analysis problems for a given logical specification φ: do all parameter instantiations within a given region of parameter values satisfy φ?, which instantiations satisfy φ and which ones do not?, and how can all such instantiations be characterised, either exactly or approximately?

We address theoretical complexity results and describe the main ideas underlying state-of-the-art algorithms that established an impressive leap over the last decade enabling the fully automated analysis of models with millions of states and thousands of parameters. Examples from distributed computing, satellites and AI (Bayesian networks and robotics planning) illustrate the applicability of these parameter synthesis techniques.

About Joost-Pieter Katoen

Joost-Pieter Katoen is a distinguished professor at RWTH Aachen University leading the Software Modeling and Verification (MOVES) group. He is part-time affiliated to the University of Twente. His main research interests are model checking, concurrency theory, program analysis, probabilistic programming, and formal semantics. He co-authored the book Principles of Model Checking, a bestseller in formal verification. He participated and led several (inter)national projects and is currently spokesman of the RTG UnRAVeL, an interdisciplinary PhD school at RWTH. He is a member of the Academia Europaea, is holder of an ERC Advanced Grant on probabilistic programming foundations, and is an ACM Fellow.

Note

The lecture series on research talks by the guest professors of the TU Wien Informatics Doctoral School can also be credited as an elective course for students of master programs of computer science: 195.072 Current Trends in Computer Science.

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.