Model Checking  (Core Module 2024 – 25)

Lecturers

• Clemens Grabmayer (5 lectures)
• Emilio Tuosto (2 lectures)

Room

• P-2.6, Ex-INPS building of GSSI L'Aquila.

Lecture times

1.   Friday, January 31, 16.00—18.00
2.   Monday, February 3, 14.30—16.30
3.   Wednesday, February 5, 14.30—16.30
4.   Thursday, February 6, 10.30—12.30
5.   Friday, February 7, 14.30—16.30
6.   Monday, February 10, 10.30—12.30
7.   Tuesday, February 11, 10.30—12.30

Motivation and Preview

• Introduction to Model Checking (Preview of Core Module)
  • slides for preview talk, December 2, 2024 (pdf)).

Book

• 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

Links to Resources

• Laboratory of Formal Methods (2017/2018) by Patrick Trentin of the University of Trento:
  • Webpage Laboratory of Formal Methods (2017/2018)
    • http://disi.unitn.it/~trentin/teaching/fm2018/fm2018.html
  • slides lecture 1: SPIN: Introduction
  • slides lecture 4: SPIN: LTL Model Checking
• 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

1. Introduction    [notes (pdf)]
   • motivation for model checking
   • difference with simulation and testing
   • glance at model checking with temporal logics
2. Modeling by labeled transition systems    [notes (pdf)]
   • modeling by Labeled Transition Systems (LTSs)
     • exections, traces,
     • non-determinism
     • examples
3. Linear-Time Behavior & Properties    [notes (pdf), exercises (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 (pdf), exercises (pdf)]
   • syntax and semantics
   • derived modalities, equivalence of formulas
   • interpretation in a transition system
   • concrete examples
5. Linear Temporal Logic (LTL)    [notes (pdf), exercise (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 (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 (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 20 Mar 2025 16:55 CST / /