• HDR Defended on :
  • Dec 5, 2019 • salle des thèses, Faculté des sciences Jean Perrin


This work presents four of the most important research results obtained after my Ph.D., i.e., from 2008 until 2019. After a brief state of the art, a formalism aiming at modelling responsibility in multi-agent environments is put forward. This formalism, called CEDL, is a modal logic that contains epistemic and dynamic operators as well as some other operators defined as abbreviations, such as obligation, agents abilities and agents knowing how abilities. The second result is an evolution of CEDL, called ATDEL. This logic aims at modelling agents abilities and knowledge trough time. It permits system specifications that are much smaller than CEDL. In addition, apart from an axiomatisation, algorithms for model checking and satisfiability checking of formulas are also provided. The third result is an adaptation of AGM belief revision theory to multi-agent scenarios. Multi-agent versions of expansion and revision postulates are proposed. The last result presented in this work is about modal logic automated reasoning. Methods for satisfiability checking of formulas in K and KT5 are proposed. Practical experiments show that our technique outperforms alternative approaches.


  • Anthony Hunter, Professor at University College London, United Kingdom
  • Odile Papini, Professor at the University of Aix-Marseille, France
  • Umberto Straccia, Director of Research at CNR, Italy


  • Salem Benferhat, professor at the University of Artois, France
  • Philippe Besnard, research director at CNRS, France
  • Sébastien Konieczny, research director at CNRS, France