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.