Representing an epistemic situation involving several agents obviously depends on the modeling point of view one takes. We start by identifying the types of modeling points of view which are logically possible. We call the one traditionally followed by epistemic logic the perfect external approach, because there the modeler is assumed to be an omniscient and external observer of the epistemic situation. In the rest of the paper we focus on what we call the internal approach, where the modeler is (...) one of the agents involved in the situation. For this approach we propose and axiomatize a logical formalism based on epistemic logic. This leads us to formalize some intuitions about the internal approach and about its connections with the external ones. Finally, we show that our internal logic is decidable and PSPACE-complete. (shrink)

Dynamic Epistemic Logic This article tells the story of the rise of dynamic epistemic logic, which began with epistemic logic, the logic of knowledge, in the 1960s. Then, in the late 1980s, came dynamic epistemic logic, the logic of change of knowledge. Much of it was motivated by puzzles and paradoxes. The number … Continue reading Dynamic Epistemic Logic →.

In this paper, we investigate the use of event models for automated planning. Event models are the action defining structures used to define a semantics for dynamic epistemic logic. Using event models, two issues in planning can be addressed: Partial observability of the environment and knowledge. In planning, partial observability gives rise to an uncertainty about the world. For single-agent domains, this uncertainty can come from incomplete knowledge of the starting situation and from the nondeterminism of actions. In multi-agent domains, (...) an additional uncertainty arises from the fact that other agents can act in the world, causing changes that are not instigated by the agent itself. For an agent to successfully construct and execute plans in an uncertain environment, the most widely used formalism in the literature on automated planning is “belief states”: sets of different alternatives for the current state of the world. Epistemic logic is a significantly more expressive and theoretically better founded method for representing knowledge and ignorance about the world. Further, epistemic logic allows for planning according to the knowledge (and iterated knowledge) of other agents, allowing the specification of a more complex class of planning domains, than those simply concerned with simple facts about the world. We show how to model multi-agent planning problems using Kripke-models for representing world states, and event models for representing actions. Our mechanism makes use of slight modifications to these concepts, in order to model the internal view of agents, rather than that of an external observer. We define a type of planning domain called epistemic planning domains, a generalisation of classical planning domains, and show how epistemic planning can successfully deal with partial observability, nondeterminism, knowledge and multiple agents. Finally, we show epistemic planning to be decidable in the single-agent case, but only semi-decidable in the multi-agent case. (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)

Modern modal logic originated as a branch of philosophical logic in which the concepts of necessity and possibility were investigated by means of a pair of dual operators that are added to a propositional or first-order language. The field owes much of its flavor and success to the introduction in the 1950s of the “possible-worlds” semantics in which the modal operators are interpreted via some “accessibility relation” connecting possible worlds. In subsequent years, modal logic has received attention as an attractive (...) approach towards formalizing such diverse notions as time, knowledge, or action. Nowadays, modal logics are applied in various disciplines, ranging from economics to linguistics and computer science. Consequently, there is by now a large variety of modal languages, with an even greater wealth of interpretations. For instance, many applications require a poly-modal framework consisting of a language with a family of modal operators and a semantics in which the corresponding accessibility relations are connected somehow. (shrink)

This paper obtains the weak completeness and decidability results for standard systems of modal logic using models built from formulas themselves. This line of work began with Fine (Notre Dame J. Form. Log. 16:229-237, 1975). There are two ways in which our work advances on that paper: First, the definition of our models is mainly based on the relation Kozen and Parikh used in their proof of the completeness of PDL, see (Theor. Comp. Sci. 113-118, 1981). The point is to (...) develop a general model-construction method based on this definition. We do this and thereby obtain the completeness of most of the standard modal systems, and in addition apply the method to some other systems of interest. None of the results use filtration, but in our final section we explore the connection. (shrink)

Dynamic Epistemic Logic This article tells the story of the rise of dynamic epistemic logic, which began with epistemic logic, the logic of knowledge, in the 1960s. Then, in the late 1980s, came dynamic epistemic logic, the logic of change of knowledge. Much of it was motivated by puzzles and paradoxes. The number … Continue reading Dynamic Epistemic Logic →.

We construct logical languages which allow one to represent a variety of possible types of changes affecting the information states of agents in a multi-agent setting. We formalize these changes by defining a notion of epistemic program. The languages are two-sorted sets that contain not only sentences but also actions or programs. This is as in dynamic logic, and indeed our languages are not significantly more complicated than dynamic logics. But the semantics is more complicated. In general, the semantics of (...) an epistemic program is what we call aprogram model. This is a Kripke model of ‘actions’,representing the agents' uncertainty about the current action in a similar way that Kripke models of ‘states’ are commonly used in epistemic logic to represent the agents' uncertainty about the current state of the system. Program models induce changes affecting agents' information, which we represent as changes of the state model, called epistemic updates. Formally, an update consists of two operations: the first is called the update map, and it takes every state model to another state model, called the updated model; the second gives, for each input state model, a transition relation between the states of that model and the states of the updated model. Each variety of epistemic actions, such as public announcements or completely private announcements to groups, gives what we call an action signature, and then each family of action signatures gives a logical language. The construction of these languages is the main topic of this paper. We also mention the systems that capture the valid sentences of our logics. But we defer to a separate paper the completeness proof. (shrink)

Dynamic Epistemic Logic (DEL) deals with the representation and the study in a multi-agent setting of knowledge and belief change. It can express in a uniform way epistemic statements about: 1. what is true about an initial situation 2. what is true about an event occurring in this situation 3. what is true about the resulting situation after the event has occurred. We axiomatize within the DEL framework what we can infer about (iii) given (i) and (ii). Given three formulas (...) φ,φ' and φ" describing respectively (i), (ii) and (iii), we also show how to build a formula φ ? φ' which captures all the information which can be inferred about (iii) from φ and φ'. We show how our results extend to other modal logics than K. In our proofs and definitions, we resort to a large extent to the normal form formulas for modal logic originally introduced by Kit Fine. In a companion paper (Aucher, 2012), we axiomatize what we can infer about (ii) given (i) and (iii), and what we can infer about (i) given (ii) and (iii), and show how to build two formulas φ ? φ" and φ' ? φ" which capture respectively all the information which can be inferred about (ii) from φ and φ", and all the information which can be inferred about (i) from φ' and φ". (shrink)

We show how belief revision can be treated systematically in the format of dynamicepistemic logic, when operators of conditional belief are added. The core engine consists of definable update rules for changing plausibility relations between worlds, which have been proposed independently in the dynamic-epistemic literature on preference change. Our analysis yields two new types of modal result. First, we obtain complete logics for concrete mechanisms of belief revision, based on compositional reduction axioms. Next, we show how various abstract postulates for (...) belief revision can be analyzed by standard modal frame correspondences for model-changing operations. (shrink)

This modern, advanced textbook reviews modal logic, a field which caught the attention of computer scientists in the late 1970's.