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: 24/04/2025 (10:30 - 12:30) 2 hour
Description: Introduction to temporal logics. Main parameters of temporal logics. Introduction to Linear Temporal Logic (LTL). Examples. Syntax of LTL.
Slides:
Lesson 2: 29/04/2025 (10:30 - 12:30) 2 hour
Description: Semantics of LTL. Examples. Equivalence between LTL and star-free languages. Extension of LTL with past operators and its equivalence with LTL. Introduction to tableau methods for LTL.
Slides:
Lesson 3: 30/04/2025 (10:30 - 12:30) 2 hour
Description: The tableau method for LTL. Definitions of closure, phi-autom, expansion rules, and alpha- and beta-formulas. Example of a tableau. Definition of fulfilling path and its correspondence with models of the formula.
Slides:
Lesson 4: 06/05/2025 (10:30 - 12:30) 2 hour
Description: The tableau method for LTL. Correspondence between fulfilling paths and induced models. Definitions of strongly connected subgraphs (SCS) and maximal SCS (MSCS). Pruning of the tableau: phi-reachable fulfilling MSCS and terminal non-fulfilling MSCS. Introduction to the succinctness of LTL+P: recap of syntax and semantics of LTL+P, construction of nondeterministic Buchi automata equivalent to an LTL+P formula.
Slides:
Lesson 5: 07/05/2025 (10:30 - 12:30) 2 hour
Description: Translation of LTL+P formulas into equivalent Generalized Buchi automata. Use of online tools for this translation. Succinctness of LTL+P w.r.t. LTL. Preliminary steps: definitions of the families of languages A_n and B_n.
Slides:
Lesson 6: 08/05/2025 (10:30 - 12:30) 2 hour
Description: Succinctness of LTL+P: proof that B_n requires Buchi automata of at least doubly-exponential size. Proof that LTL+P can be exponentially more succinct than LTL. Introduction to Model-Checking (MC): motivations, examples, differences with testing, definition of LTL model-checking.
Slides:
Lesson 7: 13/05/2025 (10:30 - 12:30) 2 hour
Description: Model checking of LTL. Definitions of P-satisfiability and P-validity. Construction of the behavior graph and examples. Definition of adequate subgraphs and examples.
Slides:
Lesson 8: 14/05/2025 (10:30 - 12:30) 2 hour
Description: Model checking of LTL: example of application of the algorithm “adequate-sub” and final considerations. Introduction to CTL: syntax, semantics, examples, and properties. Example of formulas expressible in CTL but not in LTL, and viceversa.
Slides:
Lesson 9: 15/05/2025 (10:30 - 12:30) 2 hour
Description: Algorithm for CTL model checking. Example of application on a real-world example. Introduction to symbolic model checking.
Slides: