Guillaume Aucher

JAIR Journal 2025 Journal Article

From Knowledge to Action: Logics of Permitted and Obligatory Announcements

• Xu Li
• Guillaume Aucher
• Dov Gabbay
• Réka Markovich

We formalize the notions of “permitted and obligatory announcements” in the context of information security, such as privacy policy compliance. In a sender-receiver setting, we define the sender’s permitted and obligatory announcements in terms of the receiver’s ideal epistemic states (i.e., the epistemic states that comply with the given security policies). We propose two logics, LPOA and DLPOA, to reason about permitted and obligatory announcements in static and dynamic contexts, respectively. These two logics are completely axiomatized, and we also study generalizations in which the receiver’s knowledge is characterized by non-S5 logics. Our paper makes two main contributions to the formalization of permitted and obligatory announcements: First, we clarify the interplay between the sender’s permitted and obligatory announcements and the receiver’s knowledge. Second, we distinguish between weakly and strongly permitted announcements.

FLAP Journal 2020 Journal Article

Towards Universal Logic: Gaggle Logics.

• Guillaume Aucher

A class of non–classical logics called gaggle logics is introduced, based on a Kripke–style relational semantics and inspired by Dunn’s gaggle theory. These logics deal with connectives of arbitrary arity and we show that they capture a wide range of non–classical logics. In particular, we list the 96 binary connectives and 16 unary connectives of basic gaggle logic and relate their truth conditions to the non-classical logics of the literature. We establish connections between gaggle theory and group theory. We show that Dunn’s abstract law of residuation corresponds to an action of transpositions of the symmetric group on the set of connectives of gaggle logics and that Dunn’s families of connectives are orbits of the same action. Other operations on connectives, such as dual and Boolean negation, are also reformulated in terms of actions of groups and their combination is defined by means of free groups and free products. We show how notions of groups arise naturally from our gaggle logics and how gaggle logics can be canonically defined from given groups. Our other main contribution deals with the proof theory of gaggle logics. We show how sound and complete calculi can be systematically computed from any basic gaggle logic with or without Boolean connectives. These calculi are display calculi and we prove that the cut rule can be systematically eliminated from proofs. This allows us to prove that basic gaggle logics are decidable.

FLAP Journal 2019 Journal Article

Principles for a Judgement Editor Based on Binary Decision Diagrams.

• Guillaume Aucher
• Jean Berbinau
• Marie-Laure Morin

IJCAI Conference 2015 Conference Paper

Multi-Agent Only Knowing on Planet Kripke

• Guillaume Aucher
• Vaishak Belle

The idea of only knowing is a natural and intuitive notion to precisely capture the beliefs of a knowledge base. However, an extension to the many agent case, as would be needed in many applications, has been shown to be far from straightforward. For example, previous Kripke frame-based accounts appeal to proof-theoretic constructions like canonical models, while more recent works in the area abandoned Kripke semantics entirely. We propose a new account based on Moss’ characteristic formulas, formulated for the usual Kripke semantics. This is shown to come with other benefits: the logic admits a group version of only knowing, and an operator for assessing the epistemic entrenchment of what an agent or a group only knows is definable. Finally, the multi-agent only knowing operator is shown to be expressible with the cover modality of classical modal logic, which then allows us to obtain a completeness result for a fragment of the logic.

LORI Conference 2015 Conference Paper

Sabotage Modal Logic: Some Model and Proof Theoretic Aspects

• Guillaume Aucher
• Johan van Benthem
• Davide Grossi

Abstract We investigate some model and proof theoretic aspects of sabotage modal logic. The first contribution is to prove a characterization theorem for sabotage modal logic as the fragment of first-order logic which is invariant with respect to a suitably defined notion of bisimulation (called sabotage bisimulation). The second contribution is to provide a sound and complete tableau method for sabotage modal logic. We also chart a number of open research questions concerning sabotage modal logic, aiming at integrating it within the current landscape of logics of model update.

KR Conference 2014 Short Paper

Axioms. 2 and. 4 as Interaction Axioms

• Guillaume Aucher

In epistemic logic, some axioms dealing with the notion of knowledge are rather convoluted and it is difficult to give them an intuitive interpretation, even if some of them, like. 2 and. 4, are considered by some epistemic logicians to be key axioms. We show that they can be characterized in terms of understandable interaction axioms relating knowledge and belief. In order to show it, we first present a theory dealing with the characterization of axioms in terms of interaction axioms in modal logic. We then apply the main results and methods of this theory to obtain our results related to epistemic logic.

IJCAI Conference 2013 Conference Paper

An Alternative Axiomatization of DEL and Its Applications

• Yanjing Wang
• Guillaume Aucher

In this paper, we provide a new axiomatization of the event-model-based Dynamic Epistemic Logic, based on the completeness proof method proposed in [Wang and Cao, 2013]. This axiomatization does not use any of the standard reduction axioms, but naturally captures the essence of the update product. We demonstrate the use of our new axiomatization and the corresponding proof techniques by three sets of results: characterization theorems of the update operations, representation theorems of the DEL-generatable epistemic temporal structures given a fixed event model, and a complete axiomatization of DEL on models with protocols.

TARK Conference 2013 Conference Paper

On the Complexity of Dynamic Epistemic Logic

• Guillaume Aucher
• François Schwarzentruber

