Hans van Ditmarsch

Philippe Balbiani, Hans van Ditmarsch, Clara Lerouvillois

We investigate a logic for asynchronous announcements wherein the sending of the messages by the environment is separated from their reception by the individual agents. Both come with different modalities. In the logical semantics, formulas are interpreted in a world of a Kripke model but given a history of prior announcements and receptions that already happened. An axiomatisation AA for such a logic has been given in prior work, for the formulas that are valid when interpreted in the Kripke model before any such announcements have taken place. This axiomatisation is a reduction system wherein one can show that every formula is equivalent to a purely epistemic formula without dynamic modalities for announcements and receptions. We propose a generalisation AA* of this axiomatisation, for the formulas that are valid when interpreted in the Kripke model given any history of prior announcements and receptions of announcements. It does not extend the axiomatisation AA, for example it is no longer valid that nobody has received any message. Unlike AA, this axiomatisation AA* is infinitary and it is not a reduction system.

Giorgio Cignarale, Hans van Ditmarsch, Stephan Felber et al.

We investigate self-correcting gossip protocols with errors. In distributed computing, protocols with errors have been widely investigated in temporal epistemic logics. Instead, we propose a dynamic epistemic logic. We show how to correct transmission errors due to faulty messages without a central authority coordinating protocol execution, how this affects optimality, and how this compares to bounded memory and full information protocols.

Hans van Ditmarsch, Sunil Simon

