Model Checking  (Core Course 2025 – 26)

Lecturers

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

Room

• To be determined.

Lectures

1.   Monday, January 19.
2.   Tuesday, January 20.
3.   Wednesday, January 21.
4.   Friday, January 23.
5.   Monday, January 26.
6.   Tuesday, January 27.
7.   Wednesday, January 28.

Motivation and Preview

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

Books

• Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, MIT Press, 2008.
  • An early version of that book is available on the internet:
    • https://is.ifmo.ru/books/_principles_of_model_checking.pdf

• 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.
  • An version of that book is available at:
    • https://maude.cs.illinois.edu/w/images/0/0d/Maude-book.pdf

Links to Resources

• Maude (formal reasoning tool):
  • Maude rewriting logic tool (webpage),
  • Maude 3.2.1 manual (pdf (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   (schema 2024/25)

1. Introduction    [notes 2024/25 (pdf)]
   • motivation for model checking
   • difference with simulation and testing
   • glance at model checking with temporal logics
2. Modeling by labeled transition systems    [notes 2024/25 (pdf)]
   • modeling by Labeled Transition Systems (LTSs)
     • exections, traces,
     • non-determinism
     • examples
3. Linear-Time Behavior & Properties    [notes 2024/25 (pdf), exercises 2024/25 (pdf)]
   • path fragments and paths
   • invariant, safety, and liveness properties
   • every LT-property is the intersection of a safety and a liveness property
   • fairness properties
4. Linear Temporal Logic (LTL)    [notes 2024/25 (pdf), exercises 2024/25 (pdf)]
   • syntax and semantics
   • derived modalities, equivalence of formulas
   • interpretation in a transition system
   • concrete examples
5. Linear Temporal Logic (LTL)    [notes 2024/25 (pdf), exercise 2024/25 (pdf)]
   • 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 ⇒ Ψ ).
   • Weak Until modality W
     • permits to express the negation of Until U
   • Positive Normal Form of LTL formulas
   • model checking LTL formulas
     • express properties by (generalized) Büchi automata
       • examples of translations of LTL formulas ( ○a    and   a U b ) into generalized Büchi automata
6. LTL (continued), Computation Tree Logic (CTL)    [notes 2024/25 (pdf)]
   1. LTL model checking
      • model check transition systems and properties via product automata
        • LTL model checking algorithm
          • algorithm schematically
          • example from the book (Pedestrian traffic light, property infiitely often green)
          • model checking by using Spin: easy examples
      • complexity of this model-checking procedure
        • PSPACE-complete, with upper bound O(|TS|.2^|Φ|) where |TS| the size of the transition system, and |Φ| the size of the LTL formula Φ that is checked
   2. Computation Tree Logic (CTL)
      • syntax and semantics
      • examples
7. CTL⁺, CTL^*, and CTL-model checking       [notes 2024/25 (pdf)]
   • 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
   • example for finding CTL properties (triple redundancy of processors with voter)
   • expressibility difference between LTL, CTL, CTL⁺, and CTL^*, and the modal μ–calculus
     • For every LTL formula φ that arises from a CTL formula Φ by deleting the path quantifiers one of the following alternatives holds:
       • φ is equivalent to Φ;
       • there does not exist any LTL formula that is equivalent to Φ.
     • Venn diagram
   • 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.
   • 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 ∃□Φ.

Clemens Grabmayer / www: https://clegra.github.io / mailto: c one dot a one dot grabmayer one at gmail one dot com / Last modified: Thu 11 Dec 2025 08:28 CST / /