Hans van Ditmarsch

TARK Conference 2025 Conference Paper

Modal Logic for Simulation, Refinement, and Mutual Ignorance

• Hans van Ditmarsch
• Tim French 0002
• Rustam Galimullin
• Louwe B. Kuijer

Simulation and refinement are variations of the bisimulation relation, where in the former we keep only atoms and forth, and in the latter only atoms and back. Quantifying over simulations and refinements captures the effects of information change in a multi-agent system. In the case of quantification over refinements, we are looking at all the ways the agents in a system can become more informed. Similarly, in the case of quantification over simulations, we are dealing with all the ways the agents can become less informed, or in other words, could have been less informed, as we are at liberty how to interpret time in dynamic epistemic logic. While quantification over refinements has been well explored in the literature, quantification over simulations has received considerably less attention. In this paper, we explore the relationship between refinements and simulations. To this end, we also employ the notion of mutual factual ignorance that allows us to capture the state of a model before agents have learnt any factual information. In particular, we consider the extensions of multi-modal logic with the simulation and refinement modalities, as well as modalities for mutual factual ignorance. We provide reduction-based axiomatizations for several of the resulting logics that are built extending one another in a modular fashion.

TARK Conference 2025 Conference Paper

Muddy Waters

• Hans van Ditmarsch

In the 2013 Advent calender of the Berlin Mathematics Research Center MATH+, Gerhard Woeginger presents a novel hat problem with an uncommon initial announcement. Although the information given is insufficient for the hat bearers to learn their colour, they are informed that the colours have been chosen so that they can learn their colour. We formalize this announcement in public announcement logic and in an extension of public announcement logic with fixpoints.

JAIR Journal 2024 Journal Article

Boolean Observation Games

• 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.

LORI Conference 2023 Conference Paper

An Arrow-Based Dynamic Logic of Normative Systems and Its Decidability

• Hans van Ditmarsch
• Louwe B. Kuijer
• Mo Liu 0002

Abstract Normative arrow update logic (NAUL) is a logic that combines normative temporal logic (NTL) and arrow update logic (AUL). In NAUL, norms are interpreted as arrow updates on labeled transition systems with a CTL-like logic. We show that the satisfiability problem of NAUL is decidable with a tableau method and it is in EXPSPACE.

TARK Conference 2023 Conference Paper

Comparing the Update Expressivity of Communication Patterns and Action Models

• Armando Castañeda
• Hans van Ditmarsch
• David A. Rosenblueth
• Diego A. Velázquez

Any kind of dynamics in dynamic epistemic logic can be represented as an action model. Right? Wrong! In this contribution we prove that the update expressivity of communication patterns is incomparable to that of action models. Action models, as update mechanisms, were proposed by Baltag, Moss, and Solecki in 1998 and have remained the nearly universally accepted update mechanism in dynamic epistemic logics since then. Alternatives, such as arrow updates that were proposed by Kooi and Renne in 2011, have update equivalent action models. More recently, the picture is shifting. Communication patterns are update mechanisms originally proposed in some form or other by Agotnes and Wang in 2017 (as resolving distributed knowledge), by Baltag and Smets in 2020 (as reading events), and by Velazquez, Castaneda, and Rosenblueth in 2021 (as communication patterns). All these logics have the same expressivity as the base logic of distributed knowledge. However, their update expressivity, the relation between pointed epistemic models induced by such an update, was conjectured to be different from that of action model logic. Indeed, we show that action model logic and communication pattern logic are incomparable in update expressivity. We also show that, given a history-based semantics and when restricted to (static) interpreted systems, action model logic is (strictly) more update expressive than communication pattern logic. Our results are relevant for distributed computing wherein oblivious models involve arbitrary iteration of communication patterns.

GandALF Workshop 2023 Workshop Paper

On Two- and Three-valued Semantics for Impure Simplicial Complexes

• Hans van Ditmarsch
• Roman Kuznets
• Rojo Randrianomentsoa

Simplicial complexes are a convenient semantic primitive to reason about processes (agents) communicating with each other in synchronous and asynchronous computation. Impure simplicial complexes distinguish active processes from crashed ones, in other words, agents that are alive from agents that are dead. In order to rule out that dead agents reason about themselves and about other agents, three-valued epistemic semantics have been proposed where, in addition to the usual values true and false, the third value stands for undefined: the knowledge of dead agents is undefined and so are the propositional variables describing their local state. Other semantics for impure complexes are two-valued where a dead agent knows everything. Different choices in designing a semantics produce different three-valued semantics, and also different two-valued semantics. In this work, we categorize the available choices by discounting the bad ones, identifying the equivalent ones, and connecting the non-equivalent ones via a translation. The main result of the paper is identifying the main relevant distinction to be the number of truth values and bridging this difference by means of a novel embedding from three- into two-valued semantics. This translation also enables us to highlight quite fundamental modeling differences underpinning various two- and three-valued approaches in this area of combinatorial topology. In particular, pure complexes can be defined as those invariant under the translation.

I&C Journal 2023 Journal Article

To be announced

• 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.

TARK Conference 2021 Conference Paper

No Finite Model Property for Logics of Quantified Announcements

