Invited Seminar at ICTAC 2023 Training School on Applied Formal Methods

The ICTAC 2023 Training School on Applied Formal Methods was a two days school associated to the ICTAC 2023 conference and has the aim to promote the formal methods techniques in the global south.

This edition took place in Lima, Peru at UTEC on the 4th and 5th of December, 2023.

I was very glad I was given the opportunity to give a 3 hours lecture at the school where I had the chance to lecture on Probabilistic Model Checking to master students, Ph.D. students, early-stage researchers, and colleagues curious on the subject. I enjoyed it a lot!

Title: Probabilistic Model Checking.
Abstract: Model checking is a powerful tool to verify automatically if a model satisfies a given property. They normally provide a Boolean answer to a qualitative question. However, probabilistic features normally appear in systems of usually crucial characteristics. For example, it is common to use randomized protocols to solve contention situations in networks or to understand fault models through the stochastic behaviors of faults. In this last case, for instance, the statement "the system does not fail" might be impossible to verify while rather the appropriate question could be "99% of the time the system does not fail". In this tutorial, we will introduce the fundamentals and algorithms to address the verification of this type of quantitative properties. In particular, we will discuss the verification of quantitative and qualitative properties on discrete-time Markov chains as well as on the more versatile setting of Markov decision process.