Algebra and sequent calculus for epistemic actionsAlexandru Baltag and Bob CoeckeMehrnoosh Sadrzadeh Oxford University Computing laboratoryUniversit´ e du Qu´ ebec`A Montr´ eal baltag /

[email protected]@courrier.uqam.caAbstractWe introduce an algebraic approach to Dynamic Epistemic Logic. This approach has the advantage that: (i) its semantics is a transparent algebraic object with a minimal set of primi- tives from which most ingredients of Dynamic Epistemic Logic arise, (ii) it goes with the in- troduction of non-determinism, (iii) it naturally extends beyond boolean sets of propositions, up to intuitionistic and non-distributive situations, hence allowing to accommodate construc- tive computational, information-theoretic as well as non-classical physical settings, and (iv) introduces a structure on the actions, which now constitute a quantale. We also introduce a corresponding sequent calculus (which extends Lambek calculus), in which propositions, actions as wellas agents appear as resources in aresource-sensitive dynamic-epistemic logic.1IntroductionDynamic Epistemic Logic (DEL) is a PDL-style logic to reason about epistemic actions and updates in a multi-agentsystem. It focuses in particularon epistemicprograms, i.e. programs that update the information state of agents, and it has applications to modelling and reasoning aboutinformation-flow and information exchange between agents. This is a major problem in severalfields such as secure communication where one has to deal with the privacy and authenticationof communication protocols, Artificial Intelligence where agents are to be provided with reliable tools to reason about their environment and each other’s knowledge, and e-commerce where agents need to have knowledge acquisition strategies over complex networks.The standard approach to information flow in a multi-agent system has been presented in [8]but it does not present a formal description of epistemic programs and their updates. The first attemptstoformalizesuchprogramsandupdatesweredoneby Plaza[21], Gerbrandyand Groen- eveld [12], and Gerbrandy [10, 11]. However, they only studied a restricted class of epistemic programs. A general notion of epistemicprograms and updates for DEL was introduced in [4, 5]. However, in this approach the underlying logic on propositions is boolean. For computational purposes one might want to relax this to an intuitionistic setting, hence conceiving propositions as being structured in a Heyting algebra. On the other hand, continuous lattices are also mod- els of partiality of knowledge [9], and are in general not distributive. Finally, actual physical computational situations such as quantum computation require (at least) a non-boolean setting.1In this paper we generalize ‘boolean’ DEL by introducing the notion of an abstract epis- temic system. This generalization goes hand-in-hand with the introduction of non-determinism for states and actions and brings algebraic clarity to the semantics. The particular algebraic ob-ject which we introduce is a refinement of previously used objects tailored to study concurrency in computer science [1, 22] and the dynamics and interaction of physical systems [6]. Such an abstract epistemic system consists of a quantale?of epistemic programs, a?-right module? of epistemic propositions, and each agent is encoded by an appearance map i.e. an endomor- phism of the?????-structure. We show that the boolean DEL of [5] is a concrete example of such an abstract epistemic system. The axioms of the modal operators follow immediately fromabstract properties of quantales and modules over them. Crucial notions of DEL are definable abstractly and some new notions emerge naturally. The passage to a non-boolean theory also provides a new insight into epistemic programs such as public announcement and, of a surpris- ingly different status, public refutation. We sketch an analysis of the muddy children puzzle and of a cryptographic attack in our setting and also provide a motivating example for the passage to a non-boolean theory. We also provide a corresponding sequent calculus in which sequents will typically look like??????????????????????????????????????Æwhere?????????are propositions,?????????are actions and????????are agents which re- solve into a single proposition or actionÆ. The fragment of the calculus restricted to actions is the Lambek calculus [18], hence resource sensitive.2Epistemic propositions and epistemic programsIn this section we slightly recast and enrich the Dynamic Epistemic Logic of [5] in such a way that it enables a smooth passage to the algebraic setting to be introduced in Section 4. Part of this involves the introduction of non-determinism for both states and actions.State models.For a set of facts?and a finite set of agents?, a state model is a triple?????????????where?is the set of states,??????the accessibility relation for each agent???, and????????the valuation map which encodes satisfaction???????????. The “facts”???are simple, objectives features of the world (“objective” in the sense of non-epistemic, i.e. independent of the agents’ knowledge or beliefs), and the valuation map tell us what facts hold in a given state???. Each accessibility relation can be repackaged as a map????????????????????????????????called the appearance map of agent?. The significance of the appearance maps is as follows: if???????then, whenever agent?is in state?he considers state?as a ‘possible world’. In other words, if the actual state of the system is?, agent?thinks?may be the actual state.2As an example,1considertwo players???and a referee?. In front of everybody, the referee throws a fair coin, catches it in his palm and fully covers it, before anybody (including himself) can see on which side the coin has landed. There are two possible states here, state?in which ‘the coin lies Heads’ up (????), hence????????, and state?in which the coin lies Tails up (????), hence????????. We depict the state model????as?????????????????????????????????????????????.Forevery agent there are arrows between any two states (includingidentical states), which means that nobody knows the ‘real state’. We can also consider a case in which agents?and?can see the face of the coin, but agent?cannot see it (although he knows that the others see it), so he is still uncertain if the coin is heads or tails. In this case only agent?has several arrows between states whereas agents?and?have only one arrow in each state, which means that if the coin is heads up they know it and similarly for tails up. Hence PToss gets depicted as???????????????????????????????????????????.An epistemic proposition?over a state model?is a subset?of?, containing all the states at which the proposition is ‘true’. The maps?and??of the state model are extended to elements of?as follows??????????????????????????????????????????????????Note that we have to use intersection and not union in defining????since a fact is entailed by an epistemic proposition when it holds at all the states of the proposition. This makes the passage from????to????contravariant. In other words, the actual algebra of facts is??????, that is,the complete boolean algebra????where the order is reversed i.e.?????????????. While facts are simple and non-epistemic, and thus cannot be altered by epistemic actions (see further), epistemic propositions can express complex features of the world, which may depend on the agents’ knowledge (and so may be changed by epistemic actions). However, notice that each fact???corresponds to an epistemic proposition????????????????, saying that the fact holds in the current state. In the Toss model,?and?are facts expressing the heads up or tails up of the coin. The epistemic propositions that correspond to these facts are the states in which the fact holds. The epistemic propositions are?????????????????????. We depict an epistemic proposition over a state model by double-circling the included states, hence????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????represent the four epistemic propositions of Toss. When a proposition?has exactly one state???(i.e.?????is a singleton), we shall use systematic ambiguity, identifying the proposition with the state and writing e.g.?????.1For a more elaborated example of an authentication protocol we refer the reader to [2].3Action models.Given a state model?, an action model over?is a triple??????????similar to a state model except that we think of the elements of?as possible actions instead of possible states and the valuation????????assigns to each action?a precondition, i.e. a proposition????definining the domain of applicability of?: action?can happen in a state? iff??????; e.g. a truthful announcement of a fact can only happen in those states where that fact holds. Note that since????is boolean we can equivalently consider the states at which the action cannot take place , denoted as??????????????for each???. The effect of an actionon states and appearance maps will be defined below in terms of an epistemic update product. We introducean action model over Toss. Aftercatching the coin in his hand thereferee might secretly take a peek at the coin before covering it while nobody notices this. The action model is now depicted as?????????????????????????????????where?stands for ‘cheating’ and?for ‘nothing happens’ and??????????. The action modelcan be refined when replacing?by??and??where???????and???????, specifying what the referee saw in case of deceit:??????????????????????????????????????????????????An epistemic program?over an action model?is a subset?of?; the?and??maps are both extended covariantly by continuity??????????????????????????????????????????????????The union in the definition of?maps for programs says that an epistemic program is applicable where at least one of its actions is applicable. This makes the???map follow contravariantly by boolean negation i.e.?????????????. Epistemic programs introduce non-determinism: whenever?????then??is obtained from??by increasing nondeterminism;????????? stands for “either action??or action??takes place”. In our example with actions??,??and?the epistemic program???????stands for the non-deterministic action?, in the sense that the outcome of the toss can be either. We depict the program over an action by double-circling the including actions. Hence the picture of the program?????????over?is??????????????????????????????????????????????????????????????????As in the case of states and propositions, we use systematic ambiguity to identify determin- istic programs?????with their unique undferlying action?.4Update.Given a state model?and an action model?over?we define their update product???to be a new state model given by??????????????????????????????????????????????????????????hence???????and???????????????????. In our example, after the cheating action??where the coin has lied Heads up,?and?think that nobody knows on which side the coin is lying. But they are wrong! The system after this action can be updated by taking the update product of the two models Toss and??depicted above:????????????????????????????????????????????????????????????????????????????????Note that in general???and?are not necessarily disjoint.2Definition 2.1 We define the update product of an epistemic proposition?over?and an epis- temic program?over?as the epistemic proposition?????????????????????????????????The proposition???provides the strongest postcondition for?with respect to epistemic program?: for each state in???the proposition?holds before running the?. It can be seen that?????iff????????, where?is the falsum (i.e. the trivially false epistemic proposition over?).Modalities.We define the epistemic modality for each agent???as the unary connective which assigns to proposition???over?another proposition?????????????????????????We read???as ‘agent?knows or believes?’.3We define the dynamic modality for each epistemic program?over?as the unary connec- tive which assigns to proposition???over?another proposition??℄????????????????????????????????????????Note that (as mentioned before) some states???can be themselves pairs of states and actions?????which make the above definition well defined. The proposition??℄?provides the weakest preconditionfor?with respect to theepistemicprogram?: foreach statein??℄?theproposition?holds after running?.2In fact later, the most important models we shall consider later (DEL models) are closed with respect to updateproduct, i.e.?????. 3Taking either ‘knows’ or ‘beliefs’ depends on the context.5Sequential composition.The sequential composition?????over?of two action models??and??both over?means ‘first do??and then do??’ and is defined as???????????????????????????????????????????????????????℄??????Again note that?????and??(or??) are not necessarily disjoint.4The action model over a state model?contains an action skip in which nothing happens iff5skip??skip??skip???????????skip???skip??Notice the use of systematicambiguity: we denoted with the same name (skip ) both the program skip and its only action. It is easy to see that skip is a unit, up to isomorphism, both for update product and sequential composition.Definition 2.2 We define the sequential composition of two epistemic programs??over??and??over??as the epistemic proposition????????????over?????.Concrete epistemic systems.We now have all the tools to make the passage of DEL in the sense of [5] to ‘concrete epistemic systems’ which we put forward as a stepping-stone towards ‘abstract epistemic systems’. A DEL model is essentially one that is closed underupdate product and sequential composition (and contains a skip), while a concrete epistemic system consists of all the epistemic propositions and all the epistemic programs of a DEL model:Definition 2.3 A DEL model is a pair?????where?is a state model and?is an action model over?such that skip??,???????and???????.Definition 2.4 GivenaDELmodel?????, aconcreteepistemicsystemis thepair??????????? which goes equipped with valuation?, appearance maps???????and all other operations of the DEL model extended to????and????as we showed above.3The algebra of programs and propositionsA sup-lattice?is a complete lattice with maps which preserve arbitrary joins as homomorphism. Recall that each sup-lattice also has arbitrary meets, namely???????????????????for any???. Hence the designation ‘sup-lattice refers to the fact that we require structure- preserving maps only to preserve arbitrary joins (cf. the designations locales and frames for complete Heyting algebras [16]). We denote bottom and top of?by?and?respectively anddefine its set of atoms as??????????????????????????4In fact later we only consider models where?????. 5This action has been denoted as?in the preceding examples.6A lattice?is atomistic iff???