• Hans van Ditmarsch
• Tim French 0002
• Rustam Galimullin

Quantification over public announcements shifts the perspective from reasoning strictly about the results of a particular announcement to reasoning about the existence of an announcement that achieves some certain epistemic goal. Depending on the type of the quantification, we get different formalisms, the most known of which are arbitrary public announcement logic (APAL), group announcement logic (GAL), and coalition announcement logic (CAL). It has been an open question whether the logics have the finite model property, and in the paper we answer the question negatively. We also discuss how this result is connected to other open questions in the field.

I&C Journal 2020 Journal Article

Arrow update synthesis

• Hans van Ditmarsch
• Wiebe van der Hoek
• Barteld Kooi
• Louwe B. Kuijer

In this contribution we present arbitrary arrow update model logic (AAUML). This is a dynamic epistemic logic or update logic. In update logics, static/basic modalities are interpreted on a given relational model whereas dynamic/update modalities induce transformations (updates) of relational models. In AAUML the update modalities formalize the execution of arrow update models, and there is also a modality for quantification over arrow update models. Arrow update models are an alternative to the well-known action models. We provide an axiomatization of AAUML. The axiomatization is a rewrite system allowing to eliminate arrow update modalities from any given formula, while preserving truth. Thus, AAUML is decidable and equally expressive as the base multi-agent modal logic. Our main result is to establish arrow update synthesis: if there is an arrow update model after which φ, we can construct (synthesize) that model from φ. We also point out some pregnant differences in update expressivity between arrow update logics, action model logics, and refinement modal logic.

ECAI Conference 2020 Conference Paper

From Public Announcements to Asynchronous Announcements

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

We present a multi-agent logic of belief and announcements wherein the sending of announcements and the reception of announcements by agents are separated, thus straying from the paradigm of Public Announcement Logic (PAL). Both PAL and Asynchronous Announcement Logic (recently proposed in the literature) are special cases in our framework. We provide a history-based semantics for our ‘Partially Synchronous Announcement Logic’, proposing three different interpretations of the notion of asynchronicity. We then show that the logic of our three proposals is the same (‘PSAL’) and prove soundness and completeness for a Hilbert-style axiomatisation. Finally, we propose a notion of common belief for this framework, of which we give some validities.

AIJ Journal 2020 Journal Article

The logic of gossiping

• Hans van Ditmarsch
• Wiebe van der Hoek
• Louwe B. Kuijer

The so-called gossip problem is a formal model of peer-to-peer communication. In order to perform such communication efficiently, it is important to keep track of what agents know about who holds what information at a given point in time. The knowledge that the agents possess depends strongly on the particular type of communication that is used. Here, we formally define a large number of different variants of the gossip problem, that differ in the extent to which communication is private (observable, synchronous or asynchronous), the direction of the flow of information (caller to callee, callee to caller or both) and whether the agents become aware of the exact set of information possessed by their communication partner. We consider a number of formulas that represent interesting properties that a gossip situation may or may not enjoy, and show for which variants they are valid. Additionally, we show that the model checking and validity checking problems for each variant are decidable, and we introduce sound and complete proof systems for them.

AIJ Journal 2019 Journal Article

Forgetting in multi-agent modal logics

• Liangda Fang
• Yongmei Liu
• Hans van Ditmarsch

In the past decades, forgetting has been investigated for many logics and has found many applications in knowledge representation and reasoning. In this paper, we study forgetting in multi-agent modal logics. We adopt the semantic definition of existential bisimulation quantifiers as that of forgetting. We resort to canonical formulas of modal logics introduced by Moss. An arbitrary modal formula is equivalent to the disjunction of a unique set of satisfiable canonical formulas. We show that, for the logics of K n, D n, T n, K 45 n, KD 45 n and S 5 n, the result of forgetting an atom from a satisfiable canonical formula can be computed by simply substituting the literals of the atom with ⊤. Thus we show that these logics are closed under forgetting, and hence have uniform interpolation. Finally, we generalize the above results to include common knowledge of propositional formulas.

AAMAS Conference 2019 Conference Paper

Groups Versus Coalitions: On the Relative Expressivity of GAL and CAL

• Tim French
• Rustam Galimullin
• Hans van Ditmarsch
• Natasha Alechina

Group Announcement Logic (GAL) and Coalition Announcement Logic (CAL) were proposed to study effects of public announcements by groups of agents on knowledge in multiagent systems. Both logics have operators that quantify over such announcements. In GAL, it is possible to express that ‘a group of agents G has a (truthful) announcement such that after this announcement, some property A holds’; for example, A may involve some agents in G gaining additional knowledge, while agents outside G remain ignorant. In CAL, the meaning of the coalition announcement operator is subtly different: it says that ‘G has an announcement such that, whatever else the agents outside G announce simultaneously, some property A is guaranteed to hold after the joint announcement’. It has been open for some time whether GAL and CAL are equally expressive. We show that this is not the case: there is a property expressible in GAL that is not expressible in CAL. It is still an open question whether CAL is subsumed by GAL, or whether the two logics have incomparable expressive power.

FLAP Journal 2019 Journal Article

Strengthening Gossip Protocols using Protocol-Dependent Knowledge.

