We model the ‘100 prisoners and a lightbulb’ 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. We specify the underlying nondeterministic protocol and verify its postconditions in a recent extension of the model checker DEMO with factual change. We also present (...) a synchronized version of the riddle, for which there are also other protocols, and we report on efforts to minimize the expected termination of such protocols when assuming random scheduling. (shrink)
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. (shrink)
This is a case-study in knowledge representation and dynamic epistemic protocol verification. 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 paper consists of three parts. First, we present different versions of the puzzle, and their solutions. 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 verify the basic protocol to solve the problem. Novel contributions in this paper 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.. (shrink)
We look at lying as an act of communication, where (i) the proposition that is communicated is not true, (ii) the utterer of the lie knows that what she communicates is not true, and (iii) the utterer of the lie intends the lie to be taken as truth. Rather than dwell on the moral issues, we provide a sketch of what goes on logically when a lie is communicated. We present a complete logic of manipulative updating, to analyse the effects (...) of lying in public discourse. Next, we turn to the study of lying in games. First, a game-theoretical analysis is used to explain how the possibility of lying makes such games interesting, and how lying is put to use in optimal strategies for playing the game. Finally, we give a matching logical analysis. Our running example of lying in games in liar’s dice. (shrink)
We propose a dynamic logic of lying, wherein a ‘lie that $\varphi $ ’ (where $\varphi $ 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 $\varphi $ . 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 two speaker perspectives: (Obs) an outside observer who is lying to an agent that is modelled in the system, and (Ag) an agent who is lying to another agent, and where both are modelled in the system. We distinguish three addressee perspectives: (Cred) the credulous agent who believes everything that it is told (even at the price of inconsistency), (Skep) the skeptical agent who only believes what it is told if that is consistent with its current beliefs, and (Rev) the belief revising agent who believes everything that it is told by consistently revising its current, possibly conflicting, 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 in the extension of that logic to belief revision. (shrink)
Krister Segerberg proposed irrevocable belief revision, to be contrasted with standard belief revision, in a setting wherein belief of propositional formulas is modelled explicitly. This suggests that in standard belief revision is revocable: one should be able to unmake (‘revoke’) the fresh belief in the revision formula, given yet further information that contradicts it. In a dynamic epistemic logical setting for belief revision, for multiple agents, we investigate what the requirements are for revocable belief revision. By this we not merely (...) mean recovering belief in non-modal propositions, as in the recovery principle for belief contraction, but recovering belief in modal propositions: beliefs about beliefs. These requirements are almost never met, a surprising result. (shrink)
We study the extension of public announcement logic PAL by public assignments, which we call PALA. Just as in the case of PAL, the standard procedure for deciding PALA validity, i.e. the use of so-called reduction axioms to translate PALA formulae into formulae in epistemic logic EL, may lead to exponential growth. In this paper, we show that such a price is not mandatory, for we provide a polynomial translation of PALA into EL. This is based on abbreviations of subformulae (...) by new propositional letters. Such optimal translation also enables us to show the computational complexity of the problem of deciding PALA validity, which turns out to be coNP-complete in the single-agent case and PSPACE-complete in the multiagent case. (shrink)
We propose strategic games wherein the strategies consist of players asking each other questions and answering those questions. We study simplifications of such games wherein two players simultaneously ask each other a question that the opponent is then obliged to answer. The motivation for our research is to model conversation including the dynamics of questions and answers, to provide new links between game theory and dynamic logics of information, and to exploit the dynamic/strategic structure that, we think, lies implicitly inside (...) epistemic models for epistemic languages, and to make that structure an explicit subject of logical study. Our main contributions are: the notion of a two-person question-answer game with information goals, the existence and computation of equilibria for these games, the correspondence with Bayesian games and their equilibria, and a connection between logic and game theory namely the existence of equilibria for positive goal formulae. (shrink)
Dynamic epistemic logic describes the possible information-changing actions available to individual agents, and their knowledge pre- and post conditions. For example, public announcement logic describes actions in the form of public, truthful announcements. However, little research so far has considered describing and analysing rational choice between such actions, i.e., predicting what rational self-interested agents actually will or should do. Since the outcome of information exchange ultimately depends on the actions chosen by all the agents in the system, and assuming that (...) agents have preferences over such outcomes, this is a game theoretic scenario. This is, in our opinion, an interesting general research direction, combining logic and game theory in the study of rational information exchange. In this article we take some first steps in this direction: we consider the case where available actions are public announcements, and where each agent has a (typically epistemic) goal formula that she would like to become true. What will each agent announce? The truth of the goal formula also depends on the announcements made by other agents. We analyse such public announcement games. (shrink)
As part of the conference commemorating Theoria's 75th anniversary, a round table discussion on philosophy publishing was held in Bergendal, Sollentuna, Sweden, on 1 October 2010. Bengt Hansson was the chair, and the other participants were eight editors-in-chief of philosophy journals: Hans van Ditmarsch (Journal of Philosophical Logic), Pascal Engel (Dialectica), Sven Ove Hansson (Theoria), Vincent Hendricks (Synthese), Søren Holm (Journal of Medical Ethics), Pauline Jacobson (Linguistics and Philosophy), Anthonie Meijers (Philosophical Explorations), Henry S. Richardson (Ethics) and Hans Rott (Erkenntnis).
Fitch showed that not every true proposition can be known in due time; in other words, that not every proposition is knowable. Moore showed that certain propositions cannot be consistently believed. A more recent dynamic phrasing of Moore-sentences is that not all propositions are known after their announcement, i.e., not every proposition is successful. Fitch's and Moore's results are related, as they equally apply to standard notions of knowledge and belief (S 5 and KD45, respectively). If we interpret ‘successful’ as (...) ‘known after its announcement’ and ‘knowable’ as ‘known after some announcement’, successful implies knowable. Knowable does not imply successful: there is a proposition ϕ that is not known after its announcement but there is another announcement after which ϕ is known. We show that all propositions are knowable in the more general sense that for each proposition, it can become known or its negation can become known. We can get to know whether it is true: ◊(Kϕ ∨ K¬ϕ). This result comes at a price. We cannot get to know whether the proposition was true. This restricts the philosophical relevance of interpreting ‘knowable’ as ‘known after an announcement’. (shrink)
We model the forgetting of propositional variables in a modal logical context where agents become ignorant and are aware of each others’ or their own resulting ignorance. The resulting logic is sound and complete. It can be compared to variable-forgetting as abstraction from information, wherein agents become unaware of certain variables: by employing elementary results for bisimulation, it follows that beliefs not involving the forgotten atom(s) remain true.
Hans van Ditmarsch and Barteld Kooi (2008). Semantic results for ontic and epistemic change. In: G. Bonanno, W. van der Hoek and M. Wooldridge (editors). Logic and the Foundations of Game and Decision Theory (LOFT 7). Texts in Logic and Games 3, pp. 87-117, Amsterdam University Press, Amsterdam.
We model three examples of beliefs that agents may have about other agents’ beliefs, and provide motivation for this conceptualization from the theory of mind literature. We assume a modal logical framework for modelling degrees of belief by partially ordered preference relations. In this setting, we describe that agents believe that other agents do not distinguish among their beliefs (‘no preferences’), that agents believe that the beliefs of other agents are in part as their own (‘my preferences’), and the special (...) case that agents believe that the beliefs of other agents are exactly as their own (‘preference refinement’). This multi-agent belief interaction is frame characterizable. We provide examples for introspective agents. We investigate which of these forms of belief interaction are preserved under three common forms of belief revision. (shrink)
Pit is a multi-player card game that simulates the commodities trading market, and where actions consist of bidding and of swapping cards. We present a formal description of the knowledge and change of knowledge in that game. The description is in a standard language for dynamic epistemics expanded with assignment. Assignment is necessary to describe that cards change hands. The formal description is a prerequisite to model Pit in game theory. The main contribution of this paper should be seen as (...) the rigorous formalization of all knowledge in Pit. (shrink)
In an information state where various agents have both factual knowledge and knowledge about each other, announcements can be made that change the state of information. Such informative announcements can have the curious property that they become false because they are announced. The most typical example of that is ‘fact p is true and you don’t know that’, after which you know that p, which entails the negation of the announcement formula. The announcement of such a formula in a given (...) information state is called an unsuccessful update. A successful formula is a formula that always becomes common knowledge after being announced. Analysis of information systems and ‘philosophical puzzles’ reveals a growing number of dynamic phenomena that can be described or explained by unsuccessful updates. This increases our understanding of such philosophical problems. We also investigate the syntactic characterization of the successful formulas. (shrink)
In ‘belief revision’ a theory is revised with a formula φ resulting in a revised theory . Typically, is in , one has to give up belief in by a process of retraction, and φ is in . We propose to model belief revision in a dynamic epistemic logic. In this setting, we typically have an information state (pointed Kripke model) for the theory wherein the agent believes the negation of the revision formula, i.e., wherein is true. The revision with (...) φ is a program *φ that transforms this information state into a new information state. The transformation is described by a dynamic modal operator [*φ], that is interpreted as a binary relation [ [*φ] ] between information states. The next information state is computed from the current information state and the belief revision formula. If the revision is successful, the agent believes φ in the resulting state, i.e., Bφ is then true. To make this work, as information states we propose ‘doxastic epistemic models’ that represent both knowledge and degrees of belief. These are multi-modal and multi-agent Kripke models. They are constructed from preference relations for agents, and they satisfy various characterizable multi-agent frame properties. Iterated, revocable, and higher-order belief revision are all quite natural in this setting. We present, for an example, five different ways of such dynamic belief revision. One can also see that as a non-deterministic epistemic action with two alternatives, where one is preferred over the other, and there is a natural generalization to general epistemic actions with preferences. (shrink)
In unconditionally secure protocols, a sender and receiver are able to communicate their secrets to each other without the eavesdropper(s) being able to learn the secret, even when the eavesdropper intercepts the entire communication. We investigate such protocols for the special case of deals of cards over players, where two players aim to communicate to each other their hand of cards without the remaining player(s) learning a single card from either hand. In this contribution we show that a particular protocol (...) of length strictly larger than two (i.e., consisting of more than just one announcement by one player, and one other announcement by the other player) is after all not acceptable, and therefore does not constitute a new solution. The demonstration requires a detailed case-based analysis. The result may bring a general approach to arbitrary finite-length protocols closer. (shrink)
Suppose we have a stack of cards that is divided over some players. For certain distributions of cards it is possible to communicate your hand of cards to another player by public announcements, without yet another player learning any of your cards. A solution to this problem consists of some sequence of announcements and is called an exchange. It is called a direct exchange if it consists of (the minimum of) two announcements only. The announcements in an exchange have a (...) special form: they are safe communications, an interesting new form of update. Certain unsafe communications turn out to be unsuccessful updates. A communication is a public announcement that is known to be true. Each communication may be about a set of alternative card deals only, and even about a set of alternatives to the communicating player's own hand only. We list the direct exchanges for a deal of seven cards where the two players holding three cards communicate their hands to each other. Our work may be applicable to the design of cryptographic protocols. (shrink)
To describe simultaneous knowledge updates for different subgroups we propose anepistemic language with dynamic operators for actions. The language is interpreted onequivalence states (S5 states). The actions are interpreted as state transformers. Two crucial action constructors are learning and local choice. Learning isthe dynamic equivalent of common knowledge. Local choice aids in constraining theinterpretation of an action to a functional interpretation (state transformer).Bisimilarity is preserved under execution of actions. The language is applied todescribe various actions in card games.