This paper provides a complete characterization of epistemic models in which distributed knowledge complies with the principle of full communication (van der Hoek et al., 1999; Gerbrandy, 1999). It also introduces an extended notion of bisimulation and corresponding model comparison games that match the expressive power of distributed knowledge operators.

While dynamic epistemic logics with common knowledge have been extensively studied, dynamic epistemic logics with distributed knowledge have so far received far less attention. In this paper we study extensions of public announcement logic ( $\mathcal{PAL }$ ) with distributed knowledge, in particular their expressivity, axiomatisations and complexity. $\mathcal{PAL }$ extended only with distributed knowledge is not more expressive than standard epistemic logic with distributed knowledge. Our focus is therefore on $\mathcal{PACD }$ , the result of adding both common and (...) distributed knowledge to $\mathcal{PAL }$ , which is more expressive than each of its component logics. We introduce an axiomatisation of $\mathcal{PACD }$ , which is not surprising: it is the combination of well-known axioms. The completeness proof, however, is not trivial, and requires novel combinations and extensions of techniques for dealing with $S5$ knowledge, distributed knowledge, common knowledge and public announcements at the same time. We furthermore show that $\mathcal{PACD }$ is decidable, more precisely that it is $\textsc {exptime}$ -complete. This result also carries over to $\mathcal{S 5\mathcal CD }$ with common and distributed knowledge operators for all coalitions (and not only the grand coalition). Finally, we propose a notion of a trans-bisimulation to generalise certain results and give deeper insight into the proofs. (shrink)

Public announcement logic is an extension of multiagent epistemic logic with dynamic operators to model the informational consequences of announcements to the entire group of agents. We propose an extension of public announcement logic with a dynamic modal operator that expresses what is true after any announcement: after which , does it hold that Kφ? We give various semantic results and show completeness for a Hilbert-style axiomatization of this logic. There is a natural generalization to a logic for arbitrary events.

Multi-modal versions of propositional logics S5 or S4—commonly accepted as logics of knowledge—are capable of describing static states of knowledge but they do not reflect how the knowledge changes after communications among agents. In the present paper (part of broader research on logics of knowledge and communications) we define extensions of the logic S5 which can deal with public communications. The logics have natural semantics. We prove some completeness, decidability and interpretability results and formulate a general method that solves certain (...) kind of problems involving public communications—among them well known puzzles of Muddy Children and Mr. Sum & Mr. Product. As the paper gives a formal logical treatment of the operation of restriction of the universe of a Kripke model, it contributes also to investigations of semantics for modal logics. (shrink)

Dynamic Epistemic Logic is the logic of knowledge change. This book provides various logics to support such formal specifications, including proof systems. Concrete examples and epistemic puzzles enliven the exposition. The book also offers exercises with answers. It is suitable for graduate courses in logic. Many examples, exercises, and thorough completeness proofs and expressivity results are included. A companion web page offers slides for lecturers and exams for further practice.

Coalition announcement logic is one of the family of the logics of quantified announcements. It allows us to reason about what a coalition of agents can achieve by making announcements in the setting where the anti-coalition may have an announcement of their own to preclude the former from reaching its epistemic goals. In this paper, we describe a PSPACE-complete model checking algorithm for CAL that produces winning strategies for coalitions. The algorithm is implemented in a proof-of-concept model checker.

Arbitrary public announcement logic ) reasons about how the knowledge of a set of agents changes after true public announcements and after arbitrary announcements of true epistemic formulas. We consider a variant of arbitrary public announcement logic called positive arbitrary public announcement logic ), which restricts arbitrary public announcements to announcement of positive formulas. Positive formulas prohibit statements about the ignorance of agents. The positive formulas correspond to the universal fragment in first-order logic. As two successive announcements of positive formulas (...) need not correspond to the announcement of a positive formula, \ is rather different from \. We show that \ is more expressive than public announcement logic \, and that \ is incomparable with \. We also provide a sound and complete infinitary axiomatisation. (shrink)

Current dynamic epistemic logics for analyzing effects of informational events often become cumbersome and opaque when common knowledge is added for groups of agents. Still, postconditions involving common knowledge are essential to successful multi-agent communication. We propose new systems that extend the epistemic base language with a new notion of ‘relativized common knowledge’, in such a way that the resulting full dynamic logic of information flow allows for a compositional analysis of all epistemic postconditions via perspicuous ‘reduction axioms’. We also (...) show how such systems can deal with factual alteration, rather than just information change, making them cover a much wider range of realistic events. After a warm-up stage of analyzing logics for public announcements, our main technical results are expressivity and completeness theorems for a much richer logic that we call LCC. This is a dynamic epistemic logic whose static base is propositional dynamic logic (PDL), interpreted epistemically. This system is capable of expressing all model-shifting operations with finite action models, while providing a compositional analysis for a wide range of informational events. This makes LCC a serious candidate for a standard in dynamic epistemic logic, as we illustrate by analyzing some complex communication scenarios, including sending successive emails with both ‘cc’ and ‘bcc’ lines, and other private announcements to subgroups. Our proofs involve standard modal techniques, combined with a new application of Kleene’s theorem on finite automata, as well as new Ehrenfeucht games of model comparison. (shrink)

In an information state where various agents have both factual knowledge and knowledge about each other, announcements can be made that change the state of information. Such informative announcements can have the curious property that they become false because they are announced. The most typical example of that is 'fact p is true and you don't know that', after which you know that p, which entails the negation of the announcement formula. The announcement of such a formula in a given (...) information state is called an unsuccessful update. A successful formula is a formula that always becomes common knowledge after being announced. Analysis of information systems and 'philosophical puzzles' reveals a growing number of dynamic phenomena that can be described or explained by unsuccessful updates. This increases our understanding of such philosophical problems. We also investigate the syntactic characterization of the successful formulas. (shrink)

There are several ways to quantify over public announcements. The most notable are reflected in arbitrary, group, and coalition announcement logics, with the latter being the least studied so far. In the present work, we consider coalition announcements through the lens of group announcements, and provide a complete axiomatisation of a logic with coalition announcements. To achieve this, we employ a generalisation of group announcements. Moreover, we study some logical properties of both coalition and group announcements that have not been (...) studied before. (shrink)