Lecturer(s):

Gabriele Puppis Course outline:

In this course, we will give an overview of some fundamental problems and classical techniques in the automated verification of infinite state systems.

The problems we will mainly focus on are the so-called satisfiability and model checking problems for formulas of first-order logic and monadic second-order logic, as well as variants of the reachability problem on pushdown automata and Petri nets. We will begin by recalling the fundamental results by Büchi and Rabin showing the decidability of monadic second-order theories of structures with one and two successors. We will then present application examples and techniques such as composition method, logical interpretation, unfolding, fixpoint computation of reachable sets.

Schedule:

Tentative schedule:

1- Warm-up: transition systems, automata, logics

2- First-order theories: undecidability, Presburger logic, automatic structures

3- The monadic theory of one successor: contraction and composition methods,

factorization forest theorem

4- The monadic theory of two successors: Rabin's complementation, application examples

5- The transformational approach: interpretations, context-free and prefix-rewriting graphs,

unfoldings, Caucal hierarchy, recursive schemes

6- Reachability via saturation: pushdown systems, Petri nets / VAS

Calendario delle lezioni

giovedì 29 maggio, ore 15:00-17:45, Aula Multimediale

venerdì 30 maggio, ore 15:00-17:45, Aula Multimediale

martedì 3 giugno, ore 14:00-16:45, Aula Multimediale

mercoledì 4 giugno, ore 15:00-17:45, Aula Multimediale

giovedì 5 giugno, ore 15:00-17:45, Aula Multimediale

venerdì 6 giugno, ore 15:00-17:45, Aula Multimediale