Computer Science

TONI MANCINI
TONI MANCINI
PAOLO ZULIANI
PAOLO ZULIANI

General goals:
The course is aimed to the acquisition of logical and modelling knowledge for systems engineering based on artificial intelligence (AI).

Specific goals:
Students will acquire knowledge on a wide portfolio of formal methods for AI-based systems engineering, in particular approaches to the formal verification and design optimization of complex systems.

Knowledge and understanding:
At the end of the course, students will have full understanding of the presented methods and software tools.

Apply knowledge and understanding:
Students will be able to use the methods and software tools presented in the course, but also to deepen the study independently by consulting other texts on the subject, including the available scientific literature.

Critical and judgmental skills:
The acquired knowledge will allow students to properly tackle the systems engineering tasks they will be involved in during their working carrier.

Communication skills:
Students will be stimulated to expose and communicate their experience to their peers and to the instructors.

Ability to continue the study:
The course will deal with only some of the available methodologies and technologies, but will provide students with awareness of the existence of a wide range of alternative options. This will make students able to critically choose the most suitable methodologies and technologies for their AI-based systems engineering tasks.

General goals:
The course is aimed to the acquisition of logical and modelling knowledge for systems engineering based on artificial intelligence (AI).

Specific goals:
Students will acquire knowledge on a wide portfolio of formal methods for AI-based systems engineering, in particular approaches to the formal verification and design optimization of complex systems.

Knowledge and understanding:
At the end of the course, students will have full understanding of the presented methods and software tools.

Apply knowledge and understanding:
Students will be able to use the methods and software tools presented in the course, but also to deepen the study independently by consulting other texts on the subject, including the available scientific literature.

Critical and judgmental skills:
The acquired knowledge will allow students to properly tackle the systems engineering tasks they will be involved in during their working carrier.

Communication skills:
Students will be stimulated to expose and communicate their experience to their peers and to the instructors.

Ability to continue the study:
The course will deal with only some of the available methodologies and technologies, but will provide students with awareness of the existence of a wide range of alternative options. This will make students able to critically choose the most suitable methodologies and technologies for their AI-based systems engineering tasks.

Students are expected to have good knowledge of:

1) Imperative and object-oriented programming in any high-level language
2) Design of algorithms and data structures
3) General mathematics, algebra, set theory, probability theory
4) Propositional and first-order logic
5) Software Engineering
6) Automata, computational complexity, decidability
7) General knowledge in Artificial Intelligence (even at an introductory level)

Kripke structures, Temporal logics, the Model Checking Problem, complexity.
Buchi automata, on-the-fly computation, search space reductions, mu-calculus, OBDD, hybrid automata.
Compositional reasoning, Software model checking, probabilistic model checking.
Artificial intelligence in systems engineering, state-of-the-art reasoners and model checkers, case studies.

Slides and lecture notes made available by the teacher.

Suggested reading:

Edmund M. Clarke, Jr., Orna Grumberg, Daniel Kroening, Doron Peled and Helmut Veith.
Model Checking, Second Edition.
MIT Press, 2018
ISBN: 9780262038836



Further readings:

Clarke, E.M., Henzinger, Th.A., Veith, H., Bloem, R. (eds).
Handbook of Model Checking.
Springer, 2018
ISBN: 9783319105758

Christel Baier, Joost-Pieter Katoen
Principles of Model Checking
MIT Press, 2008.
ISBN: 9780262026499

The course comprises lectures and labs covering the whole course programme.

Attendance is not mandatory, but highly recommended.

The exam comprises a written part and a student project.

In the written exam, students are requested to answer to questions and exercises on the entire programme.

The student project consists in a written report (plus, possibly, software) to be presented in a series of seminars.

To pass the exam, both parts must be of satisfactory quality.

The course website contains questions and exercises similar to those asked at the exam.

• Strutture di Kripke, logiche temporali, il problema del model checking, complessità
  • Books: Slides and lecture notes made available by the teacher


• Automi di Buchi, on-the-fly computation, riduzione dello spazio di ricerca, mu-calcolo, OBDD, automi ibridi
  • Books: Slides and lecture notes made available by the teacher


• Ragionamento composizionale, model checking per il software, model checking probabilistico
  • Books: Slides and lecture notes made available by the teacher


• Intelligenza artificiale nell'ingegneria dei sistemi, ragionatori e model checker stato dell'arte, casi di studio
  • Books: Web resources