Model Checking (Core Course 2025 – 26)

Lecturers

Clemens Grabmayer (4 lectures)
Emilio Tuosto (3 lectures)

Lectures

Monday, January 26, 10.30–12.30, room B, Aurora.
Tuesday, January 27, 14.30—16.30, P-2.6, Zenith.
Thursday, January 29, 14.30—16.30, conference room –1, Zenith.
Friday, January 30, 14.30—16.30, conference room –1, Zenith.
Monday, February 2, 14.30—16.30, conference room –1, Zenith.
Tuesday, February 3, 14.30—16.30, conference room –1, Zenith.
Thursday, February 5, 14.30—16.30, conference room –1, Zenith.

Motivation and Preview

Introduction to Model Checking (Preview of Core Course)
- slides for preview Talk, December 11, 2025 (pdf)).

Books

cover of model-checking boek by Baier and Katoen

Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, MIT Press, 2008.
- A pdf version of the book can be found on the internet.

Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott: All about Maude — A High-Performance Logical Framework (How to Specify, Program and Verify Systems in Rewrite Logic), Springer Verlag.
- Springer page: Springer webpage for book.

Links to Resources

Maude (formal reasoning tool):
- Maude rewriting logic tool (webpage),
- Maude 3.2.1 manual (html (link)),
- Maude model checker (link).
Webinterface LTL 2 BA : fast translation from LTL formulae to Büchi automata for tool LTL2BA by Denis Oddoux using a technique of his and Paul Gastin.
Further reading:
- partial model checking [notes 2024 (pdf)]
  - the research paper Partial Model Checking and Partial Model Synthesis in LTL Using a Tableau-Based Approach (link) by Serenella Cerrito, Valentin Goranko, Sophie Paillocher at FSCD 2023 on partial model checking
- modal μ–calculus
  - book chapter The mu-calculus and model-checking (link) by Julian Bradfield and Igor Wałukiewicz.

Lectures

Introduction (slides handout, slides of Lecture 1).
- motivation for model checking
- difference with simulation and testing
- glance at model checking with temporal logics
- motivating example of three processes working on a counter: program graph and labeled transition system, formulas of LTL and CTL
- Example Maude code for the three processes that work on a counter
- exam options
Modeling by labeled transition systems [notes (pdf) of Lecture 2]
- definition
- examples: beverage vending machine, traffic lights, dining philosophers
- non-determinism: action-deterministic, AP-deterministic LTSs
- handshaking communication of LTSs
- execution fragments and traces of LTSs
Linear-Time Behavior & Properties [notes (pdf) of Lecture 3]
- path fragments and paths
- invariant, safety, and liveness properties
- every LT-property is the intersection of a safety and a liveness property
- fairness properties
Linear Temporal Logic (LTL), and exercises Linear-Time Properties and Fairness
- exercises
  - vending machines example for trace inclusion example trace inclusion [note (pdf)]
  - studying fairness, strong fairness, and weak fairness for an example suggested by Gabriele [note (pdf)]
- LTL [notes of Lecture 5 (pdf) of Lecture 3]
  - syntax and semantics
  - derived modalities, equivalence of formulas
  - interpretation in a transition system
  - concrete examples
Linear Temporal Logic (LTL), continued [notes (pdf)]
- Weak Until modality W
  - permits to express the negation of Until U
  - duality between modalities W and U [notes (pdf)]
  - permits to write LTL formulas in positive normal form
- Fairness in LTL
  - unconditional, weak, and strong fairness conditions expressed by LTL-formulas
  - fair satisfiability based on fair paths
    - subjecting an LTL formula Ψ to a fairness conditions fair can be expressed as the implicative LTL formula ( fair ⇒ Ψ ).
- model checking LTL formulas
  - example of model checking "by hand" (Exercise 5.2 in the book)
  - express properties by (generalized) Büchi automata
    - examples of translations of LTL formulas ( □ ◇ a ("always eventually a") and ◇ □ a ("eventually always a") ) as non-deterministic Büchi automata
LTL (continued), Computation Tree Logic (CTL)
1. LTL model checking [notes LTL model checking (pdf)]
  - the modality "release" expressed via weak until W
  - non-deterministic Büchi automata for the until modality U and the weak-until modality W
  - model checking transition systems and properties via product automata
    - LTL model checking algorithm
      - algorithm schematically
      - example from the book (Pedestrian traffic light, property infiitely often green)
    - Computation Tree Logic (CTL) [notes CTL (pdf)]
      - syntax and semantics
      - examples
      - Extensions of CTL
        
        CTL⁺
        
        is equally expressibe as CTL (proof idea via translation of CTL⁺ formulas into CTL formulas
        
        CTL^*
        
        is more expressive as CTL
        encompasses LTL by starting with a ∀ path quatifier
LTL model checking with Maude, CTL model checking algorithm, and complexity LTL/CTL model checking [notes Lecture 7 (pdf)]
- Webinterface LTL 2 BA : fast translation from LTL formulae to Büchi automata for tool LTL2BA by Denis Oddoux using a technique of his and Paul Gastin.
- LTL model checking with Maude: the River Crossing Problem.
- CTL model checking
  - Existential normal form (ENF) of CTL formulas
  - inductive clauses for set satisfiability sets Sat(true), Sat(p), Sat(¬Φ), Sat(Φ₁∧Φ₂), Sat(∃○ ◯ Φ), Sat(∃ΦUΨ), Sat(∃□Φ).
    - least fixed-point definition of ∃ΦUΨ,
    - greatest fixed point definition of ∃□Φ.
- complexity of model-checking algorithms in comparison:
  - model checking of LTL formulas Φ in transition systems TS is PSPACE complete, with upper bound O(|TS|.2^|Φ|) ;
  - model checking of CTL formulas Φ in transition systems TS is in PTIME with complexity O(|TS|.|Φ|) ;
  - model checking of a μ-calculus formula Φ in transition systems TS is in NP ∩ co-NP.

Clemens Grabmayer / www: https://clegra.github.io / mailto: c one dot a one dot grabmayer one at gmail one dot com / Last modified: Fri 6 Feb 2026 09:43 CST /