• Hans van Ditmarsch
• Malvin Gattinger
• Louwe B. Kuijer
• Pere Pardo

Distributed dynamic gossip is a generalization of the classic telephone problem in which agents communicate to share secrets, with the additional twist that also telephone numbers are exchanged to determine who can call whom. Recent work focused on the success conditions of simple protocols such as “Learn New Secrets” (LNS) wherein an agent a may only call another agent b if a does not know b’s secret. A protocol execution is successful if all agents get to know all secrets. On partial networks these protocols sometimes fail because they ignore information available to the agents that would allow for better coordination. We study how epistemic protocols for dynamic gossip can be strengthened, using epistemic logic as a simple protocol language with a new operator for protocol-dependent knowledge. We provide definitions of different strengthenings and show that they perform better than LNS, but we also prove that there is no strengthening of LNS that always terminates successfully. Together, this gives us a better picture of when and how epistemic coordination can help in the dynamic gossip problem in particular and distributed systems in general.

AIJ Journal 2018 Journal Article

Implicit, explicit and speculative knowledge

• Hans van Ditmarsch
• Tim French
• Fernando R. Velázquez-Quesada
• Yì N. Wáng

We compare different epistemic notions in the presence of awareness of propositional variables: the logic of implicit knowledge (in which explicit knowledge is definable), the logic of explicit knowledge, and the logic of speculative knowledge. Speculative knowledge is a novel epistemic notion that permits reasoning about unawareness. These logics are interpreted on epistemic awareness models: these are multi-agent Kripke structures for propositional awareness (in each state an agent may only be aware of formulas containing occurrences of a subset of all propositional variables). Different notions of bisimulation are suitable for these logics. We provide correspondence between bisimulation and modal equivalence on image-finite models for these logics. Expressivity and axiomatizations are investigated for models without restrictions, and for models with equivalence relations for all agents (modeling knowledge) and awareness introspection (agents know what they are aware of). We show that the logic of speculative knowledge is as expressive as the logic of explicit knowledge, and the logic of implicit knowledge is more expressive than the two other logics. We also present expressivity results for more restricted languages. We then provide and compare axiomatizations for the three logics; the axiomatizations for speculative knowledge are novel. We compare our results to those for awareness achieved in artificial intelligence, computer science, philosophy, and economics.

TARK Conference 2017 Conference Paper

A Logic for Global and Local Announcements

• 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 -- $[\phi]^+_A$ and $[\phi]^-_A$ indexed to a subset $A$ of the set $Ag$ of all agents -- for global and local announcements respectively. The boundary case $[\phi]^+_{Ag}$ corresponds to the public announcement of $\phi$, 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.

AIJ Journal 2017 Journal Article

Arbitrary arrow update logic

• Hans van Ditmarsch
• Wiebe van der Hoek
• Barteld Kooi
• Louwe B. Kuijer

In this paper we introduce arbitrary arrow update logic (AAUL). The logic AAUL takes arrow update logic, a dynamic epistemic logic where the accessibility relations of agents are updated rather than the set of possible worlds, and adds a quantifier over such arrow updates. We investigate the relative expressivity of AAUL compared to other logics, most notably arbitrary public announcement logic (APAL). Additionally, we show that the model checking problem for AAUL is PSPACE-complete. Finally, we introduce a proof system for AAUL, and prove it to be sound and complete.

TARK Conference 2017 Conference Paper

Cheryl's Birthday

• Hans van Ditmarsch
• Michael Ian Hartley
• Barteld Kooi
• Jonathan Welton
• Joseph B. W. Yeo

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.

LORI Conference 2017 Conference Paper

Strategic Knowledge of the Past in Quantum Cryptography

• Christophe Chareton
• Hans van Ditmarsch

Abstract We propose an epistemic strategy logic with future and past time operators, called \(\text {SLKP}\), for Strategy Logic with Knowledge of the Past. With \(\text {SLKP}\) we can model mutually observed moves/actions in strategic contexts. In a semantic game, agents may completely or partially observe other agents’ moves, their moves may depend on their knowledge of other players’ strategies, and their knowledge may depend on the history of their own or other’s moves. The logic \(\text {SLKP}\) also allows us to describe temporal properties involving past, future, and composed tenses such as future perfect or counterfactual assertions. We illustrate SLKP by formalising the quantum cryptography protocol BB84, with the purpose to initiate an integrated epistemic and strategic treatment of agent interactions in quantum systems.

EUMAS Conference 2017 Conference Paper

The Expected Duration of Sequential Gossiping

• Hans van Ditmarsch
• Ioannis Kokkinis

Abstract A gossip protocol aims at arriving, by means of point-to-point communications (or telephone calls), at a situation in which every agent knows all the information initially present in the network. If it is forbidden to have more than one call at the same time, the protocol is called sequential. We generalise a method, that originates from the famous coupon collector’s problem and that was proposed by John Haigh in 1981, for bounding the expected duration of sequential gossip protocols. We give two examples of protocols where this method succeeds and two examples of protocols where this method fails to give useful bounds. Our main contribution is that, although Haigh originally applied this method in a protocol where any call is available at any moment, we show that this method can be applied in protocols where the number of available calls is decreasing. Furthermore, for one of the protocols where Haigh’s method fails we were able to obtain lower bounds for the expectation using results from random graph theory.

