Quantitative Model Checking

Quantitative Model Checking

Jan Krčál (instructor)

Holger Hermanns (instructor)

Hassan Hatefi (assistant)

Vahid Hashemi (assistant)

Yuliya Butkova (assistant)

Audience

This advanced course addresses Bachelor and Master students in Computer Science, Bioinformatics, CuK or Computerlinguistics. Background in probability theory and the module Verification are of advantage but not mandatory.

Objectives

Quantitative model checking is concerned with quantities (mostly probabilities) within systems exhibiting random behaviour. Such systems include networked, embedded, or biological systems. Their underlying semantics are usually discrete-time and/or continuous-time Markov chains, possibly extended with nondeterminism. On the respective models, quantitative properties of interest can be verified. The properties can be specified, e.g., by PCTL or LTL for discrete-time models, and CSL for continuous-time models. This course aims to cover both the model construction and the verification techniques for these systems.

Credits: 6 ECTS points (2 hours of lecture, 2 hours of tutorials, and some exercices every week)

When and where?

Lectures: every Tuesday 10 - 12 in the seminar room 016 in E1 3, starting on October 21, 2014.
Tutorials: every Thursday 10 - 12 in the room 528 in E1 3, starting on November 6, 2014

Grading

There will be a final written exam: 

• Exam: Tuesday February 24, 10:15 AM, E1 3 016
• Re-exam: Tuesday March 24, 10:15 AM, E1 3 016

Having at least 50% points for both theoretical and practical exercises is required for admission to the final exam. Your current point status will be made available in dCMS.

Syllabus (tentative)

• Model Checking
• Probability Theory
• Stochastic Processes
• Discrete-Time Markov Chains (DTMC)
• Probabilistic Computation Tree Logic (PCTL)
• Model Checking DTMC
• Probabilistic Bisimulation (DTMC)
• Continuous-time Markov Chains (CTMC)
• Continuous Stochastic Logic (CSL)
• Model Checking CTMC
• Probabilistic Bisimulation (CTMC)
• Logical Characterization
• Non-Determinism and Markov Decision Processes (MDP)
• Model Checking MDP
• Bisimulation and Logical Characterization (MDP)

Textbooks

• Principles of Model Checking. Christel Baier and Joost-Pieter Katoen, MIT Press, 2008 (also available from the library)
• First Look at Rigorous Probability Theory. Jeffrey S Rosenthal, World Scientific Publishing Company, 2006

References from slides

• Lecture 7 (in order of appearance)
  • [VW94] M. Vardi and P. Wolper. Reasoning about infinite computations. Information and
    Computation, 115(1):1–37, 1994.
  • [Saf88] S. Safra: On the complexity of ω-automata, Proceedings of the 29th FOCS, 1988.
  • [KE12] Jan Kretínský, Javier Esparza: Deterministic Automata for the (F, G)-Fragment of LTL. CAV 2012: 7-22
  • [BBKS13] Tomás Babiak, Frantisek Blahoudek, Mojmír Kretínský, Jan Strejcek: Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F, G)-Fragment. ATVA 2013: 24-39
  • [EK14] Javier Esparza, Jan Kretínský: From LTL to Deterministic Automata: A Safraless Compositional Approach. CAV 2014: 192-208
  • [HLSZ13] Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, Lijun Zhang: Lazy Determinisation for Quantitative Model Checking. CoRR abs/1311.2928 (2013)
  • [KB07] Joachim Klein, Christel Baier: On-the-Fly Stuttering in the Construction of Deterministic omega -Automata. CIAA 2007: 51-61
• Lecture 8 (in order of appearance)
  • [SHS03] Salem Derisavi, Holger Hermanns, William H. Sanders: Optimal state-space lumping in Markov chains. Inf. Process. Lett. 87(6): 309-315 (2003)