Upon successful completion of this course, a student:

• knows the logical and computational techniques for specifying, verifying and synthesizing the behavior of AI agents and multi-agent systems, and the limitations of these techniques
• is able to read and assess the research literature in this field
• is able to use appropriate underlying logical formalisms as a framework for specifying, verifying and synthesizing the behavior of AI agents and multi-agent systems, and has a good understanding of the computational aspects of these formalisms
• is able to use appropriate tools implementing these techniques to specify, verify and synthesize the behavior of AI agents and multi-agent systems
• has acquired a mastery of technical artificial intelligence at an advanced academic level 

Assessment
One final exam, pass grade 6/10. 
In order to sit the exam, students need tot pass 50% of the coursework assignments.

Bonus point calculation (where exam is your grade for the final exam):
- if your coursework average is in the range 8-8.49, your grade is min(exam + 0.25, 10)
- if your coursework average is in the range 8.5-8.99, your grade is min(exam + 0.5, 10)
- if your coursework average is in the range 9-9.49, your grade is min(exam + 0.75, 10)
- if your coursework average is in the range 9.5-10, your grade is min(exam + 1, 10)

A retake of the exam requires at least a 4 for the original test.
 

This course is about ensuring the safety and reliability of autonomous AI agents and multi-agent systems.
In order to guarantee that the behavior of a system achieves its objectives, we use formal proofs rather than empirical studies, and either formally verify that the system behaves in accordance with the specified objectives, or automatically synthesize provably correct behaviors from specifications of the system objectives.
The formal techniques for doing this include epistemic and temporal logics and their combinations, and constitute the main technical content of the course.
The emphasis is on mastering these techniques, their computational aspects, and the use of tools implementing them to verify and synthesize AI agents and multi-agent systems.

The course also prepares students for undertaking research on formal aspects of artificial intelligence, and provides the foundation for undertaking Masters projects on developing safe and reliable AI systems.
Lab sessions will introduce students to relevant specification and modelling techniques and the use of tools such as MCMAS, STV and SynKiti for the verification and synthesis of AI agents and multi-agent systems. 

Futher course details can be found on
https://uu.blackboard.com/webapps/blackboard/content/listContent.jsp?course_id=_134905_1&content_id=_3838780_1&mode=reset

Course format
Two lectures and one tutorial session per week.
Assignments.  

Study material

• recommended: Wojtek Jamroga "Logical Methods for the Specification and Verification of Multiagent Systems" (free download at https://home.ipipan.waw.pl/w.jamroga/papers/jamroga15specifmas-20200411.pdf
• for specific topics, we will also provide references to open source papers and software tools
• for the practical sessions, you will need to download and install the model checker MCMAS. MCMAS is open source, and runs on Windows, MacOS, and Linux. For information on how to download and install MCMAS, see the MCMAS installation guide on Blackboard