I&C Journal 2017 Journal Article

The modal logic of copy and remove

• Carlos Areces
• Hans van Ditmarsch
• Raul Fervari
• François Schwarzentruber

We propose a logic with the dynamic modal operators copy and remove. The copy operator replicates a given model, and the remove operator removes paths in a given model. We show that the product update by an action model in dynamic epistemic logic decomposes in copy and remove operations, when we consider action models with Boolean pre-conditions and no post-condition. We also show that copy and remove operators with paths of length 1 can be expressed by action models with post-conditions. We investigate the expressive power of the logic with copy and remove operations, together with the complexity of the satisfiability problem of some of its syntactic fragments.

TCS Journal 2017 Journal Article

The undecidability of arbitrary arrow update logic

• Hans van Ditmarsch
• Wiebe van der Hoek
• Louwe B. Kuijer

Arbitrary Arrow Update Logic is a dynamic modal logic with a modality to quantify over arrow updates. Some properties of this logic have already been established, but until now it remained an open question whether the logic's satisfiability problem is decidable. Here, we show by a reduction of the tiling problem that the satisfiability problem of Arbitrary Arrow Update Logic is co-RE hard, and therefore undecidable.

IJCAI Conference 2016 Conference Paper

Forgetting in Multi-Agent Modal Logics

• Liangda Fang
• Yongmei Liu
• Hans van Ditmarsch

In the past decades, forgetting has been investigated for many logics and has found many applications in knowledge representation and reasoning. However, forgetting in multi-agent modal logics has largely been unexplored. In this paper, we study forgetting in multi-agent modal logics. We adopt the semantic definition of existential bisimulation quantifiers as that of forgetting. We propose a syntactical way of performing forgetting based on the canonical formulas of modal logics introduced by Moss. We show that the result of forgetting a propositional atom from a satisfiable canonical formula can be computed by simply substituting the literals of the atom with T. Thus we show that Kn, Dn, Tn, K45n, KD45n and S5n are closed under forgetting, and hence have uniform interpolation.

AAMAS Conference 2016 Conference Paper

Second-order Propositional Announcement Logic

• Francesco Belardinelli
• Hans van Ditmarsch
• Wiebe van der Hoek

TARK Conference 2015 Conference Paper

Announcement as effort on topological spaces

• Hans van Ditmarsch
• Sophia Knight
• Aybüke Özgün

We propose a multi-agent logic of knowledge, public and arbitrary announcements, that is interpreted on topological spaces in the style of subset space semantics. The arbitrary announcement modality functions similarly to the effort modality in subset space logics, however, it comes with intuitive and semantic differences. We provide axiomatizations for three logics based on this setting, and demonstrate their completeness.

TCS Journal 2015 Journal Article

The complexity of one-agent refinement modal logic

• Laura Bozzelli
• Hans van Ditmarsch
• Sophie Pinchinat

We investigate the complexity of satisfiability for one-agent refinement modal logic (RML), a known extension of basic modal logic (ML) obtained by adding refinement quantifiers on structures. It is known that RML has the same expressiveness as ML, but the translation of RML into ML is of non-elementary complexity, and RML is at least doubly exponentially more succinct than ML. In this paper, we show that RML-satisfiability is ‘only’ singly exponentially harder than ML-satisfiability, the latter being a well-known PSPACE-complete problem. More precisely, we establish that RML-satisfiability is complete for the complexity class AEXP pol, i. e. , the class of problems solvable by alternating Turing machines running in single exponential time but only with a polynomial number of alternations (note that NEXPTIME ⊆ AEXP pol ⊆ EXPSPACE ). 1 1 This work is the revised and expanded version of [1].

EUMAS Conference 2014 Conference Paper

A Framework for Epistemic Gossip Protocols

• Maduka Attamah
• Hans van Ditmarsch
• Davide Grossi
• Wiebe van der Hoek

Abstract We implement a framework to evaluate epistemic gossip protocols. Gossip protocols spread information within a network of agents by pairwise communications. This tool, Epistemic Gossip Protocol (EGP), is applied to epistemic gossip protocols presented in [ 1 ]. We introduce a programming language for epistemic gossip protocols. We describe an interpreter for this language, together with a model generator and model checker, for a dynamic model of the protocol. The tool EGP outputs key dynamic properties of such protocols, thus facilitating the process of protocol design and planning. We conclude with some experimental results.

EUMAS Conference 2014 Conference Paper

Arbitrary Announcements on Topological Subset Spaces

• Hans van Ditmarsch
• Sophia Knight
• Aybüke Özgün

Abstract Subset space semantics for public announcement logic in the spirit of the effort modality have been proposed by Wang and Ågotnes [ 18 ] and by Bjorndahl [ 6 ]. They propose to model the public announcement modality by shrinking the epistemic range with respect to which a postcondition of the announcement is evaluated, instead of by restricting the model to the set of worlds satisfying the announcement. Thus we get an “elegant, model-internal mechanism for interpreting public announcements” [ 6, p. 12]. In this work, we extend Bjorndahl’s logic \(PAL_{int}\) of public announcement, which is modelled on topological spaces using subset space semantics and adding the interior operator, with an arbitrary announcement modality, and we provide topological subset space semantics for the corresponding arbitrary announcement logic \(APAL_{int}\), and demonstrate completeness of the logic by proving that it is equal in expressivity to the logic without arbitrary announcements, employing techniques from [ 2, 13 ].

