Dynamic Epistemic Logic (DEL) is an advanced variation of PAL; as the name PAL shows, it deals mainly with ‘public announcements,’
by which every agent shares the same information; however, the state of knowledge may be changed
not only by public announcements but also announcements to a specific group in a community.
A typical example is ‘private announcements,’ in which someone communicates something to only a single person (e.g., a personal
letter). An extension of PAL, DEL is a logic which can express not only public announcements,
but more delicate and complicated flows of information such as private announcement, and such
a factor that causes a change of knowledge state is called an action (or event) as a whole.
Technically, the notion of action a is defined with the action model which is almost the same as the Kripke model with a
finite domain. Interestingly or oddly, an action model differs from a Kripke model and belongs
to the syntax field of DEL.
| Let |
Agent := { a, b, c, a0, a1, a2, ... } be a countable set of agents,
|
|
Atom := { p, q, r, p0, p1, p2, ... } be a countable set of atomic formulas,
|
|
Evt := { e0, e1, e2, ... } be a countable set of actions (or sometimes called events),
|
An
(S5) action frame is a pair (S, ~) where S is a non-empty finite set of actions and ~
: Agent → S×S is a function which assigns an
equivalence relation on S to an agent.
The DEL-formula A and action model E = (S, ~, pre) are simultaneously defined as follows (p ∈
Atom, e ∈ Evt, a ∈ Agent):
A ::= p | ~A | (A -> A) | #aA | [(E,e)]A
where (S, ~) is an action frame, pre is a function which assigns a DEL-formula pre(b) to each action b ∈ S, and an expression
(E,e) is called a pointed action model.
#aA reads "agent a knows that A",
[(E,e)]A reads "after an action of (E,e), formula A holds".
Let E = (S, ~, pre). Then
Dom(E) := S, and Rel(E) := ~, and Pre(E) := pre.
Other logical connectives are defined in the usual way as follows:
- A & B := ~(A -> ~B)
- A v B := ~A -> B
- bot := p & ~p
- top := bot -> bot
- A <-> B := (A->B) & (B->A)
- $aA := ~#a~A
- <(E,e)>A := ~[(E,e)]~A
- &&(Rel(E)(a)(e,x))A) := A[x/e1] & A[x/e2] & ... & A[x/en]
where {e1, e2,..., en} = { x ∈ Dom(E) | (e,x) ∈ Rel(E)(a)}
and
A[x/y] means "x in A is substituted by y".
Note that ~, ->, &, v, <-> , top, bot, #a, $a and &&(Rel(E)(a)(e,x)) are usually denoted
by \(\neg\), \(\to\), \(\wedge\), \(\vee\), \(\leftrightarrow\), \(\top\), \(\bot\), \(\Box_a\)
(or \(K_a\)), \(\Diamond_a\) (or \(\hat{K}_a\)),
and \(\bigwedge\limits_{e\sim^E_ax}\) respectively.
For readability of a formula, the following notations are also usable:
- #A := #aA
- $A := $aA
- knows(a,A) := #aA
- knows_if(a,A) := #aA v ~#aA
