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 nonempty finite set of actions and ~
: Agent → S×S is a function which assigns an
equivalence relation on S to an agent.
The DELformula 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 DELformula 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