AIJ Journal 2014 Journal Article

Hidden protocols: Modifying our expectations in an evolving world

• Hans van Ditmarsch
• Sujata Ghosh
• Rineke Verbrugge
• Yanjing Wang

When agents know a protocol, this leads them to have expectations about future observations. Agents can update their knowledge by matching their actual observations with the expected ones. They eliminate states where they do not match. In this paper, we study how agents perceive protocols that are not commonly known, and propose a semantics-driven logical framework to reason about knowledge in such scenarios. In particular, we introduce the notion of epistemic expectation models and a propositional dynamic logic-style epistemic logic for reasoning about knowledge via matching agentsʼ expectations to their observations. It is shown how epistemic expectation models can be obtained from epistemic protocols. Furthermore, a characterization is presented of the effective equivalence of epistemic protocols. We introduce a new logic that incorporates updates of protocols and that can model reasoning about knowledge and observations. Finally, the framework is extended to incorporate fact-changing actions, and a worked-out example is given.

ECAI Conference 2014 Conference Paper

Knowledge and Gossip

• Maduka Attamah
• Hans van Ditmarsch
• Davide Grossi
• Wiebe van der Hoek

A well-studied phenomenon in network theory are optimal schedules to distribute information by one-to-one communication between nodes. One can take these communicative actions to be 'telephone calls', and this process of spreading information is known as gossiping [4]. It is typical to assume a global scheduler who simply executes a possibly non-deterministic protocol. Such a protocol can be seen as consisting of a sequence of instructions "first, agent a calls b, then c, next, d calls b. .. ". We investigate epistemic gossip protocols, where an agent a will call another agent not because it is so instructed but based on its knowledge or ignorance of the factual information that is distributed over the network. Such protocols therefore don't need a central schedular, but they come at a cost: they may take longer to terminate than non-epistemic, globally scheduled, protocols. We describe various epistemic protocols, we give their logical properties, and we model them in a number of ways.

I&C Journal 2014 Journal Article

Refinement modal logic

• Laura Bozzelli
• Hans van Ditmarsch
• Tim French
• James Hales
• Sophie Pinchinat

In this paper we present 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 ∀ in addition to the standard box modalities for each agent. The operator ∀ 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 ∀ 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 μ-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.

TCS Journal 2013 Journal Article

A colouring protocol for the generalized Russian cards problem

• Andrés Cordón-Franco
• Hans van Ditmarsch
• David Fernández-Duque
• Fernando Soler-Toscano

In the generalized Russian cards problem, Alice, Bob and Cath draw a, b and c cards, respectively, from a deck of size a + b + c. Alice and Bob must then communicate their entire hand to each other, without Cath learning the owner of a single card she does not hold. Unlike many traditional problems in cryptography, however, they are not allowed to encode or hide the messages they exchange from Cath. The problem is then to find methods through which they can achieve this. We propose a general four-step solution based on finite vector spaces, and call it the “colouring protocol”, as it involves colourings of lines. Our main results show that the colouring protocol may be used to solve the generalized Russian cards problem in cases where a is a power of a prime, c = O ( a 2 ) and b = O ( c 2 ). This improves substantially on the set of parameters for which solutions are known to exist; in particular, it had not been shown previously that the problem could be solved in cases where the eavesdropper has more cards than one of the communicating players.

TARK Conference 2013 Conference Paper

Knowledge, awareness, and bisimulation

• Hans van Ditmarsch
• Tim French 0002
• Fernando R. Velázquez-Quesada
• Yì N. Wáng

intuitive situations. Consider the following models. We compare different epistemic notions in the presence of awareness of propositional variables: the logics of implicit knowledge (in which explicit knowledge is definable), explicit knowledge, and speculative knowledge. Different notions of bisimulation are suitable for these logics. We provide correspondence between bisimulation and modal equivalence on image-finite models for these logics. The logic of speculative knowledge is equally expressive as the logic of explicit knowledge, and the logic of implicit knowledge is more expressive than both. We also provide axiomatizations for the three logics — only the one for speculative knowledge is novel. Then we move to the study of dynamics by recalling action models incorporating awareness. We show that any conceivable change of knowledge or awareness can be modelled in this setting, we give a complete axiomatization for the dynamic logic of implicit knowledge. The dynamic versions of all three logics are, surprising, equally expressive. ◦ s ◦ t ◦ u M0: ◦ s ◦ t • u Model M has a domain {s, t, u}, a single agent i with accessibility relation R = {(s, t), (t, u)}, atom p true in all states, and the agent is aware of p only in state s. Awareness is not depicted. Model M 0 is like M, except that p is now false in u (the black dot). As mentioned, the agent knows explicitly a given ϕ at a given state iff she is aware of the formula in that state and ϕ is true in all accessible states. Let us apply this to the depicted structures. In both, the agent is unaware of p at state t, and therefore of the value of p in u: she should see (M, t) and (M 0, t) as identical, and therefore (M, s) and (M 0, s) as well. We propose a notion of bisimilarity for which (M, s) and (M 0, s) are bisimilar. Now here is the surprise: in the language with awareness and modal box, states (M, s) and (M 0, s) are not modally equivalent. Given explicit knowledge KiE ϕ as 2i ϕ ∧ Ai ϕ, consider KiE 2i p. This is true in (M, s) but false in (M 0, s). In logics of awareness [4] it is common only to consider models for knowledge (equivalence relations) and belief. However, as always in multi-agent logics, it is elementary to transform a single-agent model with directed (asymmetric) accessibility into a multi-agent model where intersecting equivalence classes for agents force such asymmetry. For example, consider the following.

