My research interests regard many aspects of formal methods for Artificial Intelligence. In particular, I work on verification and synthesis problems for multi-agent systems, knowledge representation, strategic reasoning, logic, games, and automata theory.

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.


Selected Talks

  • From Synthesis to Rational Synthesis: A Logic-Based Approach to Multi-Agent Systems
  • Trace Alignment and Timed-Trace Alignment: An Automata-Based Approach
  • Logics for Multi-Agent Systems Verification
    • 15/12/2015: Seminar Talk, Imperial College London
  • Strategy Logic: A Powerful Formalism for Game-Theoretic Issues
    • 24/11/2014: Seminar Talk, University of California Santa Cruz
  • Le Logiche Temporali e di Strategia nell’Ambito della Verifica Formale
    • 05/04/2013: 2013 SeLP Meeting, University of Naples ‘Federico II’

Community Service

Past Community Service


  • I am member of AIxIA, Italian Association for Artificial Intelligence.
  • I am member of AILA, Italian Association for Logics and Applications.
  • I am member of GNCS, Italian Association for Scientific Calculus.
  • I support CLAIRE.