Ignorance is bliss : observability-based dynamic epistemic logics and their applications

Dans les logiques épistémiques, la connaissance est généralement modélisée par un graphe de mondes possibles, qui correspondent aux alternatives à l'état actuel du monde. Ainsi, les arêtes entre les mondes représentent l'indistinguabilité. Connaître une proposition signifie que cette proposition est vraie dans toutes les alternatives possibles. Les informaticiens théoriques ont cependant remarqué que cela a conduit à plusieurs problèmes, à la fois intuitifs et techniques : plus un agent est ignorant, plus elle a d'alternatives à examiner ; les modèles peuvent alors devenir trop grands pour la vérification de système. Ils ont récemment étudié comment la connaissance pourrait être réduite à la notion de visibilité. Intuitivement, l'idée de base est que quand un agent voit quelque chose, alors elle sait sa valeur de vérité. A l'inverse, toute combinaison de valeurs de vérité des variables non observables est possible pour l'agent. Ces informations d'observabilité permettent de reconstituer la sémantique standard de la connaissance : deux mondes sont indistinguables pour un agent si et seulement si chaque variable observée par cet agent a la même valeur dans les deux mondes. Notre objectif est de démontrer que les logiques épistémiques fondées sur la visibilité constituent un outil approprié pour plusieurs applications importantes dans le domaine de l'intelligence artificielle. Dans le cadre actuel de ces logiques de visibilité, chaque agent a un ensemble de variables propositionnelles qu'elle peut observer ; ces visibilités sont constantes à travers le modèle. Cela accompagne une hypothèse forte : les visibilités sont connues de tous, et sont même connaissance commune. De plus, la construction de la connaissance à partir de la visibilité entraîne des validités contre-intuitives, la plus importante étant que l'opérateur de la connaissance distribue sur les disjonctions de littéraux : si un agent sait que p ou q est vrai, alors elle sait que p est vrai ou que q est vrai, parce qu'elle peut les voir. Dans cette thèse, nous proposons des solutions à ces deux problèmes et les illustrons sur diverses applications telles que la planification épistémique ou les jeux booléens épistémiques, et sur des exemples plus spécifiques tels que le problème des enfants sales ou le problème du bavardage. Nous étudions en outre des propriétés formelles des logiques que nous concevons, fournissant axiomatisations et résultats de complexité.In epistemic logic, knowledge is usually modelled by a graph of possible worlds, representing the alternatives to the current state of the world. So edges between worlds stand for indistinguishability. To know a proposition means that that proposition is true in all possible alternatives. Theoretical computer scientists however noticed that this led to several issues, both intuitively and technically: the more an agent is ignorant, the more alternatives she must consider; models may then become too big for system verification. They recently investigated how knowledge could be reduced to the notion of visibility. Intuitively, the basic idea is that when an agent sees something, then she knows its truth value. The other way round, any combination of truth values of the non-observable variables is possible for the agent. Such observability information allows us to reconstruct the standard semantics of knowledge: two worlds are indistinguishable for an agent if and only if every variable observed by her has the same value in both worlds. We aim to demonstrate that visibility-based epistemic logics provide a suitable tool for several important applications in the field of artificial intelligence. In the current settings of these logics of visibility, every agent has a set of propositional variables that she can observe; these visibilities are constant across the model. This comes with a strong assumption: visibilities are known to everyone, and are even common knowledge. Moreover, constructing knowledge from visibility brings about counter-intuitive validities, the most important being that the knowledge operator distributes over disjunction of literals: if an agent knows that p or q is true, then she knows that p is true or that q is true because she can see them. In this thesis, we propose solutions to these two problems and illustrate them on various applications such as epistemic planning or epistemic boolean games, and on more specific examples such as the muddy children problem or the gossip problem. We moreover study formal properties of the logics we design, providing axiomatizations and complexity results