We introduce Boolean Observation Games, a subclass of multi-player finite strategic games with incomplete information and qualitative objectives. In Boolean observation games, each player is associated with a finite set of propositional variables of which only it can observe the value, and it controls whether and to whom it can reveal that value. It does not control the given, fixed, value of variables. Boolean observation games are a generalization of Boolean games, a well-studied subclass of strategic games but with complete information, and wherein each player controls the value of its variables. In Boolean observation games, player goals describe multi-agent knowledge of variables. As in classical strategic games, players choose their strategies simultaneously and therefore observation games capture aspects of both imperfect and incomplete information. They require reasoning about sets of outcomes given sets of indistinguishable valuations of variables. An outcome relation between such sets determines what the Nash equilibria are. We present various outcome relations, including a qualitative variant of ex-post equilibrium. We identify conditions under which, given an outcome relation, Nash equilibria are guaranteed to exist. We also study the complexity of checking for the existence of Nash equilibria and of verifying if a strategy profile is a Nash equilibrium. We further study the subclass of Boolean observation games with `knowing whether' goal formulas, for which the satisfaction does not depend on the value of variables. We show that each such Boolean observation game corresponds to a Boolean game and vice versa, by a different correspondence, and that both correspondences are precise in terms of existence of Nash equilibria.

Hans van Ditmarsch, Malvin Gattinger, Rahim Ramezanian

A gossip protocol is a procedure for sharing secrets in a network. The basic action in a gossip protocol is a pairwise message exchange (telephone call) wherein the calling agents exchange all the secrets they know. An agent who knows all secrets is an expert. The usual termination condition is that all agents are experts. Instead, we explore protocols wherein the termination condition is that all agents know that all agents are experts. We call such agents super experts. We also investigate gossip protocols that are common knowledge among the agents. Additionally, we model that agents who are super experts do not make and do not answer calls, and that this is common knowledge. We investigate conditions under which protocols terminate, both in the synchronous case, where there is a global clock, and in the asynchronous case, where there is not. We show that a commonly known protocol with engaged agents may terminate faster than the same commonly known protocol without engaged agents.

Hans van Ditmarsch

In this survey we review dynamic epistemic logics with modalities for quantification over information change. Of such logics we present complete axiomatizations, focussing on axioms involving the interaction between knowledge and such quantifiers, we report on their relative expressivity, on decidability and on the complexity of model checking and satisfiability, and on applications. We focus on open problems and new directions for research.

Francesco Belardinelli, Hans van Ditmarsch, Wiebe van der Hoek

In this paper we introduce {\em global and local announcement logic} (GLAL), a dynamic epistemic logic with two distinct announcement operators -- $[φ]^+_A$ and $[φ]^-_A$ indexed to a subset $A$ of the set $Ag$ of all agents -- for global and local announcements respectively. The boundary case $[φ]^+_{Ag}$ corresponds to the public announcement of $φ$, as known from the literature. Unlike standard public announcements, which are {\em model transformers}, the global and local announcements are {\em pointed model transformers}. In particular, the update induced by the announcement may be different in different states of the model. Therefore, the resulting computations are trees of models, rather than the typical sequences. A consequence of our semantics is that modally bisimilar states may be distinguished in our logic. Then, we provide a stronger notion of bisimilarity and we show that it preserves modal equivalence in GLAL. Additionally, we show that GLAL is strictly more expressive than public announcement logic with common knowledge. We prove a wide range of validities for GLAL involving the interaction between dynamics and knowledge, and show that the satisfiability problem for GLAL is decidable. We illustrate the formal machinery by means of detailed epistemic scenarios.

Hans van Ditmarsch, Michael Ian Hartley, Barteld Kooi et al.

We present four logic puzzles and after that their solutions. Joseph Yeo designed 'Cheryl's Birthday'. Mike Hartley came up with a novel solution for 'One Hundred Prisoners and a Light Bulb'. Jonathan Welton designed 'A Blind Guess' and 'Abby's Birthday'. Hans van Ditmarsch and Barteld Kooi authored the puzzlebook 'One Hundred Prisoners and a Light Bulb' that contains other knowledge puzzles, and that can also be found on the webpage http://personal.us.es/hvd/lightbulb.html dedicated to the book.

Philippe Balbiani, Hans van Ditmarsch, Saúl Fernández González

We propose a multi-agent epistemic logic of asynchronous announcements, where truthful announcements are publicly sent but individually received by agents, and in the order in which they were sent. Additional to epistemic modalities the logic contains dynamic modalities for making announcements and for receiving them. What an agent believes is a function of her initial uncertainty and of the announcements she has received. Beliefs need not be truthful, because announcements already made may not yet have been received. As announcements are true when sent, certain message sequences can be ruled out, just like inconsistent cuts in distributed computing. We provide a complete axiomatization for this \emph{asynchronous announcement logic} (AA). It is a reduction system that also demonstrates that any formula in $AA$ is equivalent to one without dynamic modalities, just as for public announcement logic. A detailed example modelling message exchanging processes in distributed computing in $AA$ closes our investigation.

Thomas Ågotnes, Hans van Ditmarsch, Yanjing Wang

A true lie is a lie that becomes true when announced. In a logic of announcements, where the announcing agent is not modelled, a true lie is a formula (that is false and) that becomes true when announced. We investigate true lies and other types of interaction between announced formulas, their preconditions and their postconditions, in the setting of Gerbrandy's logic of believed announcements, wherein agents may have or obtain incorrect beliefs. Our results are on the satisfiability and validity of instantiations of these semantically defined categories, on iterated announcements, including arbitrarily often iterated announcements, and on syntactic characterization. We close with results for iterated announcements in the logic of knowledge (instead of belief), and for lying as private announcements (instead of public announcements) to different agents. Detailed examples illustrate our lying concepts.

Mikkel Birkegaard Andersen, Thomas Bolander, Hans van Ditmarsch et al.

Plausibility models are Kripke models that agents use to reason about knowledge and belief, both of themselves and of each other. Such models are used to interpret the notions of conditional belief, degrees of belief, and safe belief. The logic of conditional belief contains that modality and also the knowledge modality, and similarly for the logic of degrees of belief and the logic of safe belief. With respect to these logics, plausibility models may contain too much information. A proper notion of bisimulation is required that characterises them. We define that notion of bisimulation and prove the required characterisations: on the class of image-finite and preimage-finite models (with respect to the plausibility relation), two pointed Kripke models are modally equivalent in either of the three logics, if and only if they are bisimilar. As a result, the information content of such a model can be similarly expressed in the logic of conditional belief, or the logic of degrees of belief, or that of safe belief. This, we found a surprising result. Still, that does not mean that the logics are equally expressive: the logics of conditional and degrees of belief are incomparable, the logics of degrees of belief and safe belief are incomparable, while the logic of safe belief is more expressive than the logic of conditional belief. In view of the result on bisimulation characterisation, this is an equally surprising result. We hope our insights may contribute to the growing community of formal epistemology and on the relation between qualitative and quantitative modelling.

Hans van Ditmarsch, Joseph Y. Halpern, Wiebe van der Hoek et al.

This chapter provides an introduction to some basic concepts of epistemic logic, basic formal languages, their semantics, and proof systems. It also contains an overview of the handbook, and a brief history of epistemic logic and pointers to the literature.

Jie Fan, Yanjing Wang, Hans van Ditmarsch

Knowing whether a proposition is true means knowing that it is true or knowing that it is false. In this paper, we study logics with a modal operator Kw for knowing whether but without a modal operator K for knowing that. This logic is not a normal modal logic, because we do not have Kw (phi -> psi) -> (Kw phi -> Kw psi). Knowing whether logic cannot define many common frame properties, and its expressive power less than that of basic modal logic over classes of models without reflexivity. These features make axiomatizing knowing whether logics non-trivial. We axiomatize knowing whether logic over various frame classes. We also present an extension of knowing whether logic with public announcement operators and we give corresponding reduction axioms for that. We compare our work in detail to two recent similar proposals.

Andrés Cordón-Franco, Hans van Ditmarsch, David Fernández-Duque et al.

In the generalized Russian cards problem, the three players Alice, Bob and Cath draw a,b and c cards, respectively, from a deck of a+b+c cards. Players only know their own cards and what the deck of cards is. Alice and Bob are then required to communicate their hand of cards to each other by way of public messages. The communication is said to be safe if Cath does not learn the ownership of any specific card; in this paper we consider a strengthened notion of safety introduced by Swanson and Stinson which we call k-safety. An elegant solution by Atkinson views the cards as points in a finite projective plane. We propose a general solution in the spirit of Atkinson's, although based on finite vector spaces rather than projective planes, and call it the `geometric protocol'. Given arbitrary c,k>0, this protocol gives an informative and k-safe solution to the generalized Russian cards problem for infinitely many values of (a,b,c) with b=O(ac). This improves on the collection of parameters for which solutions are known. In particular, it is the first solution which guarantees $k$-safety when Cath has more than one card.

Laura Bozzelli, Hans van Ditmarsch, Tim French et al.

In this paper we present {\em refinement modal logic}. A refinement is like a bisimulation, except that from the three relational requirements only `atoms' and `back' need to be satisfied. Our logic contains a new operator 'all' in addition to the standard modalities 'box' for each agent. The operator 'all' acts as a quantifier over the set of all refinements of a given model. As a variation on a bisimulation quantifier, this refinement operator or refinement quantifier 'all' can be seen as quantifying over a variable not occurring in the formula bound by it. The logic combines the simplicity of multi-agent modal logic with some powers of monadic second-order quantification. We present a sound and complete axiomatization of multi-agent refinement modal logic. We also present an extension of the logic to the modal mu-calculus, and an axiomatization for the single-agent version of this logic. Examples and applications are also discussed: to software verification and design (the set of agents can also be seen as a set of actions), and to dynamic epistemic logic. We further give detailed results on the complexity of satisfiability, and on succinctness.