Probabilistic Model Checking and Analysis

Module aims

The course is an introduction to the areas of probabilistic model checking and probabilistic program analysis.
Probabilistic model checking (PMC) is a formal technique for the analysis of systems that exhibit probabilistic behavior, either intrinsically (e.g., randomized protocols) or due to uncertain interactions (e.g., with the physical world). The course covers modelling system' behaviors using Markov models (DTMCs, CTMCs, and MDPs) and specifying  probabilistic properties in the main modal temporal logics (PCTL, PLTL, and CSL). Model checking algorithms for different classes of models and properties will be discussed. The course will include also practical case studies with the use of the PRISM model checker.

Probabilistic program analysis extends classical program, i.e. programming language based, analysis to extract probabilistic and quantitative properties of programs as well as formal analysis applied to probabilistic programs. The course will use a simple probabilistic toy language (pWhile) in order to introduce basic ideas about the concrete semantics of probabilistic languages/programs (in terms of DTMCs) and ways to construct an optimal abstract semantics which suitable for a simplified evaluation of its features. This leads to a framework of Probabilistic Abstract Interpretation (PAI) which generalises Abstract Interpretation.

Learning outcomes

On successful completion of the module, students should be able to:

Knowledge and Understanding

  • Know the specific material covered in the Syllabus, including the ability to do the following:

Intellectual skills

  • Understand the modelling formalisms and logics for the specification of uncertainty in systems and requirements
  • Understand and use state of the art probabilistic model checking algorithms
  • Appreciate the applicability scope and limitations of the different probabilistic models and probabilistic model checking algorithms


Practical skills

  • Precisely formalise uncertainty in software design models and requirements
  • Solve probabilistic model checking problems both manually, on paper, and using state of the art tools


Transferable skills

  • Become proficient in the use of probabilistic modelling and model checking to formalise and quantitatively evaluate different design solutions

Module syllabus

Probabilistic Model Checking:

  • Foundation of discrete time Markov chains (DTMCs)
  • Probabilistic linear and branching time logics (LTL, PCTL, PCTL*)
  • PCTL model checking for DTMCs
  • Tools (PRISM)
  • Reward models and Reward-PCTL
  • Nondeterminism and Markov decision processes (MDPs)
  • PCTL model checking for MDPs
  • Continuous time Markov chains (CTMCs)
  • Continuous stochastic logic (CSL)
  • CSL model checking for CTMCs

Optional advanced topics:

  •  parametric PMC
  •  statistical PMC
  •  probabilistic counterexamples

Probabilistic Program Analysis:

  • Static Program Analysis (Dataflow Analysis)
  • Operational Semantics and Traces
  • Program Properties (Lattices)
  • Abstract Interpretation (Galois Connections)
  • Compositional Probabilistic Models (Tensor/Kronecker Product)
  • Order Reduction and Simplification
  • Probabilistic Abstract Interpretation (Moore-Penrose)
  • Applications: Dataflow Analysis, Bisimulation, etc.
  • Machine Learning and Least Square Approximation/Regression
  • Optional: Construction of Optimal Abstractions

Pre-requisites

Basic Linear Algebra (vectors, matrices, etc.) e.g. from Mathematical Methods (CO145)

Teaching methods

Lectures combined with tutorials, coding sessions in PRISM (Suggested, non-mandatory homework).

Assessments

Examination and Coursework (Tests)

Module leaders

Dr Antonio Filieri
Dr Herbert Wiklicky