Title: Formal verification of multi-agent systems

Abstract: Model checking is a well-established method that allows to verify the system correctness. First applications of model checking involved closed systems by analyzing whether a model of the system meets a temporal logic formula, specifying a desired behavior. Unfortunately, this technique is quite useless in practice since most systems are open, i.e. they are characterized by an ongoing interaction between multiple entities. To overcome this problem, researchers have started looking at multi-agent systems. Breakthrough contributions along this direction concern the introduction of strategic logics. In this course, we will focus on Alternating-time Temporal Logic (ATL), the first introduced logic for the strategic reasoning.

Bio: Vadim is an Associate Professor in the Computer Science and Networks department (INFRES) of Télécom Paris . From November 2017 to June 2020, He was a postdoctoral researcher at the University of Evry under the supervision of Francesco Belardinelli. In February 2018, He obtained his Ph.D. in Computer Science at the University of Naples "Federico II", with a thesis titled "Strategic Reasoning in Game Theory", developed under the supervision of Aniello Murano. During his Ph.D. program, He was a visiting researcher at the Polish Academy of Sciences, under the supervision of Wojtek Jamroga. In July 2014, He obtained his Master's degree in Computer Science, with a thesis titled "Graded modalities in strategic reasoning", developed under the supervision of Aniello Murano and Fabio Mogavero. In December 2010, He obtained his Bachelor's degree in Computer Science, with a thesis titled "Implementazione di un algoritmo di verifica formale per programmi gerarchici nel tool Yasm" (Implementation of a formal verification algorithm for hierarchical programs in the Yasm tool), developed under the supervision of Aniello Murano.

Title: Accountability in Multi-Agent Organizations: a Guided Tour from Conceptual Design to Agent Programming in JaCaMo

Abstract: Accountability has been studied in many fields (e.g. social sciences, political sciences) because it supports organizations in responding to evolving environmental conditions, enabling a review-and-learn process. Recently, it started to receive attention in multiagent systems research. Multiagent systems and organizations provide abstractions for realizing networked systems of autonomous parties, which altogether work at the achievement of some organizational goal, decomposed into sub-goals distributed to the agents, each of which contributes to the overall achievement. This tutorial introduces accountability and explains its use from a software engineering perspective, that is, accountability as a tool for realizing multiagent systems that can cope with perturbations, like failures, lack of resources, or stressful execution conditions. More precisely, after an initial discussion about accountability in abstract terms, the tutorial will present how it could be the means for the design of robust distributed systems. A conceptual model of accountabilty is therefore presented in the context of multiagent organizations. Finally, the tutorial exemplify how accountability can be practically used for programming agents in an extension of the JaCaMo agent platform.

Bio: Roberto Micalizio took his Laurea degree summa cum laude in Computer Science in April 2003, and his Ph.D. in Computer Science in February 2007, both at the Università Torino, Italy. Since October 2007 he is a researcher at the Dipartimento di Informatica, Università degli studi di Torino, where he is member of the working group on Intelligent Supervision of Complex Systems. His PhD dissertation "On-line Monitoring and Diagnosis of a Multi-Agent System: a Model-Based Approach" has been awarded by Associazione Italiana per l'Intelligenza Artificiale (AIxIA) [Italian Association for Artificial Intelligence] as the best Phd thesis on AI discussed between 2007 and 2008. His main research interests include Model-Based Reasoning and Diagnosis, Multiagent Planning, and plan execution in unpredictable and partially observable environments.