Un peu d'action, connaissance, croyance et beaucoup de logique modale

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.Ce travail présente quatre des mes résultats de recherche les plus importants obtenus après ma thèse de doctorat, c’est-à-dire, de 2008 à 2019. Après un bref état de l’art, un formalisme visant à modéliser la responsabilité dans des environnements multi-agents est mis en avant. Ce formalisme, appelé CEDL, est une logique modale qui contient des opérateurs épistémiques et dynamiques ainsi que d’autres opérateurs définis comme des abréviations, telles que l’obligation, la capacité des agents et la capacité de savoir des agents. Le deuxième résultat est une évolution de CEDL, appelée ATDEL. Cette logique vise à modéliser les capacités et les connaissances des agents dans un cadre temporel. Elle permet des spécifications des systèmes beaucoup plus courtes que celles de CEDL. De plus, outre une axiomatisation, des algorithmes de vérification de modèles et de vérification de la satisfiabilité de formules sont proposés. Le troisième résultat est une adaptation de la théorie de révision de croyances AGM à des scénarios multi-agents.Les postulats d’expansion et de révision AGM sont généralisés à de tels scénarios et des opérateurs concrets pour l’expansion et la révision des croyances multi-agents sont proposés. Le dernier résultat présenté porte sur le raisonnement automatique pour les logiques modales. Des méthodes de vérification de la satisfiabilité de formules dans les logiques modales K et KT5 sont proposés. Des expériences pratiques montrent que notre techniques surpasse toutes les méthodes alternatives