The course aims at providing a systematic account of computer science methods, formalisms, and algorithms for the formal specification and automatic verification/validation of complex reactive systems. The student will learn how to master advanced formal tools (logic, automata theory, logical game theory) to be used for the analysis and the automatic verification of complex systems. See also this link.
Lesson 1: 03/03/2026 (10:30 - 12:30) 2 hours
Description: Introduction on the 2nd and 3rd module of the course: outline of the main topics that will be covered. Overview of automatic verification and validation technique, in particular to Model Checking. Introduction to the SMV modeling language: history and a first simple example.
Lesson 2: 04/03/2026 (10:30 - 12:30) 2 hours
Description: Syntax of SMV: the ASSIGN, init, and trans keywords. The CASE expressions. Semantics of SMV: transition system associated with an SMV module. Nondeterminism in SMV, implicit modeling, and input variables. Examples.
Lesson 3: 06/03/2026 (10:30 - 12:30) 2 hours
Description: SMV modules. Example of formal verification of a mechanical counter. Synchronous and asynchronous modeling: the PROCESS keyword. Fairness constraints: definitions of justice and compassion.
Lesson 4: 18/03/2026 (10:30 - 12:30) 2 hours
Description: The monadic second-order theory of 1 successor over the alphabet A (S1S-A): syntax, semantics, and example. How to define < with only +1. Examples of languages and their corresponding S1S-A formula.
Lesson 5: 20/03/2026 (10:30 - 12:30) 2 hours
Description: Definition of S1S_0. Expressive equivalence of S1S and omega-regular languages. From Buchi automata to S1S, and from S1S to Buchi automata.
Lesson 6: 24/03/2026 (10:30 - 12:30) 2 hours
Description: Buchi Theorem: decidability of S1S sentences with input-free nondeterministic Buchi automata. Decidability of S1S over finite domain (finite words). Extensions of S1S: decidable and undecidable cases. Deterministic Buchi automata (DBA): definition and examples.
Lesson 7: 25/03/2026 (10:30 - 12:30) 2 hours
Description: Characterization of the languages recognized by Deterministic Buchi Automata (DBA) in terms of vectorial closure. Proof that the language of words with finitely many “a” is not recognizable by any DBA. Definition and examples of Muller Automata over infinite words.
Lesson 8: 27/03/2026 (10:30 - 12:30) 2 hours
Description: Characterization of languages recognized by DMA (deterministic Muller automata) in terms of (Boolean combination of) vectorial closure of regular languages. Statement (without proof) that omega-regular languages can be translated into Boolean combinations of vectorial closures of regular sets, and viceversa: point out the difficult steps and why the equivalence is not trivial. McNaughton’s Theorem. Proof that WS1S is equivalent to S1S.
Lesson 9: 31/03/2026 (10:30 - 12:30) 2 hours
Description: Rabin automata over omega-words: definition and examples. Star-free (omega)-regular expressions (SF) and their connection with the first-order fragment of S1S (FO-S1S). Translation from SF to FO-S1S. From FO-S1S to SF: definition of the equivalence regarding the formulas of quantifier depth n.
Lesson 10: 01/04/2026 (10:30 - 12:30) 2 hours
Description: Proof of McNaughton-Papert Theorem: direction from FO-S1S[<] sentences to star-free regular expressions. Languages over trees: definition of tree, path, frontier and outer frontiers. Languages of finite trees and languages over infinite trees. From k-ary A-valued trees to (infinite) binary A-valued trees.
Lesson 11: 08/04/2026 (10:30 - 12:30) 2 hours
Description: Concatenation between trees and Kleene’star of tree languages. Definition of nondeterministic top-down tree automata and two examples. Limitations of deterministic top-down tree automata (path properties) and introduction and definition to bottom-up tree automata.
Lesson 12: 10/04/2026 (10:30 - 12:30) 2 hours
Description: Buchi automata over infinite trees: definition and three examples. Example of a language of infinite trees that is not Buchi recognizable. Rabin automata over infinite trees and their expressive power. Main theorems: decidability of emptiness problem for Rabin automata and their equivalence with S2S. Brief mentions to WS2S. Introduction to modal logic and overview of Linear Temporal Logic (LTL).
Lesson 13: 14/04/2026 (10:30 - 12:30) 2 hours
Description: Linear Temporal Logic. Definition of state sequence and examples of formulas. Formal semantics: when an LTL formula is true at position i of a state sequence. Examples of GFp (“infinitely many times p”) and FGp (stabilization constraint).
Lesson 14: 15/04/2026 (10:30 - 12:30) 2 hours
Description: Linear Temporal Logic with Past (LTL+P): the Yesterday and Since modalities. Main theorems about LTL and LTL+P: expressive power and expressive equivalence with S1S[FO] and star-free omega-regular expressions. Examples. Introduction to tableaux methods for LTL satisfiability checking: overview of various approaches (implicit vs explicit, declarative vs incremental) and definition of the closure set of a formula.
Lesson 15: 17/04/2026 (10:30 - 12:30) 2 hours
Description: Tableau for LTL. Definition of tableau for phi in terms of phi-atoms and the accessibility relation of phi-atoms. Definitions of fulfilling paths and proof that they correspond to induced models. Example of tableau for the formula G(p) & F(!p). Definition of Strongly Connected Subgraphs (SCSs) and fulfilling SCSs. Equivalence between LTL satisfiability checking and search of fulfilling SCSs reachable from a phi-atom.
Lesson 16: 21/04/2026 (10:30 - 12:30) 2 hours
Description: Tableau for LTL satisfiability: pruning of the tableau, Maximal SCS (MSCS), and terminal MSCS, final considerations. Transformation of LTL+P formulas into equivalent Nondeterministic Buchi Automata (NBA): definition of states, transitions, and final state. Definition of Generalized Buchi automata and notes on their degeneralization. Exponential complexity of the translation. Automata-based model checking of LTL+P formulas and example with nuXmv.
Lesson 17: 22/04/2026 (10:30 - 12:30) 2 hours
Description: Proof that LTL+P can be exponentially more succinct than LTL. Definition of the family of languages A_n and B_n. Polynomial LTL+P formulas for A_n. Proof that every Nondeterministic Buchi Automaton (NBA) for B_n is of size doubly exponential in n. Conclusions of the proof. Model checking of LTL: definitions and examples.
Lesson 18: 24/04/2026 (10:30 - 12:30) 2 hours
Description: Fair model checking of LTL. Construction of the behavior graph for P and phi. Example with the LOOP system and the LTL formula FG(x != 3). Definitions of just, compassionate, and fulfilling subgraph. Adequate subgraph S’ does not imply that S is adequate, for S subgraph containing S’. Overview of the “ADEQUATE-SUB” algorithm for LTL fair model checking.