LORI Conference 2013 Conference Paper

Listen to Me! Public Announcements to Agents That Pay Attention - or Not

• Hans van Ditmarsch
• Andreas Herzig
• Emiliano Lorini
• François Schwarzentruber

Abstract In public announcement logic it is assumed that all agents pay attention (listen to/observe) to the announcement. Weaker observational conditions can be modelled in event (action) model logic. In this work, we propose a version of public announcement logic wherein it is encoded in the states of the epistemic model which agents pay attention to the announcement. This logic is called attention-based announcement logic, abbreviated ABAL. We give an axiomatization and prove that complexity of satisfiability is the same as that of public announcement logic, and therefore lower than that of action model logic [2]. We exploit our logic to formalize the concept of joint attention that has been widely discussed in the philosophical and cognitive science literature. Finally, we extend our logic by integrating attention change.

TARK Conference 2013 Conference Paper

Strategic voting and the logic of knowledge

• Hans van Ditmarsch
• Jérôme Lang
• Abdallah Saffidine

We propose a general framework for strategic voting when a voter may lack knowledge about other votes or about other voters’ knowledge about her own vote. In this setting we define notions of manipulation and equilibrium. We also model action changing knowledge about votes, such as a voter revealing its preference or as a central authority performing a voting poll. Some forms of manipulation are preserved under such updates and others not. Another form of knowledge dynamics is the effect of a voter declaring its vote. We envisage Stackelberg games for uncertain profiles. The purpose of this investigation is to provide the epistemic background for the analysis and design of voting rules that incorporate uncertainty.

IJCAI Conference 2013 Conference Paper

The Complexity of One-Agent Refinement Modal Logic

• Laura Bozzelli
• Hans van Ditmarsch
• Sophie Pinchinat

We investigate the complexity of satisfiability for one-agent refinement modal logic (RML), an extension of basic modal logic (ML) obtained by adding refinement quantifiers on structures. RML is known to have the same expressiveness as ML, but the translation of RML into ML is of non-elementary complexity, and RML is at least doubly exponentially more succinct than ML. In this paper we show that RML-satisfiability is ‘only’ singly exponentially harder than ML-satisfiability, the latter being a well-known PSPACE-complete problem.

AAMAS Conference 2012 Conference Paper

Action models for knowledge and awareness

• Hans van Ditmarsch
• Tim French
• Fernando R. Vel
• aacute; zquez-Quesada

We consider semantic structures and logics that differentiate between being uncertain about a proposition, being unaware of a proposition, becoming aware of a proposition and getting to know the truth value of a proposition. In this paper we give a unified setting to model all this variety of static and dynamic aspects of awareness and knowledge, without any constraints on the modal properties of knowledge (or belief -- such as introspection) or on the interaction between awareness and knowledge (such as awareness introspection). Our primitive epistemic operator is called \emph{speculative knowledge}. This is different from the better known \emph{implicit knowledge}, now definable, which plays a more restricted role. Some dynamic semantic primitives that are elegantly definable in our setting are the actions of 'becoming aware of a propositional variable', 'implicit knowledge', 'adressing a novel issue in an announcement', and also more complex ways in which an agent can become aware of a novel issue by way of increasing the complexity of the epistemic model.

AIJ Journal 2012 Journal Article

Local properties in modal logic

• Hans van Ditmarsch
• Wiebe van der Hoek
• Barteld Kooi

In modal logic, when adding a syntactic property to an axiomatisation, this property will semantically become true in all models, in all situations, under all circumstances. For instance, adding a property like K a p → K b p (agent b knows at least what agent a knows) to an axiomatisation of some epistemic logic has as an effect that such a property becomes globally true, i. e. , it will hold in all states, at all time points (in a temporal setting), after every action (in a dynamic setting) and after any communication (in an update setting), and every agent will know that it holds, it will even be common knowledge. We propose a way to express that a property like the above only needs to hold locally: it may hold in the actual state, but not in all states, and not all agents may know that it holds. We achieve this by adding relational atoms to the language that represent (implicitly) quantification over all formulas, as in ∀ p ( K a p → K b p ). We show how this can be done for a rich class of modal logics and a variety of syntactic properties. We then study the epistemic logic enriched with the syntactic property ‘knowing at least as much as’ in more detail. We show that the enriched language is not preserved under bisimulations. We also demonstrate that adding public announcements to this enriched epistemic logic makes it more expressive, which is for instance not true for the ‘standard’ epistemic logic S5.

