# algebra and sequent calculus for epistemic actions[精选推荐pdf]

Algebra and sequent calculus for epistemic actionsAlexandru Baltag and Bob CoeckeMehrnoosh Sadrzadeh Oxford University Computing laboratoryUniversit´ e du Qu´ ebecA Montr´ eal baltag / coeckecomlab.ox.ac.uksadrzadeh.mehrnooshcourrier.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, ination-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 ination state of agents, and it has applications to modelling and reasoning aboutination-flow and ination 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 ination flow in a multi-agent system has been presented in [8]but it does not present a al description of epistemic programs and their updates. The first attemptstoalizesuchprogramsandupdatesweredoneby 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 quantaleof 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Æwhereare propositions,are actions andare 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 factsand a finite set of agents, a state model is a triplewhereis the set of states,the accessibility relation for each agent, andthe 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 mapcalled the appearance map of agent. The significance of the appearance maps is as follows ifthen, whenever agentis in statehe considers stateas a ‘possible world’. In other words, if the actual state of the system is, agentthinksmay be the actual state.2As an example,1considertwo playersand 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, statein which ‘the coin lies Heads’ up , hence, and statein which the coin lies Tails up , hence. We depict the state modelas.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 agentsandcan see the face of the coin, but agentcannot 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 agenthas several arrows between states whereas agentsandhave 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 propositionover a state modelis a subsetof, containing all the states at which the proposition is ‘true’. The mapsandof the state model are extended to elements ofas followsNote that we have to use intersection and not union in definingsince a fact is entailed by an epistemic proposition when it holds at all the states of the proposition. This makes the passage fromtocontravariant. In other words, the actual algebra of facts is, that is,the complete boolean algebrawhere 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 factcorresponds to an epistemic proposition, saying that the fact holds in the current state. In the Toss model,andare 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, hencerepresent the four epistemic propositions of Toss. When a propositionhas exactly one statei.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 overis a triplesimilar to a state model except that we think of the elements ofas possible actions instead of possible states and the valuationassigns to each actiona precondition, i.e. a propositiondefinining the domain of applicability of actioncan 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 sinceis boolean we can equivalently consider the states at which the action cannot take place , denoted asfor 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 aswherestands for ‘cheating’ andfor ‘nothing happens’ and. The action modelcan be refined when replacingbyandwhereand, specifying what the referee saw in case of deceitAn epistemic programover an action modelis a subsetof; theandmaps are both extended covariantly by continuityThe union in the definition ofmaps for programs says that an epistemic program is applicable where at least one of its actions is applicable. This makes themap follow contravariantly by boolean negation i.e.. Epistemic programs introduce non-determinism wheneverthenis obtained fromby increasing nondeterminism; stands for “either actionor actiontakes place”. In our example with actions,andthe epistemic programstands 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 programoverisAs in the case of states and propositions, we use systematic ambiguity to identify determin- istic programswith their unique undferlying action.4Update.Given a state modeland an action modeloverwe define their update productto be a new state model given byhenceand. In our example, after the cheating actionwhere the coin has lied Heads up,andthink 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 anddepicted aboveNote that in generalandare not necessarily disjoint.2Definition 2.1 We define the update product of an epistemic propositionoverand an epis- temic programoveras the epistemic propositionThe propositionprovides the strongest postcondition forwith respect to epistemic program for each state inthe propositionholds before running the. It can be seen thatiff, whereis the falsum i.e. the trivially false epistemic proposition over.Modalities.We define the epistemic modality for each agentas the unary connective which assigns to propositionoveranother propositionWe readas ‘agentknows or believes’.3We define the dynamic modality for each epistemic programoveras the unary connec- tive which assigns to propositionoveranother proposition℄Note that as mentioned before some statescan be themselves pairs of states and actionswhich make the above definition well defined. The proposition℄provides the weakest preconditionforwith respect to theepistemicprogram foreach statein℄thepropositionholds 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 compositionoverof two action modelsandboth overmeans ‘first doand then do’ and is defined as℄Again note thatandor are not necessarily disjoint.4The action model over a state modelcontains an action skip in which nothing happens iff5skipskipskipskipskipNotice 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 programsoverandoveras the epistemic propositionover.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 modelDefinition 2.3 A DEL model is a pairwhereis a state model andis an action model oversuch that skip,and.Definition 2.4 GivenaDELmodel, aconcreteepistemicsystemis thepair which goes equipped with valuation, appearance mapsand all other operations of the DEL model extended toandas we showed above.3The algebra of programs and propositionsA sup-latticeis a complete lattice with maps which preserve arbitrary joins as homomorphism. Recall that each sup-lattice also has arbitrary meets, namelyfor 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 ofbyandrespectively anddefine its set of atoms as4In fact later we only consider models where. 5This action has been denoted asin the preceding examples.6A latticeis atomistic iff