Concurrent dynamic epistemic logic for MAS H.P. van Ditmarsch
W. van der Hoek
B.P. Kooi
Computer Science University of Otago Dunedin, New Zealand
Computer Science University of Liverpool Liverpool, United Kingdom
Computing Science University of Groningen Groningen, the Netherlands
[email protected]
[email protected]
[email protected]
ABSTRACT When giving an analysis of knowledge in multiagent systems, one needs a framework in whi h higher-order information and its dynami s an both be represented. A re ent tradition starting in original work by Plaza treats all of knowledge, higher-order knowledge, and its dynami s on the same foot. Our work is in that tradition. It also ts in approa hes that not only dynamize the epistemi s, but also epistemize the dynami s: the a tions that (groups of) agents perform are epistemi a tions. Di erent agents may have di erent information about whi h a tion is taking pla e, in luding higher-order information. We demonstrate that su h information hanges require subtle des riptions. The
ontribution of our paper is that it provides a omplete axiomatization for an a tion language of van Ditmars h, where an a tion is interpreted as a relation between states and sets of states. The appli ability of the framework is found in every ontext where multiagent strategi de ision making is at stake, and already demonstrated in game-like s enarios su h as Cluedo and ard games. Categories and Subject Descriptors I.2.11 [Distributed Arti ial Intelligen e℄: Multiagent systems Keywords agent ommuni ation, on urren y, a tions, dynami logi , epistemi logi 1.
INTRODUCTION Sin e Hintikka's [14℄ epistemi logi , the logi of knowledge, has been a subje t of resear h in philosophy [15℄, omputer s ien e [9℄, arti ial intelligen e [17℄ and game theory [3℄. The latter three appli ation areas made it more and more apparent that in multiagent systems higher-order information, knowledge about other agents' knowledge, is
ru ial.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. AAMAS 2003, Melbourne, Australia Copyright 2002 ACM X-XXXXX-XX-X/XX/XX ...$5.00.
The famous paper [1℄ by Al hourron et al. put the hange of information, or belief revision, as a topi on the philosophi al and logi al agenda: it was followed by a large stream of publi ations and mu h resear h in: belief revision, netuning the notion of epistemi entren hement [18℄, revising ( nite) belief bases [6℄, di eren es between belief revision and belief updates [16℄, and the problem of iterated belief
hange [8℄. However, in all these approa hes the dynami s is studied at a level above the informational level, making it impossible to reason about hange of agents' knowledge and ignoran e within the framework, let alone about the hange of other agents' information. Our work takes these the observations on higher-order knowledge and hange of information as a starting point: when giving an analysis of knowledge in multiagent systems, one needs a framework in whi h higher-order information and its dynami s an be represented. Although the notion of a run in an interpreted system as des ribed in [9℄ makes it in prin iple possible to reason about the dynami s of an agent's knowledge, the interpretation of a run is typi ally that of a standard program. Further, the pioneering work of Moore [17℄ also studies the relation between a tions and knowledge: there the emphasis is on epistemi pre onditions that are needed to perform ertain a tions in the world, su h as knowing a key- ombination in order to open a safe. From the point of view of expressivity, one an say that the work on interpreted systems enables one to reason about the ( hange of) knowledge over time, and by adding a tions to the language, one an also reason about the hange of knowledge brought about by performing ertain plans. This enables one to express properties like perfe t re all and no learning. Re ently, based on work by Alur et al [2℄, van der Hoek and Wooldridge [25℄ added a so ial or oalitional aspe t to an epistemi framework, giving them the possibility to express that for instan e a group an establish that some knowledge is eventually obtained, or that two agents an enfor e that they ex hange a se ret, without a third agent getting to know this. Our work ts in approa hes that not only dynamize the epistemi s, but also epistemize the dynami s: the a tions that (groups of) agents perform are epistemi a tions. Different agents may have di erent information about whi h a tion is taking pla e, in luding higher-order information. This rather re ent tradition treats all of knowledge, higherorder knowledge, and its dynami s on the same foot. Following an original ontribution by Plaza in 1989 [22℄, a stream of publi ations appeared around the year 2000 [11, 10, 4, 26,
24, 5, 29, 28, 23℄. The following, possibly simplest example in the setting of MAS (two agents, one atom) tries to demonstrate that the notions of higher-order information and epistemi a tions are indeed important and may be subtle. Anne and Bert are in a bar, sitting at a table. A messenger omes in and delivers a letter to Anne. The letter ontains either an invitation for a night out in Amsterdam, or an obligation to give a le ture instead. Anne and Bert ommonly know that these are the only alternatives.
This situation an be modelled as follows: There is one atom p, des ribing `the letter ontains an invitation for a night out in Amsterdam', so that :p stands for the le ture obligation. There are two agents 1 (Anne) and 2 (Bert). Whatever happens in ea h of the following a tion s enarios, is publi ly known (to Anne and Bert). Also, assume that in fa t p is true. A tion s enario
1. Anne reads the letter aloud. (tell)
A tion s enario
2. Bert is seeing that Anne reads the
letter. (read)
A tion s enario 3. Bert orders a drink at the bar so that Anne may have read the letter. (mayread) A tion s enario 4. Bert orders a drink at the bar while Anne goes to the bathroom. Both may have read the letter. (bothmayread)
After exe ution of the rst s enario it is ommon knowledge that p: in the resulting state C12 p (i.e. Cf1;2g p) holds. This is not the ase in the se ond s enario, but still, some
ommon knowledge is obtained there: C12 (K1 p _ K1 :p): it is ommonly known that Anne knows the ontents of the letter, irrespe tive of it being p or :p. Does this higherorder information hange in S enario 3? Yes, in this ase Bert does not even know if Anne knows p or knows :p: :K2 (K1 p _ K1 :p). In S enario 4 something similar happens, that may best be des ribed by saying that the agents
on urrently learn that the other may have learnt p or :p. Now both agents may have learnt p, after whi h p is generally known { E12 p {, but they are in that ase unaware of ea h other's knowledge { :C12 p {, and that is ommonly known. Van Ditmars h has des ribed su h a tions as knowledge a tions (with orresponding dynami modal operators) in a multiagent dynami epistemi language [26, 29℄. Knowledge a tions are interpreted as a relation between states. The ontribution of our paper is that it provides a omplete axiomatization for the extension of this language with
on urren y as found in [27, 28℄. This builds on work on
on urren y in dynami logi (PDL) [21, 13, 12℄ and is partially related to game theoreti al semanti s for (extensions of) PDL [19, 20℄. The appli ability of the framework is found in every ontext where multiagent strategi de ision making is at stake, and already demonstrated in game-like s enarios su h as Cluedo and ard games [26℄. Se tion 2 introdu es the language and its semanti s. Se tion 3 de nes the axioms and derivation rules, its synta ti
1; 2
p
p
:
p
bothmayread
1
p
p
2
:
1
2
2 2
p
1
p 1; 2
p
:
2 1
p
:
1
p
:
mayread tell
p
read
p
2
p
:
p
2
2
p
p
:
2 1; 2
p
:
Figure 1: A tions for two agents and one atom. The
top left gure represents (Ar ; u). Points of models are underlined. Assume transitivity of a
ess. For mayread and bothmayread only one of more exe utions is shown.
prerequisites su h as synta ti equivalen e of a tions, and shows the soundness of this proof system. Se tion 4 shows the ompleteness of this proof system. Se tion 5 gives some appli ations of the language in spe ifying MAS dynami s, and is followed by the on lusions (Se tion 6). Almost all proofs have been omitted.
2. LANGUAGE AND SEMANTICS Stru tures Given a nite set of agents N and a set of atoms P , a (Kripke) model M = hW; R; V i onsists of a domain W of worlds or fa tual states, for ea h agent n 2 N a binary a
essibility relation Rn on W , and a valuation V : P ! P (W ), or in other words: for ea h atom p 2 P , a subset Vp of W . Given a model, the operator gr returns the set of agents: gr(hW; R; V i) = N ; this is alled the group of the model. The group of a set of models is the union of the groups of these models. In an epistemi model ( ommonly known as an S 5 model) all a
essibility relations are equivalen e relations. We then write n for the equivalen e relation for agent n. If w n w0 we say that w is the same as w0Sfor n, or that w is equivalent to w0 for n. Write B for ( n2B n ) . Write S 5N (P ) for the lass of epistemi S models for agents N and atoms P , write S 5N (P ) for BN S 5B (P ). We drop the `P ' if it is lear from the
ontext. For a given model M , D(M ) returns its domain. Instead of w 2 D(M ) we also write w 2 M . Given a model M and a world w 2 M , (M; w) is alled a modal state, w the point of that state, and M the model underlying that state. Also, if M is lear from the ontext, write w for (M; w). Similarly, we visually point to a world in a gure by underlining it. If s = (M; w) and w 2 D(M ) we also write w 2 s. All notions for models are assumed to be similarly de ned for modal states. Write S 5N (P ) for the lass of epistemi states (`pointed' - `' - models) for agents N and atoms P . Example 5. The ba kground setting for `Le ture or Amsterdam' an be represented by an epistemi state. Ar is the model hfu; v g; ; V i su h that both 1 and 2 are the universal relation on fu; v g, and Vp = fug. The state (Ar ; u)
orresponds to p being a tually the ase. After Anne has
read the letter, a state is rea hed that is like (Ar ; u) but with 1 = f(u; u); (v; v )g instead. See Figure 1.
Syntax To a standard multiagent epistemi language with ommon knowledge for a set N of agents and a set P of atoms [17, 9℄, we add dynami modal operators for programs that are alled knowledge a tions and that des ribe a tions. The language LN , the knowledge a tions La t N , and the group gr are de ned by simultaneous indu tion: Definition 6
(Formulas and a tions).
The formulas LN (P ) are de ned by
' ::= p j :' j (' ^ ') j Kn ' j CB ' j [ ℄ where p 2 P , n 2 N , B N , 2 La t N (P ), and a t Lgr ( ) (P ). The a tions LN (P ) are de ned by
2
?' j LB j ( ! ) j ( ; 0 ) j ( [ ) j ( \ ) 0 a t where ' 2 LN (P ), B N , 2 La t B (P ), and 2 Lgr( ) (P ), a t and where the group gr( ) of an a tion 2 LN (P ) is de ned as: gr(?') := ;, gr(LB ) := B , and gr( 0 ) := gr( ) \ gr( 0 ) for = ! ; \; [; ; .
Other propositional onne tives and modal operators are de ned abbreviations, in parti ular EB ' := V Kby'. standard n2B n Outermost parentheses of formulas and a tions are deleted whenever onvenient. As we may generally assume an arbitrary P , write LN instead of LN (P ), and La t N instead of La t N (P ). Instead of, e.g., Cfa;b; g we always write Cab . For an arbitrary epistemi (`box') operator K , write K^ for its dual (`diamond'). The dual of [ ℄ is 3 . The program onstru tor LB is alled learning. A tion ?' is a test, ( ; 0 ) is sequential exe ution, ( [ 0 ) is nondeterministi hoi e, ( ! 0 ) is alled lo al hoi e, and ( \ 0 ) is on urrent exe ution. The onstru t LB ?' is pronoun ed as `B learn that '', the onstru t ! 0 is pronoun ed as `from and 0 , hoose the rst'. We will see that the interpretation of lo al hoi e depends on the ontext of learning that binds it (as in LB ( ! 0 ): everybody in B but not in ; 0 , is unaware of the hoi e, that is therefore `lo al'). Th group gr was already used for the agents `o
urring' in epistemi states and models. It serves a similar fun tion on a tions, when e the overloading. We need it, be ause in expressions [ ℄', epistemi operators in ' must o
ur in epistemi states resulting from exe uting (or they would have no meaning). A nondeterministi a tion an have more than one exe ution in a given epistemi state. The only way to get su h an a tion is to use [ (nondeterministi hoi e) operators in its des ription. If we use ! operators instead, typi ally, only some but not all of the agents are aware of the hoi es made. Constru ts [ and ! are related by the type of an a tion: The type t of an a tion is de ned as t( ) := [!=[℄ (repla e all ! 's by ['s). Instead of ! 0 we generally write ! [ t( 0 ) or t( 0 )[ ! . This expresses more learly that given
hoi e between and 0 , the agents involved in those a tions
hoose , whereas that hoi e remains invisible to the agents that learn about these alternatives but are not involved. Example
7. The des ription in La t 12 (fpg) of the a tions
in the introdu tion are: tell L12 ?p [ L12 ?:p read L12 (L1 ?p [ L1 ?:p) mayread L12 (L1 ?p [ L1 ?:p[ ?>) bothmayread L12 ( (L1 ?p \ L2 ?p) [ (L1 ?:p \ L2 ?:p) [L1 ?p [ L1 ?:p [ L2 ?p [ L2 ?:p[ ?>) For example, the des ription of read (Anne reads the letter) reads as follows: `Anne and Bert learn that either Anne learns that she is invited for a night out in Amsterdam or that Anne learns that she has to give a le ture instead.' In the last two a tions, instead of ?> (for `nothing happens') we may as well write ?p[?:p. Example 8. The a tion read where Bert is seeing that Anne reads the letter is di erent from the a tion where Bert is seeing that Anne reads the letter and Anne is a tually invited for a night out. The last is des ribed as L12 (L1 ?p ! L1 ?:p): of the two alternatives L1 ?p and L1 ?:p the rst is
hosen, but agent 2 is unaware of that hoi e. A di erent way of writing that a tion is L12 (!L1 ?p [ L1 ?:p). The a tion read is its type. Somewhat similarly, the a tion bothmayread has four di erent exe utions if p is true and another four if p is false: there are eight ` on rete' a tions (state transformers) of that type.
Semanti s The semanti s of LN (on epistemi models) is de ned as usual [17℄, plus an additional lause for the meaning of dynami operators. The interpretation of a dynami operator is a relation between an epistemi state and a set of epistemi states. The omposition (R Æ R0 ) of two relations R; R0 : W ! P (W ) (su h as [ ℄ ) is de ned as follows: let v 2 W; V W , then: (R Æ R0 )(v; V ) :, 9V 0 : 0 0 : 9V 00 V : R0 (v 0 ; V 00 ) and V = R 8v 2 V S(v; V 0f)Vand 00 0 0 00 j R (v ; V )g. We write vR for fV j R(v; V )g. v 2V Further, R t R0 := f(v; V ) j 9V 0 ; V 00 : R(v; V 0 ); R0 (v; V 00 ); and V = V 0 [ V 00 g. In the semanti s, we need a notion of equivalen e between sets of epistemi states. We lift equivalen e of worlds in a state to equivalen e of states and to equivalen e of sets of states. Sets of states will o
ur as worlds in de nition 11 of a tion interpretation, and equivalen e of su h worlds for an agent will be de ned as equivalen e of those sets. 0
0
Definition 9
(Equivalen e of sets of states).
Let M; M 0 2 S 5N , v; w 2 M , and w0 2 M 0 . Let S; S 0 S 5N . Let n 2 N . Then: (M; w) n (M; v ) : i w n v (M; w) n (M 0 ; w0 ) : i 9v 2 M : (M; v ) $ (M 0 ; w0 ) and (M; w) n (M; v ) S n S 0 : i [ 8s 2 S : n 2 gr(s) ) 9s0 2 S 0 : s n s0 ℄ and [ 8s0 2 S 0 : n 2 gr(s0 ) ) 9s 2 S : s n s0 ℄
In the se ond lause of the de nition, $ stands for `is bisimilar to' [7℄. Bisimilarity is a notion of sameness between states that implies equivalen e of their logi al des riptions (theories), though not vi e versa. The impli it symmetri
losure in the third lause of the de nition is needed to keep n an equivalen e relation. We now ontinue with the semanti s. The interpretation of formulas and a tions is de ned simultaneously.
Definition 10
(Interpretation of formulas).
Let s = (M; w) 2 S 5N and ' 2 LN , where M = hW; ; V i. We de ne M; w j= ' by indu tive ases. M; w j= p : i w 2 V (p) M; w j= :' : i M; w 6j= ' M; w j= ' ^ : i M; w j= ' and M; w j= M; w j= Kn ' : i 8w0 : w0 n w ) M; w0 j= ' M; w j= CB ' : i 8w0 : w0 B w ) M; w0 j= ' M; w j= [ ℄' : i 8S S 5N : (M; w)[[ ℄ S ) 0 0 9s 2 S : s j= ' Definition 11
:p
?
L1 ?p
(Interpretation of a tions).
Let 2 LN . The interpretation [ ℄ of in an arbitary epistemi state s = (M; w) 2 S 5N , where M = hW; ; V i, is de ned by indu tive ases: [ ?'℄ := f(s; S ) j S = f(hW' ; ;; V jW' i; w)g g [ LB ℄ := f(s; S ) j 9S 0 : s[ ℄ S 0 and S = f(hW 0 ; 0 ; V 0 i; S 0 )g g [ ; 0 ℄ := [ ℄ Æ [ 0 ℄ [ [ 0 ℄ := [ ℄ [ [ 0 ℄ [ ! 0 ℄ := [ ℄ [ \ 0 ℄ := [ ℄ t [ 0 ℄ In the lause for `test', W' = fv 2 D(M ) j M; v j= 'g. In the lause for `learning': W 0 := f(M 0 ; v 0 ) j 9v 2 M : (M; v )[[t( )℄℄(M 0 ; v 0 )g; for an arbitrary agent n, 0n := n , seen as equivalen e between sets of epistemi states; and for an arbitrary atom p: S 00 2 Vp0 i [ for all (hW 00 ; 00 ; V 00 i; w00 ) = s00 2 S 00 , w00 2 Vp00 ℄. The notion h i is dual to [ ℄ and is de ned as s j= h i' i [ 9S S 5N : s[ ℄ S and 8s0 2 S : s0 j= ' ℄. This may be intuitively more appealing: from the given state s, we an rea h a set of of states S where ' holds everywhere (` on urrently'). Our treatment of the dynami operators is similar to that in dynami logi [21, 12℄. A test results in an epistemi state without a
ess for any agent. This is appropriate: how knowledge hanges is only expressed in `learning', so before we en ounter a learn operator we annot say anything at all about the knowledge of the agents in the state resulting from a tion exe ution: no a
ess. One might as well say that, while ompositionally interpreting an a tion, the omputation of agents' knowledge is deferred until L operators are en ountered. Learning LB is de ned in terms of t( ), and this is how lo al hoi e onstru tions ! 0 get their meaning from being bound by a learning operator. To exe ute an a tion LB in a state s, we do not just have to exe ute the a tual a tion in the a tual state s, but also any other a tion of the same type t( ) as in any other state s0 with the same underlying model as s. The results are the worlds in the state that results from exe uting LB 0 in s. Su h worlds (that are sets of states) annot be distinguished from ea h other by an agent n 2 B if it ould not distinguish their origins and it ould not distinguish the a tions resulting in those sets of states either. An appealing way to de ne the equivalen e between worlds in the lause for `learning' is to say that, for state transformers ; 0 of type (and by further lifting the notion of equivalen e of sets of states to equivalen e of relations { su h as indu ed by a tion interpretation): (M; v )[[ ℄ 0n (M; v 0 )[[ 0 ℄ i v n v 0 and [ ℄ n [ 0 ℄ The semanti s may appear omplex, be ause worlds in the model resulting from learning are a tually sets of epistemi a t
p
?
L1 ?:p
L12(L1 ?p [ L1?:p)
Figure 2: Details of the interpretation of a tion read in
(see Figure 1). All a
ess is visualized: a
ess for 1 is a straight arrow, a
ess for 2 is a dotted arrow. We have abstra ted from the point of Ar , the left two and middle a tions are a tually exe uted in (Ar ; u) and the right two in (Ar ; v). Linked boxes are identi al.
(Ar ; u)
states. It is therefore important to realize that this is merely a omplex naming devi e for worlds, but that the semanti s is simple where it matters: the a
essibility between worlds (simple: use n ), and the value of atoms (simple: keep
urrent value). If the interpretation of in s is not empty, we say that is exe utable in s. For all a tions ex ept on urrent knowledge a tions it is more intuitive to think of their interpretation as a relation between states than as a relation between a state and a set of states: if s[ ℄ fs0 g, we like to think of s0 as the result of exe uting in s. The notational abbreviation s[ ℄ s0 :, s[ ℄ fs0 g allows us to keep using this helpful intuition. Further, if the interpretation is fun tional as well, write s[ ℄ for the unique s0 su h that s[ ℄ s0 . If this is the
ase for arbitrary s, we all a state transformer. Note that tests are state transformers. Example 12. The interpretation of read = L12 (L1 ?p [ L1 ?:p) on (Ar ; u) (see Example 5) is de ned in terms of the interpretation of L1 ?p [ L1 ?:p on (Ar ; u) and (Ar ; v ). To interpret L1 ?p [ L1 ?:p on (Ar ; u) we may either interpret L1 ?p or L1 ?:p. Only the rst an be exe uted. The interpretation of L1 ?p on (Ar ; u) is de ned in terms of the interpretation of ?p on any state (Ar ; x) where ?p an be exe uted, i.e. where p holds, that is on (Ar ; u); (Ar ; u)[[?p℄ is the singleton state onsisting of world u without a
ess. This epistemi state is therefore the single world in the domain of (Ar ; u)[[L1 ?p℄ . That world has re exive a
ess for 1, be ause (Ar ; u)[[?p℄ 1 (Ar ; u)[[?p℄
Et . In the next and nal stage of the interpretation, note that (as worlds) (Ar ; u)[[L1 ?p℄ 2 (Ar ; u)[[L1 ?:p℄ be ause agent 2 does not o
ur in those states, but that (Ar ; u)[[L1 ?p℄ 61 (Ar ; u)[[L1 ?:p℄ be ause (Ar ; u)[[L1 ?p℄ is not bisimilar to (Ar ; u)[[L1 ?:p℄ . Further details have been omitted. See Figure 2, and Figure 1 for the other example a tions.
Various algebrai a tion properties hold, su h as asso iativity of [ and of \. The two main theorems of interest for the semanti s are (for proofs see [29℄): Theorem 13
(Bisim. implies modal equivalen e). 0 $ s , then
Let ' 2 LN . Let s; s0 be epistemi states. If s s j= ' , s0 j= '. Theorem 14
(A tion exe ution preserves bisim.). 0 Let 2 La t N and s; s 2 S 5N . For ea h S 2 S 5N there is a S 0 2 S 5N and a bije tion f : S ! S 0 su h that: If s $ s0 and s[ ℄ S , then s0 [ ℄ S 0 and for all s00 2 S : s00 $ f (s00 ).
A orollary of theorem 14 is the following: Corollary 15. Let s; s0 2 S 5N and let 2 La t N be a state transformer that is exe utable in s. If s $ s0 , then s[ ℄ $ s0 [ ℄ .
3.
PROOF SYSTEM In this se tion we present the proof system for on urrent dynami epistemi logi . It is based on the dynami episti logi s of [10℄ and [5℄, and on Con urrent PDL [21℄. We rst introdu e some synta ti notions to be used in the proof system: the set of state transformers that are the on retizations or instan es of an a tion, synta ti equivalen e of a tions, and the pre ondition of an a tion. A nondeterministi a tion an have more than one exe ution in a given epistemi state. By repla ing nondeterministi hoi e operators in a given a tion with lo al hoi e operators we get a on rete a tion, i.e. a state tranformer, of the same type. Definition 16. Set T ( ) is de ned by indu tion on a tion stru ture (no details) with only nontrivial lause T ( [ 0 ) := f ! 0 j 2 T ( ) and 0 2 T ( 0 )g [ f 0 ! j 2 T ( ) and 0 2 T ( 0 )g. Lemma 17. The interpretation of every a tion is equivalent to nondeterministi hoi e between all S the state transformers that are its on retizations: [ ℄ = [ 2T ( ) ℄ .
Given some , set T (t( )) is the set of all on retizations of t( ), i.e. the set of state transformers of type . We now use T (t( )) to de ne synta ti a
essibility between a tions: given the nite and e e tively omputable set of all a tions of the same type, whi h of those are synta ti ally indistinguishable for an agent n? We omit details: Definition 18
(Synta ti a
essibility).
Given 2 La t N and n 2 N , an equivalen e relation n indu es a partition on T (t( )).
Example 19. Consider a tion L12 (!L1 ?p [ L1 ?:p) (i.e., L12 (L1 ?p ! L1 ?:p)). We have that T (L12 (!L1 ?p [ L1 ?:p)) = fL12 (!L1 ?p [ L1 ?:p)g (it is already a state transformer), that t(L12 (!L1 ?p [ L1 ?:p)) = L12 (L1 ?p [ L1 ?:p) and that T (t(L12 (!L1 ?p [ L1 ?:p))) = fL12 (!L1 ?p [ L1 ?:p); L12 (L1 ?p [ !L1 ?:p)g: there are two state transformers of that type. Agent 1, but not agent 2, an tell learning p apart from learning :p: L12 (!L1 ?p [ L1 ?:p) 61 L12 (L1 ?p[ !L1 ?:p) L12 (!L1 ?p [ L1 ?:p) 2 L12 (L1 ?p[ !L1 ?:p) 0 Proposition 20. Given are 2 La t N , n 2 N , and ; 2 0 0 T (t( )). If n , then [ ℄ n [ ℄ . In other words: synta ti equivalen e of a tions implies semanti equivalen e. The onverse does not hold! But we will see that there are `just enough' indistinguishable a tions to ensure ompleteness. Theorem 21
(Preservation of a
essibility).
If v; v 0 2 M 2 S 5N su h that v n v 0 , and ; 0 2 La t N su h that n 0 , and (M; v )[[ ℄ S , then there is an S 0 su h that (M; v 0 )[[ 0 ℄ S 0 and S n S 0 . Corollary 22. For state transformers ; 0 we have: if v n v 0 and n 0 , then (M; v )[[ ℄ n (M; v 0 )[[ 0 ℄ .
The last notion that we need in the proof system is that of the pre ondition of an a tion. If the pre ondition of an a tion holds, the a tion an be exe uted. Definition 23
(Pre ondition).
pre(?') pre( ; ) pre( [ ) pre( \ ) pre( ! ) pre(LB ) Definition 24
:= := := := := :=
'
pre( ) ^ h ipre( ) pre( ) _ pre( ) pre( ) ^ pre( ) pre( ) pre( )
(Proof system).
a b
d e f g h i j k l m n o p
All propositional tautologies Kn (' ! ) ! (Kn ' ! Kn ) Kn ' ! ' Kn ' ! Kn Kn ' :Kn ' ! Kn :Kn ' CB ' ! (' ^ EB CB ') [?'℄ $ (' ! ) [ ; 0 ℄' $ [ ℄[ 0 ℄' [ [ 0 ℄' $ ([ ℄' ^ [ 0 ℄') [ \ 0 ℄' $ ([ ℄' _ [ 0 ℄') hLB i> $ pre(LB ) [ ! 0 ℄'V$ [ ℄' [ ℄' $ 2T ( ) [ ℄' [ ℄p $ (pre( ) ! p) (' ^ CB (' ! EB ')) ! CVB ' [ ℄Kn ' $ (pre( ) ! Kn n [ 0 ℄')
q r s t
if ' and ' ! ; then if '; then Kn ' if ' ! ; then [ ℄' ! [ ℄ if : for all B there is a su h that: ! [ ℄'; and su h that n 0 implies ( ^ pre( )) ! EB ; then ! [ ℄CB '
0
0
f (?') f ( ; ) f ( [ ) f ( \ ) f ( ! ) f (LB )
A formula ' is dedu able, abbreviated as ` ', i there exists a nite sequen e of formulas su h that ea h formula is either an instantiation of one of the axioms a { p, or if it is obtained by applying one of the rules q { t to formulas that appear earlier in the sequen e. Theorem 25
(Soundness).
If ` ', then j= '.
The soundness of most of the axioms is easily seen. For m we use lemma 17. For rule t some more work needs to be done. For this we need the following lemma (based on [5℄). ^B : ℄ i Lemma 26 (witness path). [ M; w j= h iC [ there is a B su h that M; w j= C^B h i: ℄. 27. ` [L12 ?p℄C12 p p!p [L12 ?p℄p $ (p ! p) [L12 ?p℄p > ! [L12 ?p℄p
Example
1 2 3 4 5 6 7 8 9 10
>
a n a,q 1; 2 a,q 3 a r 5 r 5 a,q 6; 7 t 4; 8 q 5; 9
K1 > K2 > ((> ^ p) ! K1 >) ^ ((> ^ p) ! K2 >) > ! [L12 ?p℄C12 p [L12 ?p℄C12 p One might have expe ted a distribution axiom for [ ℄, but this is not sound. Su h an axiom is also unsound in the logi presented in [21℄, for the same reason: the interpretation of a tions are relations between states and sets of states. The modality [ ℄ orrespond to a 89 quanti er and distribution does not hold for that. We do have a weaker form of distribution in the form of rule s. This is all we need in the
ompleteness proof.
4.
COMPLETENESS The ompleteness proof is based on [5℄, [9℄, and [21℄. Spa e does not permit us to go into mu h detail. We generally follow the stru ture of the proof in [5℄. The main diÆ ulty in the proof is the truth lemma, whi h is proven by indu tion on formulas. We show that every formula is provably equivalent to a formula in a sublanguage of the full language. The indu tion follows the stru ture of the formulas in the sublanguage. We rst de ne the translation to the sublanguage. Definition 28
(Translation).
f (p) := p f (:') := :f (') f (' ^ ) := f (') ^ f ( ) f (Kn ') := Kn f (') f (CB ') := CB f (') f ([?'℄ ) := f (') ! f ( ) f ([ ; ℄ ) := f ([ ℄f ([ ℄ )) f ([ [ ℄ ) := f ([ ℄ ) ^ f ([ ℄ ) f ([ \ ℄ ) := f ([ ℄ ) _ f ([ ℄ ) f ([ ! ℄ ) := f ([ ℄ ) f ([LB ℄p) := fW(pre( )) ! p f ([LB ℄:') := 2T (LB ) :f ([ ℄') f ([LB ℄(' ^ )) := f ([LB ℄') ^ f ([LVB ℄ ) f ([LB ℄Kn ') := f (pre( )) ! Kn n LB f ([ ℄') f ([LB ℄CB ') := [LB f ( )℄CB f (') f ([LB ℄[ ℄') := f ([LB ℄f ([ ℄'))
Lemma
29.
`
:= := := := := :=
?f (') f ( ) ; f ( ) f ( ) [ f ( ) f ( ) \ f ( ) f ( ) ! f ( ) LB f ( )
f (') $ '
The sublanguage has the following stru ture. Lemma 30. Given a formula ' 2 LN , we have that f (') 2 f f LN , where LN is de ned by the following BNF: ! ::= p j :! j ! ^ ! j Kn ! j CB ! j [LB ℄CB !
where, if ! 0 o
urs in LB , it is also of the form ! 2 LfN . The next lemma shows we an apply indu tion on this sublanguage in the truth lemma. Lemma 31 (well-founded order). There is a wellfounded order < on the language LN with the following properties: (1) for any subformula of ', < ', (2) < is transitive, (3) f (') '. We an now start onstru ting the anoni al model. Be ause logi s with re exive transitive losure operators are generally not ompa t we need to onstru t a nite anoni al model for every formula. That means we only look at maximally onsistent sets with respe t to some nite set of senten es. This set of senten es is alled the losure. f Definition 32 (Closure). Let ! 2 LN . The losure f of ! is the minimal set C l(! ) LN su h that 1 ! 2 C l(! ) 2 If ! 0 2 C l(! ) and ! 00 is a subf. of ! 0 , then ! 00 2 C l(! ). 3 If ! 0 2 C l(! ) and ! 0 is not a negation, then :! 0 2 C l(! ) 4 If CB ! 0 2 C l(! ), then Kn CB ! 0 2 C l(! ), for all a 2 B . 5 If [ ℄CB ! 0 2 C l(! ), then for all and all n 2 B su h that n : Kn [ ℄CB ! 0 ; [ ℄! 0 2 C l(! ).
For any formula ! 2 LfN , the losure of ! is nite. We will often write for C l(! ). Now we only look at maximally
onsistent sets in . It is lear that any onsistent subset of
an be expanded to a maximally onsistent subset. Definition 33 ( - anoni al model). The - anoni al model is M = (W ; ; V ) where W
= f : is maximally - onsistent g
n i f! 0 2 j Kn ! 0 2 g = 0 0 f! 2 j Kn ! 2 g
V (p) = f : p 2 g Note that M is nite: it ontains at most 2j j elements. Moreover, note that it is a model in SB , where B is the group of agents that o
ur in ', be ause the a
essibility relations n are all equivalen e relations. To ensure that the truth lemma holds for senten es of the form [LB ℄CB ! we need the following de nition and lemma, whi h is also based on a similar de nition and lemma found in [5℄. Definition 34 (Good Path). A good path from 2 M for h iC^B is a path in M
= 0 n1 1 n2 nk k
su h that k 0, ni 2 N and there are a tions i su h that
= 0 n1 1 n2 nk k su h that h i i> 2 i (0 i k) and h k i 2 k . Lemma 35. Suppose [ ℄CB 2 . Then: there is a good path from 0 for h iC^B : , i h iC^B : 2 0 .
This ensures that the truth lemma holds. Lemma 36 (Truth Lemma). If 2 W , then for all
2 it holds that (M ; ) j= i 2 .
Completeness follows in the standard way from the truth lemma. Theorem 37 (Completeness). If 6` ', then there is a model (M; w) su h that (M; w) 6j= ' Proof. Suppose 6` '. Then, :' is onsistent. Take ! = f (:'). Note that :' and ! are provably equivalent (Lemma 29). Now, there is a maximally onsistent set in the losure
of ! su h that ! 2 . Be ause of the nite truth lemma we may on lude that (M ; ) j= ! , and therefore (Lemma 29), (M ; ) j= :' and thus (M ; ) 6j= '
5.
APPLICATIONS In various publi ations this language has been applied to des ribe the dynami s of on rete multiagent systems [26, 29, 28, 30℄. We merely give an overview of appli ation areas by examples, without mu h detail. Example 38
(Card game a tions).
Assume three players 1; 2; 3 and three ards a; b; . Ea h player is dealt one ard. Atom a1 represents the fa t where
ard a is held by player 1, et . The a tion where player 1 pi ks up his ard, so that the others annot see whi h ard it is, is des ribed by the a tion pi kup = L123 (L1 ?a1 [ L1 ?b1 [ L1 ?b1 )
In some state s where ea h player is dealt one ard and all players have pi ked up their ards (for details, see [29℄), player 1 puts his ard fa e up on the table. This is des ribed by the a tion table = L123 ?a1 [ L123 ?b1 [ L123 ? 1
Note that in a given epistemi state only one of these alternatives an be exe uted. Now in that same state s we an also exe ute two rather di erent a tions: rstly, player 1
an show his ard to player 2 without player 3 seeing whi h
ard is shown. This a tion is des ribed by show = L123 (L12 ?a1 [ L12 ?b1 [ L12 ? 1 )
Next, player 2 an ask player 1 \please whisper in my ear the name of a ard that you do not have," after whi h player 1 responds to 2's request. That a tion is des ribed by whisper = L123 (L12 ?:a1 [ L12 ?:b1 [ L12 ?: 1 )
In this ase, whatever the a tual state, 1 an hoose one of two ards to whisper (and indeed, the omplexity of the resulting epistemi state has now in reased).
Example 39 (Cluedo). The `murder game' Cluedo is a ard game where a tions as in the previous example an take pla e. Other typi al a tions in Cluedo are `ending your move' and `winning the game'. For a perfe t logi ian, ending a move in Cluedo is publi ly announ ing that you annot win the game yet. This is the a tion LN ?:winn , where winn is an epistemi formula des ribing knowledge of the `murder
ards', the ards `held by the table' (agent 0) so to speak, i.e. winn = Kn (s arlett0 ^ knife0 ^ kit hen0 ) _ Kn ::: (all murder
ards ombinations). Example 40
(Different ards).
Two players 1; 2 fa e three ards a; b; lying fa e-down in two sta ks on the table. Let a be the atom des ribing ` ard a is in the sta k with two ards', et . Some outsider hands player 1 one of the two-sta k ards and, `at the same time, with his other hand', player 2 the other (`di erent') ard. The a tion is des ribed by
[
di erent ards = L12 (
(L1 ?x \ L2 ?y ))
x6=y=a;b;
Example 41 (Muddy hildren). We assume familiarity with the `muddy hildren problem' [9℄. Publi announ ement of ' orresponds in LN to a knowledge a tion LN ?'. Suppose there are three hildren 1, 2, and 3. First `father' tells them that at least one of them is muddy. This is des ribed by L123 ?(m1 _ m2 _ m3 ) (where mi stand for ` hild i is muddy'). And then father tells them, that who knows whether (s)he is muddy may step forward. When nobody steps forward, that a tion noforward is generally [22, 11, 4℄ analysed as the publi announ ement of a onjun tion des ribing that none of the hildren knows whether he/she is muddy: L123 ?((:K1 m1 ^ :K1 :m1 ) ^ (:K2 m2 ^ :K2 :m2 ) ^ (:K3 m3 ^ :K3 :m3 )). We prefer an analysis where `nobody steps forward' is omposed of subprograms `1 does not step forward', `2 does not step forward' and `3 does not step forward': noforward = L123 ( L123 ?(:K1 m1 ^ :K1 :m1 )\ L123 ?(:K2 m2 ^ :K2 :m2 )\ L123 ?(:K3 m3 ^ :K3 :m3 ) ) Example 42 (Se urity proto ols). From a pa k of seven known ards (0; 1; 2; 3; 4; 5; 6) two players Anne (a) and Bill (b) ea h draw three ards and a third player Crow ( ) gets the remaining ard. How an Anne and Bill openly (publi ly) inform ea h other about their ards, without Crow learning from any of their ards who holds it? There are many solutions to this problem [30℄. Suppose Anne a tually holds f0,1,2g (012a ), Bill f3,4,5g, and Crow ard 6. One of the solutions onsists of Anne saying \My hand is one of 012; 034; 056; 135; 246" after whi h Bill says \Crow has
ard 6". This is des ribed by the sequen e of two publi announ ements Lab ?Ka (012a _ 034a _ 056a _ 135a _ 246a ) ; Lab ?Kb 6 Hereafter, it is ommon knowledge that Anne knows Bill's
ards, Bill knows Anne's ards, and Crow doesn't know any of Anne's or Bill's ards.
6. CONCLUSIONS We have presented a proof system, and proved it to be sound and omplete, for a dynami epistemi logi in whi h
higher-order information and belief hange, and even higherorder belief hange, an all be elegantly expressed. The
ru ial te hni al features of the language are, (1) that the notion of epistemi a
essibility is lifted from one between worlds of an epistemi state to one between more omplex semanti obje ts, su h as sets of states, (2) the notion of the group of models, states, and a tions, and (3) that a tions are interpreted as a relation between states and sets of states. In view of proving ompleteness, we introdu ed a useful notion of synta ti a
ess between a tions. We gave an overview of the wide range of appli ations of this language for on rete MAS spe i ation. We intend to ontinue this resear h by generalizing the semanti s to in lude (not just knowledge but also) belief.
7.
ACKNOWLEDGMENTS Wiebe van der Hoek has arried out part of this resear h while visiting the University of Otago on a William Evans Fellowship. Barteld Kooi has been arrying out this resear h with the assistan e of the Netherlands Organization for S ienti Resear h (NWO). 8. REFERENCES [1℄ C. Al hourron, P. Gardenfors, and D. Makinson. On the logi of theory hange: partial meet ontra tion and revision fun tions. Journal of Symboli Logi , 50:510{530, 1985. [2℄ R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logi . In Pro eedings of the [3℄ [4℄ [5℄ [6℄ [7℄ [8℄ [9℄ [10℄ [11℄ [12℄
38th IEEE Symposium on Foundations of Computer S ien e, pages 100{109, Florida, O tober 1997. R. Aumann and A. Brandenburger. Epistemi
onditions for Nash equilibrium. E onometri a, (63):1161{1180, 1995. A. Baltag. A logi for suspi ious players: Epistemi a tions and belief updates in games. Bulletin of E onomi Resear h, 54(1):1{45, 2002. A. Baltag, L. Moss, and S. Sole ki. The logi of publi announ ements, ommon knowledge and private suspi ions. Presented at TARK 98, a
epted for Annals of Pure and Applied Logi , 2002. S. Benferhat, D. Dubois, H. Prade, and M. Williams. A pra ti al approa h to revising prioritized knowledge bases. Studia Logi a, 70(1), 2002. P. Bla kburn, M. de Rijke, and Y. Venema. Modal Logi . Cambridge University Press, Cambridge, 2001. Cambridge Tra ts in Theoreti al Computer S ien e 53. A. Darwi he and J. Pearl. On the logi of iterated belief revision. Arti ial Intelligen e, 89(1-2):1{29, 1997. R. Fagin, J. Halpern, Y. Moses, and M. Vardi. Reasoning about Knowledge. MIT Press, Cambridge MA, 1995. J. Gerbrandy. Bisimulations on Planet Kripke. PhD thesis, University of Amsterdam, 1999. ILLC Dissertation Series DS-1999-01. J. Gerbrandy and W. Groeneveld. Reasoning about information hange. Journal of Logi , Language, and Information, 6:147{169, 1997. R. Goldblatt. Logi s of Time and Computation. CSLI Publi ations, Stanford, 2 edition, 1992. CSLI Le ture Notes No. 7.
[13℄ D. Harel, D. Kozen, and J. Tiuryn. Dynami Logi . MIT Press, Cambridge MA, 2000. Foundations of Computing Series. [14℄ J. Hintikka. Knowledge and Belief. Cornell University Press: Itha a, NY, 1962. [15℄ J. Hintikka. Reasoning about knowledge in philosophy. In J. Y. Halpern, editor, Pro eedings of TARK 1986, pages 63{80. Morgan Kaufmann: San Mateo, CA, 1986. [16℄ H. Katsuno and A. Mendelzon. On the di eren e between updating a knowledge base and revising it. In Pro eedings of KR '91, pages 387{394, 1991. [17℄ J.-J. Meyer and W. van der Hoek. Epistemi Logi for AI and Computer S ien e. Cambridge Tra ts in Theoreti al Computer S ien e 41. Cambridge University Press, Cambridge, 1995. [18℄ T. Meyer, W. Labus hagne, and J. Heidema. Re ned epistemi entren hment. Journal of Logi , Language and Information, 9:237{259, 2000. [19℄ R. Parikh. The logi of games and its appli ations. In M. Karpinski and J. van Leeuwen, editors, Topi s in the theory of omputation Annals of Dis rete Mathemati s 24, pages 111{139, Amsterdam, 1985. Elsevier S ien e. [20℄ M. Pauly. Logi for so ial software. PhD thesis, University of Amsterdam, 2001. ILLC Dissertation Series DS-2001-10. [21℄ D. Peleg. Con urrent dynami logi . Journal of the ACM, 34(2):450{479, 1987. [22℄ J. Plaza. Logi s of publi ommuni ations. In M. Emri h, M. Pfeifer, M. Hadzikadi , and Z. Ras, editors, Pro eedings of the 4th International Symposium on Methodologies for Intelligent Systems, pages 201{216, 1989. [23℄ B. ten Cate. Internalizing epistemi a tions. In M. Martinez, editor, Pro eedings of the NASSLLI-2002 student session, Stanford University, 2002. [24℄ J. van Benthem. Logi s for information update. In J. van Benthem, editor, Pro eedings of TARK VIII, pages 51{88, Los Altos, 2001. Morgan Kaufmann. [25℄ W. van der Hoek and M. Wooldridge. Tra table multi agent planning for epistemi goals. In C. Castelfran hi and W. Johnson, editors, Pro eedings of AAMAS, pages 1167{1174, New York, USA, 2002. ACM Press. [26℄ H. van Ditmars h. Knowledge games. PhD thesis, University of Groningen, 2000. ILLC Dissertation Series DS-2000-06. [27℄ H. van Ditmars h. The semanti s of on urrent knowledge a tions. In M. Pauly and G. Sandu, editors, ESSLLI 2001 workshop on Logi and Games, 2001. [28℄ H. van Ditmars h. The des ription of game a tions in
luedo. In L. Petrosian and V. Mazalov, editors, Game Theory and Appli ations, volume 8, pages 1{28, Comma k, NY, USA, 2002. Nova S ien e Publishers. [29℄ H. van Ditmars h. Des riptions of game a tions. Journal of Logi , Language and Information, 11:349{365, 2002. [30℄ H. van Ditmars h. The russian ards problem: a ase study in ryptography with publi announ ements. Te hni al report, Department of Computer S ien e, University of Otago, 2002. OUCS-2002-08.