AAMAS Conference 2012 Conference Paper

Strategic voting and the logic of knowledge

• Hans van Ditmarsch
• J
• eacute; r
• ocirc; me Lang
• Abdallah Saffidine

JELIA Conference 2012 Conference Paper

The Complexity of One-Agent Refinement Modal Logic

• Laura Bozzelli
• Hans van Ditmarsch
• Sophie Pinchinat

Abstract We investigate the complexity of satisfiability for one-agent Refinement Modal Logic ( \(\text{\sffamily RML}\) ), a known extension of basic modal logic ( \(\text{\sffamily ML}\) ) obtained by adding refinement quantifiers on structures. It is known that \(\text{\sffamily RML}\) has the same expressiveness as \(\text{\sffamily ML}\), but the translation of \(\text{\sffamily RML}\) into \(\text{\sffamily ML}\) is of non-elementary complexity, and \(\text{\sffamily RML}\) is at least doubly exponentially more succinct than \(\text{\sffamily ML}\). In this paper, we show that \(\text{\sffamily RML}\) -satisfiability is ‘only’ singly exponentially harder than \(\text{\sffamily ML}\) -satisfiability, the latter being a well-known PSPACE -complete problem. More precisely, we establish that \(\text{\sffamily RML}\) -satisfiability is complete for the complexity class AEXP \(_{\text{\sffamily pol}}\), i. e. , the class of problems solvable by alternating Turing machines running in single exponential time but only with a polynomial number of alternations (note that NEXPTIME ⊆ AEXP \(_{\text{\sffamily pol}}\) ⊆ EXPSPACE ).

TARK Conference 2011 Conference Paper

Hidden protocols

• Hans van Ditmarsch
• Sujata Ghosh
• Rineke Verbrugge
• Yanjing Wang 0001

When agents know a protocol, this leads them to have expectations about future observations. Agents can update their knowledge by matching their actual observations with the expected ones. They eliminate states where they do not match. In this paper, we study how agents perceive protocols that are not commonly known, and propose a logic to reason about knowledge in such scenarios.

AAMAS Conference 2011 Conference Paper

Reasoning About Local Properties in Modal Logic

• Hans van Ditmarsch
• Wiebe van der Hoek
• Barteld Kooi

In modal logic, when adding a syntactic property to an axiomatisation, this property will semantically become true in all models, in all situations, under all circumstances. For instance, adding a property like K_a p → K_b p (agent b knows at least what agent a knows) to an axiomatisation of some epistemic logic has as an effect that such a property becomes globally true, i. e. , it will hold in all states, at all time points (in a temporal setting), after every action (in a dynamic setting) and after any communication (in an update setting), and every agent will know that it holds, it will even be common knowledge. We propose a way to express that a property like the above only needs to hold locally: it may hold in the actual state, but not in all states, and not all agents may know that it holds. We can achieve this by adding relational atoms to the language that represent (implicitly) quantification over all formulas, as in ∀ p (K_a p → K_b p). We show how this can be done for a rich class of modal logics and a variety of syntactic properties.

ECAI Conference 2010 Conference Paper

A Logical Model of Intention and Plan Dynamics

• Emiliano Lorini
• Hans van Ditmarsch
• Tiago de Lima

We propose a formal semantics of intention and plan dynamics based on the notion of local assignment. The function of a local assignment is to change the truth value of a given proposition at a specific time point along a history. We combine a static modal logic including a temporal modality and modal operators for mental attitudes belief and choice, with three kinds of dynamic modalities and corresponding three kinds of local assignments operating on agent's beliefs, on agent's choices and on the physical world. An agent's intention is defined in our approach as the agent's choice to perform a given action at a certain time point in the future and two operations called intention generation and intention reconsideration are defined as specific kinds of local assignments on choices. In Section 1 we introduce a static logic of time, action, and mental attitudes. In Section 2 we add the dynamic notion of local assignment to the logic of Section 1. In Section 3, we focus on two specific kinds of local assignment on choice which allow to model the processes of intention and plan generation and reconsideration.

KR Conference 2010 Conference Paper

One hundred prisoners and a lightbulb - logic and computation

• Hans van Ditmarsch
• Jan van Eijck
• William Wu

is the only way in which they can communicate). The light This is a case-study in knowledge representation. We analyze the ‘one hundred prisoners and a lightbulb’ puzzle. In this puzzle it is relevant what the agents (prisoners) know, how their knowledge changes due to observations, and how they affect the state of the world by changing facts, i. e., by their actions. These actions depend on the history of previous actions and observations. Part of its interest is that all actions are local, i. e. not publicly observable, and part of the problem is therefore how to disseminate local results to other agents, and make them global. The various solutions to the puzzle are presented as protocols (iterated functions from agent’s local states, and histories of actions, to actions). The computational aspect is about average runtime termination under conditions of random (‘fair’) scheduling. The paper consists of three parts. First, we present different versions of the puzzle, and their solution. This includes a probabilistic version, and a version assuming synchronicity (the interval between prisoners’ interrogations is known). The latter is very informative for the prisoners, and allows different protocols (with faster expected termination). Then, we model the puzzle in an epistemic logic incorporating dynamic operators for the effects of information changing events. Such events include both informative actions, where agents become more informed about the non-changing state of the world, and factual changes, wherein the world and the facts describing it change themselves as well. Finally, we give the expected termination results of several protocols when assuming random scheduling. This paper integrates the literature and presents novel contributions. Novel are: Firstly, Protocol 2 and Protocol 4. Secondly, the modelling in dynamic epistemic logic in its entirety — we do not know of a case study that combines factual and informational dynamics in a setting of non-public events, or of a similar proposal to handle asynchronous behaviour in a dynamic epistemic logic. Thirdly, our computational results on Protocol 2 and results from manuscript (Wu 2002).

