Formal Methods for AI-based Systems Engineering
Course taught within the Master programme in Computer Science at Sapienza University of Rome.
Instructors
- Prof. Toni Mancini
- Prof. Paolo Zuliani
- Dr. Leonardo Picchiami (teaching assistant)
Course facts sheet
- Sapienza course ID: 10607006
- Number of credits: 6
- Language of lectures: English
Objectives
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.
Programme
The course is split in 2 equally sized parts, which will be taught in order.
Part 1 (held by Prof. Paolo Zuliani)
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.
Part 2 (held by Prof. Toni Mancini)
Artificial intelligence in systems engineering, state-of-the-art reasoners and model checkers, case studies.
RAISE