Although Dynamic Epistemic Logic (DEL) is an influential logical framework for representing and reasoning about information change, little is known about the computational complexity of its associated decision problems. In fact, we only know that for public announcement logic, a fragment of DEL, the satisfiability problem and the model-checking problem are respectively PSPACE-complete and in P. We contribute to fill this gap by proving that for the DEL language with event models, the model-checking problem is, surprisingly, PSPACE-complete. Also, we prove that the satisfiability problem is NEXPTIME-complete. In doing so, we provide a sound and complete tableau method deciding the satisfiability problem.

IJCAI Conference 2013 Conference Paper

Undecidability in Epistemic Planning

• Guillaume Aucher
• Thomas Bolander

Dynamic epistemic logic (DEL) provides a very expressive framework for multi-agent planning that can deal with nondeterminism, partial observability, sensing actions, and arbitrary nesting of beliefs about other agents’ beliefs. However, as we show in this paper, this expressiveness comes at a price. The planning framework is undecidable, even if we allow only purely epistemic actions (actions that change only beliefs, not ontic facts). Undecidability holds already in the S5 setting with at least 2 agents, and even with 1 agent in S4. It shows that multi-agent planning is robustly undecidable if we assume that agents can reason with an arbitrary nesting of beliefs about beliefs. We also prove a corollary showing undecidability of the DEL model checking problem with the star operator on actions (iteration).

JELIA Conference 2012 Conference Paper

Generalized DEL-Sequents

• Guillaume Aucher
• Bastien Maubert
• François Schwarzentruber

Abstract Let us consider a sequence of formulas providing partial information about an initial situation, about a set of events occurring sequentially in this situation, and about the resulting situation after the occurrence of each event. From this whole sequence, we want to infer more information, either about the initial situation, or about one of the events, or about the resulting situation after one of the events. Within the framework of Dynamic Epistemic Logic (DEL), we show that these different kinds of problems are all reducible to the problem of inferring what holds in the final situation after the occurrence of all the events. We then provide a tableau method deciding whether this kind of inference is valid. We implement it in LotrecScheme and show that these inference problems are NEXPTIME-complete. We extend our results to the cases where the accessibility relation is serial and reflexive and illustrate them with the coordinated attack problem.

AILAW Journal 2011 Journal Article

A dynamic logic for privacy compliance

• Guillaume Aucher
• Guido Boella
• Leendert van der Torre

Abstract Knowledge based privacy policies are more declarative than traditional action based ones, because they specify only what is permitted or forbidden to know, and leave the derivation of the permitted actions to a security monitor. This inference problem is already non trivial with a static privacy policy, and becomes challenging when privacy policies can change over time. We therefore introduce a dynamic modal logic that permits not only to reason about permitted and forbidden knowledge to derive the permitted actions, but also to represent explicitly the declarative privacy policies together with their dynamics. The logic can be used to check both regulatory and behavioral compliance, respectively by checking that the permissions and obligations set up by the security monitor of an organization are not in conflict with the privacy policies, and by checking that these obligations are indeed enforced.

KR Conference 2010 Conference Paper

characterizing updates in dynamic epistemic logic

• Guillaume Aucher

Dynamic Epistemic Logic: BMS Revisited In logical formalisms for representing and reasoning about events and their effects, it is often difficult to represent situations during the occurrence of events. 1 The event calculus for instance (Shanahan 1997) is a narrative-based formalism, and as such is more appropriate for planing and reasoning about a given course of events (via logic programming) than for representing a situation and updating this representation as new events start or terminate. In (Aucher 2009a), we addressed this issue and others within the paradigm of dynamic epistemic logic. In this section, we are going to give an account of a simplified version of the general framework developed in (Aucher 2009a). Dynamic epistemic logic deals with the representation of situations in a multi-agent and dynamic setting. It allows to express in a uniform way statements about: 1. what is true about an initial situation 2. what is true about an event occurring in this situation 3. what is true about the resulting situation after the event has occurred. We axiomatize in this framework what we can infer about (3) given (1) and (2), introducing thereby new techniques to prove completeness. We also show that this axiomatization is decidable. Besides being useful for reasoning about actions, it provides a natural characterization of the product update of dynamic epistemic logic. 2. 1 A Language to Talk about Events If we want to represent a situation during the occurrence of events, we need to be able not only to express static statements about the situation but also statements about events occurring in this situation. This leads us to define two languages L and L to express these two kinds of statements. Let Φ and Φ be two finite and disjoint sets of propositional letters. G is a finite set of agents.

TARK Conference 2009 Conference Paper

BMS revisited

• Guillaume Aucher

LORI Conference 2009 Conference Paper

Dynamic Context Logic

• Guillaume Aucher
• Davide Grossi
• Andreas Herzig
• Emiliano Lorini

Abstract Building on a simple modal logic of context, the paper presents a dynamic logic characterizing operations of contraction and expansion on theories. We investigate the mathematical properties of the logic, and show how it can capture some aspects of the dynamics of normative systems once they are viewed as logical theories.

JELIA Conference 2008 Conference Paper

Consistency Preservation and Crazy Formulas in BMS

• Guillaume Aucher

Abstract We provide conditions under which seriality is preserved during an update in the BMS framework. We consider not only whether the entire updated model is serial but also whether its generated submodels are serial. We also introduce the notion of crazy formulas which are formulas such that after being publicly announced at least one of the agents’ beliefs become inconsistent.

AAMAS Conference 2008 Conference Paper

Internal models and private multi agent belief revision

• Guillaume Aucher

We generalize AGM belief revision theory to the multi-agent case. To do so, we first generalize the semantics of the singleagent case, based on the notion of interpretation, to the multi-agent case. Then we show that, thanks to the shape of our new semantics, all the results of the AGM framework transfer. Afterwards we investigate some postulates that are specific to our multi-agent setting.