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: 16/04/2024 (11:30 - 12:30) 1 hour
Description: Introduction to temporal logics. Main parameters of temporal logics. Introduction to Linear Temporal Logic (LTL). Examples. Syntax of LTL.
Slides:
Lesson 2: 17/04/2024 (10:30 - 12:30) 2 hours
Description: Examples of formulas in Linear Temporal Logic (LTL). Semantics of LTL. Addition of Past temporal operators. Main properties of LTL: correspondence with star-free languages, and expressively equivalence with the extension of past operators.
Slides:
Lesson 3: 18/04/2024 (10:30 - 12:30) 2 hours
Description: Introduction to tableaux methods for LTL satisfiability. Classification of tableaux methods. Definitions of closure, expansion rules, alpha and beta formulas, atoms, tableau, and induced and fulfilling paths. Proof of the theorem on the correspondence between fulfilling paths and good models of the formula.
Slides:
Lesson 4: 23/04/2024 (10:30 - 12:30) 2 hours
Description: Tableau methods for the satisfiability problem of LTL. Recap of the definitions of atoms and of fulfilling paths. Definition of SCS and fulfilling SCS. Euristics for pruning the tableau and MSCS.
Introduction to the problem of succinctness and to the construction of nondeterministic Buchi automata from LTL formulas.
Slides:
Lesson 5: 24/04/2024 (10:30 - 12:30) 2 hours
Description: Recap of the construction of nondeterministic Buchi automata starting from LTL+P formulas, definition of generalized Buchi automata, and examples with the tool LTL2BA.
Proof of Markey’s Theorem that LTLP can be exponentially more succinct than LTL.
Slides:
Lesson 6: 30/04/2024 (10:30 - 12:30) 2 hours
Description: Introduction to model checking. Formal definition of model checking. Examples.
Slides:
Lesson 7: 02/05/2024 (10:30 - 12:30) 2 hours
Description: Model checking algorithm for LTL. Construction of the behavior graph. Definition of adequate strongly connected subgraphs. Algorithm to compute adequate SCSs.
Slides:
Lesson 8: 07/05/2024 (10:30 - 12:30) 2 hours
Description: Computational Tree Logic (CTL): syntax, semantics, and examples. CTL*: examples. Comparison between the expressiveness of LTL and of CTL.
Slides:
Lesson 9: 08/05/2024 (10:30 - 12:30) 2 hours
Description: CTL Model Checking: examples and algorithm. Introduction of Symbolic Model Checking. Definition of symbolic transition system.
Slides:
Lesson 10: 09/05/2024 (10:30 - 12:30) 2 hours
Description: Symbolic Model Checking: example of BDD-based model checking, examples of symbolic transition systems. Bounded Model Checking: main ideas, (k,l)-loops, program unfolding, encoding, examples.
Slides:
Lesson 11: 14/05/2024 (10:30 - 12:30) 2 hours
Description: Binary Decision Trees. Binary Decision Diagrams (BDD). Canonical Form. Examples. The “restrict” function.
Slides:
Lesson 12: 15/05/2024 (10:30 - 12:30) 2 hours
Description: BDD: Shannon expansion, the Apply function, the LFP and the GFP algorithms, predicate transformers for CTL operators.
Slides:
Lesson 13: 16/05/2024 (10:30 - 12:30) 2 hours
Description: CTL symbolic model checking: the CHECK function. The nuXMV tool.
Slides: