Trustworthy Intelligent Systems

Practical aspects of Probabilistic Model Checking

In this summer school, we survey the main aspects relative to probabilistic model checking, with a specific attention to the practical aspects.

After a brief introduction on why probabilistic systems are worth of consideration and on why it is important to formally verify the correctness of probabilistic systems, we shortly present the underlying theory for modelling probabilistic systems and for specifying the desired properties the systems are expected to satisfy.

These open the way to the core part of the summer school, that is, how model checking can be done in practice and how a model checker can be developed in practice. In particular, we focus on the core parts of a model checker, the importance of its modular construction and its extension, a description formalism allowing to interact with other tools, and so on.

Main topics covered in the summer school:

  1. The Why’s of probabilistic model checking:
    • why formal verification is important
    • why model checking is important
    • why probabilistic systems are important
  2. Lightweight theory:
    • the models for representing probabilistic systems (discrete time Markov chains, Markov decision processes, …)
    • the logics for talking about properties of probabilistic systems (PCTL, PLTL, PCTL*, …)
    • the extensions, for more informative analysis (rewards, intervals, parametric analysis, …)
  3. Model checking in practice, the modelling language:
    • JANI modelling language
    • PRISM modelling language
    • JANI interaction language
  4. Model checking in practice, the tool architecture:
    • the development tools: languages, editors, and build system
    • model checker architecture
    • plugin system for extendibility
    • type system
  5. Model checking in theory, the details:
    • the algorithm for model checking PCTL formulas
    • how to work with LTL formulas
    • the algorithm for model checking PLTL/PCTL* formulas
  6. Advanced model checking:
    • practical improvements for probabilistic model checking (lazy determinisation, on-the-fly construction, …)
    • probabilistic games
    • planning

Material: slides, handout