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.
Lesson 19: 28/04/2026 (10:30 - 12:30) 2 hours
Description: Last considerations on LTL model checking via behavior graphs. Computation Tree Logic (CTL): syntax and semantics. Examples. Comparison between LTL and CTL: examples of their incomparability.
Lesson 20: 29/04/2026 (10:30 - 12:30) 2 hours
Description: CTL model checking: microwave oven examples and algorithm. Symbolic Model Checking: the state-space explosion problem, limitations of explicit-state model checking algorithms, and definition of symbolic transition system.
Lesson 21: 05/05/2026 (10:30 - 12:30) 2 hours
Description: Example of application of symbolic model checking. Bounded Model Checking (BMC): structure of the overall algorithm, definition of (k,l)-loop, k-loop, and loop-free path. Bounded semantics of LTL. Encoding of all the paths of length k of the model. Encoding of the LTL formula. Overall encoding and the use of SAT-solvers. Example with the nuXmv model checker.
Lesson 22: 06/05/2026 (10:30 - 12:30) 2 hours
Description: Ordered Binary Decision Diagrams (OBBDs): definition of Binary Decision Trees (BDTs) and their limitations (redundancies), definition of OBDDs, examples, and Boolean formulas corresponding to OBDDs. Three rules for minimizing an OBDD: applications to the example and definition of OBDDs in Canonical Form. Definition of the RESTRICT function.
Lesson 23: 08/05/2026 (10:30 - 12:30) 2 hours
Description: OBDDS: definition of the RESTRICT function, of Shannon Expansion and its use for the construction of an OBDD implementing one Boolean function. Definition of Predicate Transformer and its visualization in the Hasse Diagram of the lattice of all subsets of a set S. Examples. Definition of monotonic predicate transformers and main lemmas. Knapster-Tarski Theorem for the existence and calculations of the least and the greatest fixpoints and its implication for the case in which S is a finite set.
Lesson 24: 12/05/2026 (10:30 - 12:30) 2 hours
Description: Algorithms LFP and GFP for the computation of the least and greatest fixpoint of a monotonic predicate transformer. Proof of termination and correctness of LFP. Predicate transformers for CTL operators and examples. Proof of correctness for the predicate transformer of EGp. Symbolic model checking algorithm of CTL: the CHECK function. Final considerations.