IJCAI Conference 2009 Conference Paper

• Hans van Ditmarsch
• Wiebe van der Hoek
• Barteld Kooi

Modal correspondence theory is a powerful and effective way to guarantee that adding specific syntactic axioms to a modal logic is mirrored by requiring ‘corresponding’ properties of the underlying Kripke models. However, such axioms not only quantify over all formulas, but they are also global in the sense that the corresponding semantic property is assumed to hold for all states. However, in for instance epistemic logic one would like to have the flexibility to say that certain properties (like ‘agent b knows at least what agent a knows’) are true locally in a specific state, but not necessarily globally, in all states. This would enable one to say ‘currently, b knows at least what a knows, but this is not common knowledge’, or ‘. .. but this is not always true’, or ‘. .. but this could be changed by action α’. We offer a logic for ‘knowing at least as’, where the (global) axiom scheme Kaϕ → Kbϕ is replaced by a (local) inference rule. We give a complete modal system, and discuss some consequences of the axiom in an epistemic setting. Our completeness proof also suggests how achieving such local properties can be generalized to other axioms schemes and modal logics.

LORI Conference 2009 Conference Paper

Intentions and Assignments

• Emiliano Lorini
• Mehdi Dastani
• Hans van Ditmarsch
• Andreas Herzig
• John-Jules Ch. Meyer

Abstract The aim of this work is propose a logical approach to intention dynamics based on the notion of assignment [3, 7]. The function of an assignment is to associate the truth value of a certain formula ϕ to a propositional atom p. We combine a static modal logic of belief and choice with three kinds of dynamic modalities and corresponding three kinds of assignments: assignments operating on an agent’s beliefs, assignments operating on the agent’s choices and assignments operating on the objective world. An agent’s intention is defined in our approach as the agent’s choice to perform a given action and two basic operations on intentions called intention generation and intention reconsideration are defined as specific kinds of assignments on choices.

AAMAS Conference 2008 Conference Paper

Coalitions and Announcements

• Thomas Agotnes
• Hans van Ditmarsch

Two currently active strands of research on logics for multi-agent systems are dynamic epistemic logic, focusing on the epistemic consequences of actions, and logics of coalitional ability, focusing on what coalitions of agents can achieve by cooperating strategically. In this paper we make a first attempt to bridge these topics by considering the question: “what can a coalition achieve by public announcements? ”. We propose, first, an extension of public announcement logic with constructs of the form hGiϕ, where G is a set of agents, with the intuitive meaning that G can jointly make an announcement such that ϕ will be true afterwards. Second, we consider a setting where all agents can make (truthful) announcements at the same time, and propose a logic with a construct h[G]iϕ, meaning that G can jointly make an announcement such that no matter what the other agents announce, ϕ will be true. The latter logic is closely related to Marc Pauly’s Coalition Logic.

AAAI Conference 2007 Conference Paper

Optimal Regression for Reasoning about Knowledge and Actions

• Hans van Ditmarsch

We show how in the propositional case both Reiter’s and Scherl & Levesque’s solutions to the frame problem can be modelled in dynamic epistemic logic (DEL), and provide an optimal regression algorithm for the latter. Our method is as follows: we extend Reiter’s framework by integrating observation actions and modal operators of knowledge, and encode the resulting formalism in DEL with announcement and assignment operators. By extending Lutz’ recent satisfiability-preserving reduction to our logic, we establish optimal decision procedures for both Reiter’s and Scherl & Levesque’s approaches: satisfiability is NP-complete for one agent, PSPACE-complete for multiple agents and EXPTIMEcomplete when common knowledge is involved.

TARK Conference 2007 Conference Paper

What can we achieve by arbitrary announcements? : A dynamic take on Fitch's knowability

• Philippe Balbiani
• Alexandru Baltag
• Hans van Ditmarsch
• Andreas Herzig
• Tomohiro Hoshi
• Tiago de Lima

Public announcement logic is an extension of multi-agent 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: ϕ expresses that ϕ is true after an arbitrary announcement ψ. As this includes the trivial announcement >, one might as well say that ϕ expresses what remains true after any announcement: it therefore corresponds to truth persistence after (definable) relativisation. The dual operation ♦ϕ expresses that there is an announcement after which ϕ. This gives a perspective on Fitch’s knowability issues: for which formulas ϕ does it hold that ϕ → ♦Kϕ? We give various semantic results, and we show completeness for a Hilbert-style axiomatisation of this logic.