Logic and Automata

During my PhD, I focused on the study of Logics for the Verification and Synthesis of strategic behavior in multi-agent systems. In particular, I gave my decisive contribution to the development of Strategy Logic: a language now widely applied in AI and formal methods to reason about strategies and actions in multi-agent systems.

Rational Synthesis

During my years as a research associate at the University of Oxford, University of Leicester, and Chalmers University, my main focus was on Rational Verification and Synthesis, concerning the synthesis of equilibria for games that are used as a modelling tool for multi-agent interacting scenarios, such as autonomous-driving cars, automated wharehouse, and the like. I have contributed to the development of EVE: a formal verification tool for the automated analysis of temporal equilibrium properties of concurrent and multi-agent systems.

Finite Trace

I focused on defining and solving synthesis variants of finite temporal specifications. The problem has direct applications in the areas of planning, business process management, as well as robotics, where agents tasks are assumed to be of finite duration.

Normative Systems

My recent focus has been on Normative Systems, concerning the problem of regulating MAS by means of norms and other formally defined machineries, employed to guarantee correct-by-construction behaviour of systems from a global/designer point of view.