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.

shown on this cover page is limited to 10 maximum.

Abstract We generalize the language of substructural logics interpreted over the ternary relational semantics. This is motivated by our intention to capture within the logical framework of substructural logics various logic-based formalisms dealing with common sense reasoning and logical dynamics. This initiative is based on the key observation that an update can be represented abstractly by the ternary relation of the substructural framework: the first argument of the ternary relation represents an initial situation, the second an informative event and the third the resulting situation after the occurrence of the informative event. Refining the language of substructural logics may allow us to account for the fine-grained reasoning present in common sense reasoning. Thus, we introduce three triples of connectives that are interconnected by means of cyclic permutations. The usual fusion, implication and co-implication connectives form one of these triples. We define a cut-free display calculus for our language that generalizes the display calculus for modal logic. We do not resort to structural connectives for truth constants and we show how we can obtain our display rules using Gaggle Theory. We prove the soundness and strong completeness of our display calculus via a Henkin-style construction. Using correspondence results from substructural logics, we also obtain sound and complete display calculi for a wide variety of classical and substructural logics. Then, we define dual substructural connectives and we provide a display calculus for our language extended with these dual connectives. Finally, we focus on the specific case of bi-intuitionistic logic for which we provide a novel sound and strongly complete display calculus. In a companion article (Aucher, 2016, J. Logic Comput.), we provide a sequent calculus for update logic that generalizes the non-associative Lambek calculus and a sequent calculus for dynamic epistemic logic that extends this sequent calculus for update logic.

International audience

AGM belief revision theory and the BMS framework of dynamic epistemic logic both deal with the formalization of belief change, the former in a single-agent setting and the latter in a multi-agent setting. In this article, we study the relation between these two formalisms.To be fair,we restrict our attention to the AGM operation of expansion since the original BMS framework does not allow for belief revision. The generalization of the AGM operation of revision to the multi-agent setting is dealt with in the companion paper [Aucher (2010, Logic Journal of the IGPL, 18, 530–558)]. Besides, because AGM theory follows the internal approach, instead of the original BMS framework we define and deal with its internal version. This allows us to show that the AGM operation of expansion can naturally be viewed in the multi-agent setting of the BMS framework as the operation of private announcement, which goes against the claims of [van Ditmarsch, van der Hoek and Kooi (2004, Advances in Modal Logic, 335–346)]. In parallel, we also provide conditions under which seriality of accessibility relations is preserved during an update, in the BMS framework as well as its internal version: it is a preliminary step towards the introduction of revision mechanisms into these frameworks.

The insight of the BMS logical framework (proposed by Baltag, Moss and Solecki) is to represent how an event is perceived by several agents very similarly to the way one represents how a static situation is perceived by them: by means of a Kripke model. There are however some differences between the definitions of an epistemic model (representing the static situation) and an event model. In this paper we restore the symmetry. The resulting logical framework allows, unlike any other one, to express statements about ongoing events and to model the fact that our perception of events (and not only of the static situation) can also be updated due to other events. We axiomatize it and prove its decidability. Finally, we show that it embeds the BMS one if we add common belief operators.