-
Bisimulation for Impure Simplicial Complexes
Authors:
Marta Bílková,
Hans van Ditmarsch,
Roman Kuznets,
Rojo Randrianomentsoa
Abstract:
As an alternative to Kripke models, simplicial complexes are a versatile semantic primitive on which to interpret epistemic logic. Given a set of vertices, a simplicial complex is a downward closed set of subsets, called simplexes, of the vertex set. A maximal simplex is called a facet. Impure simplicial complexes represent that some agents (processes) are dead. It is known that impure simplicial…
▽ More
As an alternative to Kripke models, simplicial complexes are a versatile semantic primitive on which to interpret epistemic logic. Given a set of vertices, a simplicial complex is a downward closed set of subsets, called simplexes, of the vertex set. A maximal simplex is called a facet. Impure simplicial complexes represent that some agents (processes) are dead. It is known that impure simplicial complexes categorically correspond to so-called partial epistemic (Kripke) models. In this contribution, we define a notion of bisimulation to compare impure simplicial complexes and show that it has the Hennessy-Milner property. These results are for a logical language including atoms that express whether agents are alive or dead. Without these atoms no reasonable standard notion of bisimulation exists, as we amply justify by counterexamples, because such a restricted language is insufficiently expressive.
△ Less
Submitted 24 June, 2024;
originally announced June 2024.
-
The Undecidability of Quantified Announcements
Authors:
Thomas Ågotnes,
Hans van Ditmarsch,
Tim French
Abstract:
This paper demonstrates the undecidability of a number of logics with quantification over public announcements: arbitrary public announcement logic (APAL), group announcement logic (GAL), and coalition announcement logic (CAL). In APAL we consider the informative consequences of any announcement, in GAL we consider the informative consequences of a group of agents (this group may be a proper subse…
▽ More
This paper demonstrates the undecidability of a number of logics with quantification over public announcements: arbitrary public announcement logic (APAL), group announcement logic (GAL), and coalition announcement logic (CAL). In APAL we consider the informative consequences of any announcement, in GAL we consider the informative consequences of a group of agents (this group may be a proper subset of the set of all agents) all of which are simultaneously (and publicly) making known announcements. So this is more restrictive than APAL. Finally, CAL is as GAL except that we now quantify over anything the agents not in that group may announce simultaneously as well. The logic CAL therefore has some features of game logic and of ATL. We show that when there are multiple agents in the language, the satisfiability problem is undecidable for APAL, GAL, and CAL. In the single agent case, the satisfiability problem is decidable for all three logics. This paper corrects an error to the submitted version of Undecidability of Quantified Announcements, identified by Yuta Asami . The nature of the error was in the definition of the formula $cga(X)$ (see Subsection 5.2) which is corrected in this version.
△ Less
Submitted 5 June, 2024; v1 submitted 24 May, 2024;
originally announced May 2024.
-
A Logic for Repair and State Recovery in Byzantine Fault-tolerant Multi-agent Systems
Authors:
Hans van Ditmarsch,
Krisztina Fruzsa,
Roman Kuznets,
Ulrich Schmid
Abstract:
We provide an epistemic logical language and semantics for the modeling and analysis of byzantine fault-tolerant multi-agent systems. This not only facilitates reasoning about the agents' fault status but also supports model updates for implementing repair and state recovery. For each agent, besides the standard knowledge modality our logic provides an additional modality called hope, which is cap…
▽ More
We provide an epistemic logical language and semantics for the modeling and analysis of byzantine fault-tolerant multi-agent systems. This not only facilitates reasoning about the agents' fault status but also supports model updates for implementing repair and state recovery. For each agent, besides the standard knowledge modality our logic provides an additional modality called hope, which is capable of expressing that the agent is correct (not faulty), and also dynamic modalities enabling change of the agents' correctness status. These dynamic modalities are interpreted as model updates that come in three flavours: fully public, more private, or involving factual change. We provide complete axiomatizations for all these variants in the form of reduction systems: formulas with dynamic modalities are equivalent to formulas without. Therefore, they have the same expressivity as the logic of knowledge and hope. Multiple examples are provided to demonstrate the utility and flexibility of our logic for modeling a wide range of repair and state recovery techniques that have been implemented in the context of fault-detection, isolation, and recovery (FDIR) approaches in fault-tolerant distributed computing with byzantine agents.
△ Less
Submitted 27 June, 2024; v1 submitted 12 January, 2024;
originally announced January 2024.
-
On Two- and Three-valued Semantics for Impure Simplicial Complexes
Authors:
Hans van Ditmarsch,
Roman Kuznets,
Rojo Randrianomentsoa
Abstract:
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-…
▽ More
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.
△ Less
Submitted 2 October, 2023;
originally announced October 2023.
-
Comparing the Update Expressivity of Communication Patterns and Action Models
Authors:
Armando Castañeda,
Hans van Ditmarsch,
David A. Rosenblueth,
Diego A. Velázquez
Abstract:
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 episte…
▽ More
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.
△ Less
Submitted 11 July, 2023;
originally announced July 2023.
-
Impure Simplicial Complexes: Complete Axiomatization
Authors:
Rojo Randrianomentsoa,
Hans van Ditmarsch,
Roman Kuznets
Abstract:
Combinatorial topology is used in distributed computing to model concurrency and asynchrony. The basic structure in combinatorial topology is the simplicial complex, a collection of subsets called simplices of a set of vertices, closed under containment. Pure simplicial complexes describe message passing in asynchronous systems where all processes (agents) are alive, whereas impure simplicial comp…
▽ More
Combinatorial topology is used in distributed computing to model concurrency and asynchrony. The basic structure in combinatorial topology is the simplicial complex, a collection of subsets called simplices of a set of vertices, closed under containment. Pure simplicial complexes describe message passing in asynchronous systems where all processes (agents) are alive, whereas impure simplicial complexes describe message passing in synchronous systems where processes may be dead (have crashed). Properties of impure simplicial complexes can be described in a three-valued multi-agent epistemic logic where the third value represents formulae that are undefined, e.g., the knowledge and local propositions of dead agents. In this work we present an axiomatization for the logic of the class of impure complexes and show soundness and completeness. The completeness proof involves the novel construction of the canonical simplicial model and requires a careful manipulation of undefined formulae.
△ Less
Submitted 17 October, 2023; v1 submitted 24 November, 2022;
originally announced November 2022.
-
A Labelled Sequent Calculus for Public Announcement Logic
Authors:
Hao Wu,
Hans van Ditmarsch,
**sheng Chen
Abstract:
Public announcement logic(PAL) is an extension of epistemic logic (EL) with some reduction axioms. In this paper, we propose a cut-free labelled sequent calculus for PAL, which is an extension of that for EL with sequent rules adapted from the reduction axioms. This calculus admits cut and allows terminating proof search.
Public announcement logic(PAL) is an extension of epistemic logic (EL) with some reduction axioms. In this paper, we propose a cut-free labelled sequent calculus for PAL, which is an extension of that for EL with sequent rules adapted from the reduction axioms. This calculus admits cut and allows terminating proof search.
△ Less
Submitted 27 October, 2022; v1 submitted 20 July, 2022;
originally announced July 2022.
-
Communication Pattern Logic: Epistemic and Topological Views
Authors:
Armando Castañeda,
Hans van Ditmarsch,
David A. Rosenblueth,
Diego A. Velázquez
Abstract:
We propose communication pattern logic. A communication pattern describes how processes or agents inform each other, independently of the information content. The full-information protocol in distributed computing is the special case wherein all agents inform each other. We study this protocol in distributed computing models where communication might fail: an agent is certain about the messages it…
▽ More
We propose communication pattern logic. A communication pattern describes how processes or agents inform each other, independently of the information content. The full-information protocol in distributed computing is the special case wherein all agents inform each other. We study this protocol in distributed computing models where communication might fail: an agent is certain about the messages it receives, but it may be uncertain about the messages other agents have received. In a dynamic epistemic logic with distributed knowledge and with modalities for communication patterns, the latter are interpreted by updating Kripke models. We propose an axiomatization of communication pattern logic, and we show that collective bisimilarity (comparing models on their distributed knowledge) is preserved when updating models with communication patterns. We can also interpret communication patterns by updating simplicial complexes, a well-known topological framework for distributed computing. We show that the different semantics correspond, and propose collective bisimulation between simplicial complexes.
△ Less
Submitted 1 August, 2023; v1 submitted 2 July, 2022;
originally announced July 2022.
-
Satisfiability of Quantified Boolean Announcements
Authors:
Hans van Ditmarsch,
Tim French,
Rustam Galimullin
Abstract:
Dynamic epistemic logics consider formal representations of agents' knowledge, and how the knowledge of agents changes in response to informative events, such as public announcements. Quantifying over informative events allows us to ask whether it is possible to achieve some state of knowledge, and has important applications in synthesising secure communication protocols. However, quantifying over…
▽ More
Dynamic epistemic logics consider formal representations of agents' knowledge, and how the knowledge of agents changes in response to informative events, such as public announcements. Quantifying over informative events allows us to ask whether it is possible to achieve some state of knowledge, and has important applications in synthesising secure communication protocols. However, quantifying over quite simple informative events, public announcements, is not computable: such an arbitrary public announcement logic, APAL, has an undecidable satisfiability problem. Here we consider even simpler informative events called Boolean announcements, where announcements are restricted to be a Boolean combination of atomic propositions. The logic is called Boolean arbitrary public announcement logic, BAPAL. A companion paper provides a complete finitary axiomatization, and related expressivity results, for BAPAL. In this work the satisfiability problem for BAPAL is shown to decidable, and also that BAPAL does not have the finite model property.
△ Less
Submitted 2 June, 2022;
originally announced June 2022.
-
Boolean Observation Games
Authors:
Hans van Ditmarsch,
Sunil Simon
Abstract:
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 vari…
▽ More
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.
△ Less
Submitted 8 February, 2024; v1 submitted 7 February, 2022;
originally announced February 2022.
-
No Finite Model Property for Logics of Quantified Announcements
Authors:
Hans van Ditmarsch,
Tim French,
Rustam Galimullin
Abstract:
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…
▽ More
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.
△ Less
Submitted 21 June, 2021;
originally announced June 2021.
-
Neighbourhood semantics for graded modal logic
Authors:
**sheng Chen,
Hans van Ditmarsch,
Giuseppe Greco,
Apostolos Tzimoulis
Abstract:
We introduce a class of neighbourhood frames for graded modal logic embedding Kripke frames into neighbourhood frames. This class of neighbourhood frames is shown to be first-order definable but not modally definable. We also obtain a new definition of graded bisimulation with respect to Kripke frames by modifying the definition of monotonic bisimulation.
We introduce a class of neighbourhood frames for graded modal logic embedding Kripke frames into neighbourhood frames. This class of neighbourhood frames is shown to be first-order definable but not modally definable. We also obtain a new definition of graded bisimulation with respect to Kripke frames by modifying the definition of monotonic bisimulation.
△ Less
Submitted 19 May, 2021;
originally announced May 2021.
-
Wanted Dead or Alive : Epistemic logic for impure simplicial complexes
Authors:
Hans van Ditmarsch,
Roman Kuznets
Abstract:
We propose a logic of knowledge for impure simplicial complexes. Impure simplicial complexes represent synchronous distributed systems under uncertainty over which processes are still active (are alive) and which processes have failed or crashed (are dead). Our work generalizes the logic of knowledge for pure simplicial complexes, where all processes are alive, by Goubault et al. In our semantics,…
▽ More
We propose a logic of knowledge for impure simplicial complexes. Impure simplicial complexes represent synchronous distributed systems under uncertainty over which processes are still active (are alive) and which processes have failed or crashed (are dead). Our work generalizes the logic of knowledge for pure simplicial complexes, where all processes are alive, by Goubault et al. In our semantics, given a designated face in a complex, a formula can only be true or false there if it is defined. The following are undefined: dead processes cannot know or be ignorant of any proposition, and live processes cannot know or be ignorant of factual propositions involving processes they know to be dead. The semantics are therefore three-valued, with undefined as the third value. We propose an axiomatization that is a version of the modal logic S5. We also show that impure simplicial complexes correspond to certain Kripke models where agents' accessibility relations are equivalence relations on a subset of the domain only. This work extends a WoLLIC 21 conference publication with the same title.
△ Less
Submitted 20 April, 2023; v1 submitted 4 March, 2021;
originally announced March 2021.
-
Everyone Knows that Everyone Knows: Gossip Protocols for Super Experts
Authors:
Hans van Ditmarsch,
Malvin Gattinger,
Rahim Ramezanian
Abstract:
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…
▽ More
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.
△ Less
Submitted 22 December, 2022; v1 submitted 26 November, 2020;
originally announced November 2020.
-
To Be Announced
Authors:
Hans van Ditmarsch
Abstract:
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 o…
▽ More
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.
△ Less
Submitted 15 March, 2023; v1 submitted 13 April, 2020;
originally announced April 2020.
-
Knowledge and simplicial complexes
Authors:
Hans van Ditmarsch,
Eric Goubault,
Jeremy Ledent,
Sergio Rajsbaum
Abstract:
Simplicial complexes are a versatile and convenient paradigm on which to build all the tools and techniques of the logic of knowledge, on the assumption that initial epistemic models can be described in a distributed fashion. Thus, we can define: knowledge, belief, bisimulation, the group notions of mutual, distributed and common knowledge, and also dynamics in the shape of simplicial action model…
▽ More
Simplicial complexes are a versatile and convenient paradigm on which to build all the tools and techniques of the logic of knowledge, on the assumption that initial epistemic models can be described in a distributed fashion. Thus, we can define: knowledge, belief, bisimulation, the group notions of mutual, distributed and common knowledge, and also dynamics in the shape of simplicial action models. We give a survey on how to interpret all such notions on simplicial complexes, building upon the foundations laid in prior work by Goubault and others.
△ Less
Submitted 20 February, 2020;
originally announced February 2020.
-
Strengthening Gossip Protocols using Protocol-Dependent Knowledge
Authors:
Hans van Ditmarsch,
Malvin Gattinger,
Louwe B. Kuijer,
Pere Pardo
Abstract:
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 se…
▽ More
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.
△ Less
Submitted 29 July, 2019;
originally announced July 2019.
-
How does uncertainty about other voters determine a strategic vote?
Authors:
Zeinab Bakhtiari,
Hans van Ditmarsch,
Abdallah Saffidine
Abstract:
We propose a framework for strategic voting when a voter may lack knowledge about the preferences of other voters, or about other voters' knowledge about her own preference. In this setting we define notions of manipulation, equilibrium, and dominance, under uncertainty. We provide scenarios wherein the profiles of true preferences are the same but the equilibrium profiles are different, because t…
▽ More
We propose a framework for strategic voting when a voter may lack knowledge about the preferences of other voters, or about other voters' knowledge about her own preference. In this setting we define notions of manipulation, equilibrium, and dominance, under uncertainty. We provide scenarios wherein the profiles of true preferences are the same but the equilibrium profiles are different, because the voters have different knowledge about other voters. We also model actions that change such uncertainty about preferences, such as a voter revealing her preference. We show that some forms of manipulation and equilibrium are preserved under such uncertainty updates and others not. We then formalize epistemic voting terminology in a logic. Our aim is to provide the epistemic background for the analysis and design of voting rules that incorporate uncertainty.
△ Less
Submitted 11 May, 2019; v1 submitted 27 September, 2018;
originally announced September 2018.
-
Positive Announcements
Authors:
Hans van Ditmarsch,
Tim French,
James Hales
Abstract:
Arbitrary public announcement logic (APAL) 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 (APAL+), which restricts arbitrary public announcements to announcement of positive formula…
▽ More
Arbitrary public announcement logic (APAL) 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 (APAL+), 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, APAL+ is rather different from APAL. We show that APAL+ is more expressive than public announcement logic PAL, and that APAL+ is incomparable with APAL. We also provide a sound and complete infinitary axiomatisation.
△ Less
Submitted 22 July, 2020; v1 submitted 5 March, 2018;
originally announced March 2018.
-
Arrow Update Synthesis
Authors:
Hans van Ditmarsch,
Wiebe van der Hoek,
Barteld Kooi,
Louwe B. Kuijer
Abstract:
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…
▽ More
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 phi, we can construct (synthesize) that model from phi. We also point out some pregnant differences in update expressivity between arrow update logics, action model logics, and refinement modal logic.
△ Less
Submitted 24 October, 2019; v1 submitted 3 February, 2018;
originally announced February 2018.
-
Quantifying over Boolean announcements
Authors:
Hans van Ditmarsch,
Tim French
Abstract:
Various extensions of public announcement logic have been proposed with quantification over announcements. The best-known extension is called arbitrary public announcement logic, APAL. It contains a primitive language construct Box phi intuitively expressing that "after every public announcement of a formula, formula phi is true". The logic APAL is undecidable and it has an infinitary axiomatizati…
▽ More
Various extensions of public announcement logic have been proposed with quantification over announcements. The best-known extension is called arbitrary public announcement logic, APAL. It contains a primitive language construct Box phi intuitively expressing that "after every public announcement of a formula, formula phi is true". The logic APAL is undecidable and it has an infinitary axiomatization. Now consider restricting the APAL quantification to public announcements of Boolean formulas only, such that Box phi intuitively expresses that "after every public announcement of a Boolean formula, formula phi is true". This logic can therefore called Boolean arbitrary public announcement logic, BAPAL. The logic BAPAL is the subject of this work. Unlike APAL it has a finitary axiomatization. Also, BAPAL is not at least as expressive as APAL. A further claim that BAPAL is decidable is deferred to a companion paper.
△ Less
Submitted 20 January, 2022; v1 submitted 14 December, 2017;
originally announced December 2017.
-
Cheryl's Birthday
Authors:
Hans van Ditmarsch,
Michael Ian Hartley,
Barteld Kooi,
Jonathan Welton,
Joseph B. W. Yeo
Abstract:
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…
▽ More
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.
△ Less
Submitted 27 July, 2017;
originally announced August 2017.
-
A Logic for Global and Local Announcements
Authors:
Francesco Belardinelli,
Hans van Ditmarsch,
Wiebe van der Hoek
Abstract:
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…
▽ More
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.
△ Less
Submitted 27 July, 2017;
originally announced July 2017.
-
Asynchronous Announcements
Authors:
Philippe Balbiani,
Hans van Ditmarsch,
Saúl Fernández González
Abstract:
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 annou…
▽ More
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.
△ Less
Submitted 18 January, 2021; v1 submitted 8 May, 2017;
originally announced May 2017.
-
The Undecidability of Arbitrary Arrow Update Logic
Authors:
Hans van Ditmarsch,
Wiebe van der Hoek,
Louwe B. Kuijer
Abstract:
Arbitrary Arrow Update Logic is a dynamic modal logic that uses an arbitrary arrow update modality to quantify over all 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 that the satisfiability problem of Arbitrary Arrow Update Logic is co-RE hard, and therefo…
▽ More
Arbitrary Arrow Update Logic is a dynamic modal logic that uses an arbitrary arrow update modality to quantify over all 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 that the satisfiability problem of Arbitrary Arrow Update Logic is co-RE hard, and therefore undecidable, by a reduction of the tiling problem.
△ Less
Submitted 19 September, 2016;
originally announced September 2016.
-
True Lies
Authors:
Thomas Ågotnes,
Hans van Ditmarsch,
Yan**g Wang
Abstract:
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, wh…
▽ More
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.
△ Less
Submitted 27 April, 2017; v1 submitted 27 June, 2016;
originally announced June 2016.
-
Announcement as effort on topological spaces
Authors:
Hans van Ditmarsch,
Sophia Knight,
Aybüke Özgün
Abstract:
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 de…
▽ More
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.
△ Less
Submitted 23 June, 2016;
originally announced June 2016.
-
Dynamic Gossip
Authors:
Hans van Ditmarsch,
Jan van Eijck,
Pere Pardo,
Rahim Ramezanian,
François Schwarzentruber
Abstract:
A gossip protocol is a procedure for spreading secrets among a group of agents, using a connection graph. The goal is for all agents to get to know all secrets, in which case we call the execution of the protocol successful. We consider distributed and dynamic gossip protocols. In distributed gossip the agents themselves instead of a global scheduler determine whom to call. In dynamic gossip not o…
▽ More
A gossip protocol is a procedure for spreading secrets among a group of agents, using a connection graph. The goal is for all agents to get to know all secrets, in which case we call the execution of the protocol successful. We consider distributed and dynamic gossip protocols. In distributed gossip the agents themselves instead of a global scheduler determine whom to call. In dynamic gossip not only secrets are exchanged but also telephone numbers (agent identities). This results in increased graph connectivity. We define six such distributed dynamic gossip protocols, and we characterize them in terms of the topology of the graphs on which they are successful, wherein we distinguish strong success (the protocol always terminates, possibly assuming fair scheduling) from weak success (the protocol sometimes terminates). For five of these protocols strong (fair) and weak success are characterized by weakly connected graphs. This result is surprising because the protocols are fairly different. In the sixth protocol an agent may only call another agent if it does not know the other agent's secret. Strong success for this protocol is characterized by graphs for which the set of non-terminal nodes is strongly connected. Weak success for this protocol is characterized by weakly connected graphs satisfying further topological constraints that we define in the paper. One direction of this characterization is surprisingly harder to prove than the other results in this contribution.
△ Less
Submitted 12 February, 2018; v1 submitted 3 November, 2015;
originally announced November 2015.
-
Bisimulation and expressivity for conditional belief, degrees of belief, and safe belief
Authors:
Mikkel Birkegaard Andersen,
Thomas Bolander,
Hans van Ditmarsch,
Martin Holm Jensen
Abstract:
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…
▽ More
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.
△ Less
Submitted 25 February, 2016; v1 submitted 26 June, 2015;
originally announced June 2015.
-
An Introduction to Logics of Knowledge and Belief
Authors:
Hans van Ditmarsch,
Joseph Y. Halpern,
Wiebe van der Hoek,
Barteld Kooi
Abstract:
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.
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.
△ Less
Submitted 2 March, 2015;
originally announced March 2015.
-
A simple proof of the completeness of APAL
Authors:
Philippe Balbiani,
Hans van Ditmarsch
Abstract:
We provide a simple proof of the completeness of arbitrary public announcement logic APAL. The proof is an improvement over the proof found in the publication Knowable as Known after an Announcement.
We provide a simple proof of the completeness of arbitrary public announcement logic APAL. The proof is an improvement over the proof found in the publication Knowable as Known after an Announcement.
△ Less
Submitted 10 September, 2014; v1 submitted 9 September, 2014;
originally announced September 2014.
-
Knowing Whether
Authors:
Jie Fan,
Yan**g Wang,
Hans van Ditmarsch
Abstract:
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 ex…
▽ More
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.
△ Less
Submitted 12 December, 2013; v1 submitted 30 November, 2013;
originally announced December 2013.
-
Strategic Voting and the Logic of Knowledge
Authors:
Hans van Ditmarsch,
Jerome Lang,
Abdallah Saffidine
Abstract:
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 p…
▽ More
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.
△ Less
Submitted 23 October, 2013;
originally announced October 2013.
-
Knowledge, Awareness, and Bisimulation
Authors:
Hans van Ditmarsch,
Tim French,
Fernando R. Velazquez-Quesada,
Yi N. Wang
Abstract:
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 l…
▽ More
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.
△ Less
Submitted 23 October, 2013;
originally announced October 2013.
-
A geometric protocol for cryptography with cards
Authors:
Andrés Cordón-Franco,
Hans van Ditmarsch,
David Fernández-Duque,
Fernando Soler-Toscano
Abstract:
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 sp…
▽ More
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.
△ Less
Submitted 24 January, 2013; v1 submitted 17 January, 2013;
originally announced January 2013.
-
A colouring protocol for the generalized Russian cards problem
Authors:
Andrés Cordón-Franco,
Hans van Ditmarsch,
David Fernández-Duque,
Fernando Soler-Toscano
Abstract:
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…
▽ More
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.
△ Less
Submitted 26 March, 2014; v1 submitted 22 July, 2012;
originally announced July 2012.
-
Refinement Modal Logic
Authors:
Laura Bozzelli,
Hans van Ditmarsch,
Tim French,
James Hales,
Sophie Pinchinat
Abstract:
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…
▽ More
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.
△ Less
Submitted 25 December, 2013; v1 submitted 16 February, 2012;
originally announced February 2012.
-
A secure additive protocol for card players
Authors:
Andres Cordon-Franco,
Hans van Ditmarsch,
David Fernandez-Duque,
Joost J. Joosten,
Fernando Soler-Toscano
Abstract:
Consider three players Alice, Bob and Cath who hold a, b and c cards, respectively, from a deck of d=a+b+c cards. The cards are all different and players only know their own cards. Suppose Alice and Bob wish to communicate their cards to each other without Cath learning whether Alice or Bob holds a specific card.
Considering the cards as consecutive natural numbers 0,1,..., we investigate genera…
▽ More
Consider three players Alice, Bob and Cath who hold a, b and c cards, respectively, from a deck of d=a+b+c cards. The cards are all different and players only know their own cards. Suppose Alice and Bob wish to communicate their cards to each other without Cath learning whether Alice or Bob holds a specific card.
Considering the cards as consecutive natural numbers 0,1,..., we investigate general conditions for when Alice or Bob can safely announce the sum of the cards they hold modulo an appropriately chosen integer. We demonstrate that this holds whenever a,b>2 and c=1. Because Cath holds a single card, this also implies that Alice and Bob will learn the card deal from the other player's announcement.
△ Less
Submitted 1 November, 2011;
originally announced November 2011.
-
The Ditmarsch Tale of Wonders - The Dynamics of Lying
Authors:
Hans van Ditmarsch
Abstract:
We propose a dynamic logic of lying, wherein a 'lie that phi' (where phi is a formula in the logic) is an action in the sense of dynamic modal logic, that is interpreted as a state transformer relative to the formula phi. The states that are being transformed are pointed Kripke models encoding the uncertainty of agents about their beliefs. Lies can be about factual propositions but also about moda…
▽ More
We propose a dynamic logic of lying, wherein a 'lie that phi' (where phi is a formula in the logic) is an action in the sense of dynamic modal logic, that is interpreted as a state transformer relative to the formula phi. The states that are being transformed are pointed Kripke models encoding the uncertainty of agents about their beliefs. Lies can be about factual propositions but also about modal formulas, such as the beliefs of other agents or the belief consequences of the lies of other agents. We distinguish (i) an outside observer who is lying to an agent that is modelled in the system, from (ii) one agent who is lying to another agent, and where both are modelled in the system. For either case, we further distinguish (iii) the agent who believes everything that it is told (even at the price of inconsistency), from (iv) the agent who only believes what it is told if that is consistent with its current beliefs, and from (v) the agent who believes everything that it is told by consistently revising its current beliefs. The logics have complete axiomatizations, which can most elegantly be shown by way of their embedding in what is known as action model logic or the extension of that logic to belief revision.
△ Less
Submitted 21 March, 2012; v1 submitted 10 August, 2011;
originally announced August 2011.
-
Avoiding bias in cards cryptography
Authors:
M. D. Atkinson,
H. P. van Ditmarsch,
S. Roehling
Abstract:
We outline the need for stricter requirements for unconditionally secure cryptographic protocols inspired by the Russian Cards problem. A new requirement CA4 is proposed that checks for bias in single card occurrence in announcements consisting of alternatives for players' holdings of cards. This requirement CA4 is shown to be equivalent to an alternative requirement CA5. All announcements found…
▽ More
We outline the need for stricter requirements for unconditionally secure cryptographic protocols inspired by the Russian Cards problem. A new requirement CA4 is proposed that checks for bias in single card occurrence in announcements consisting of alternatives for players' holdings of cards. This requirement CA4 is shown to be equivalent to an alternative requirement CA5. All announcements found to satisfy CA4 are 2-designs. We also show that all binary designs are 3-designs. Instead of avoiding bias in announcements produced by such protocols, one may as well apply unbiased protocols such that patterns in announcements become meaningless. We gave two examples of such protocols for card deal parameters (3,3,1), i.e. two of the players hold three cards, and the remaining player, playing the role of eavesdropper, holds a single card.
△ Less
Submitted 16 February, 2007;
originally announced February 2007.
-
Semantic results for ontic and epistemic change
Authors:
H. P. van Ditmarsch,
B. P. Kooi
Abstract:
We give some semantic results for an epistemic logic incorporating dynamic operators to describe information changing events. Such events include epistemic changes, where agents become more informed about the non-changing state of the world, and ontic changes, wherein the world changes. The events are executed in information states that are modeled as pointed Kripke models. Our contribution cons…
▽ More
We give some semantic results for an epistemic logic incorporating dynamic operators to describe information changing events. Such events include epistemic changes, where agents become more informed about the non-changing state of the world, and ontic changes, wherein the world changes. The events are executed in information states that are modeled as pointed Kripke models. Our contribution consists of three semantic results. (i) Given two information states, there is an event transforming one into the other. The linguistic correspondent to this is that every consistent formula can be made true in every information state by the execution of an event. (ii) A more technical result is that: every event corresponds to an event in which the postconditions formalizing ontic change are assignments to `true' and `false' only (instead of assignments to arbitrary formulas in the logical language). `Corresponds' means that execution of either event in a given information state results in bisimilar information states. (iii) The third, also technical, result is that every event corresponds to a sequence of events wherein all postconditions are assignments of a single atom only (instead of simultaneous assignments of more than one atom).
△ Less
Submitted 6 November, 2007; v1 submitted 15 October, 2006;
originally announced October 2006.
