General Dynamic Dynamic Logic
Patrick Girard Jeremy Seligman
Department of Philosophy
University of Auckland

Fenrong Liu
Department of Philosophy
Tsinghua University

Abstract
Dynamic epistemic logic (DEL) extends purely modal epistemic logic (S5) by adding
dynamic operators that change the model structure. Propositional dynamic logic(PDL) extends basic modal logic with programs that allow the definition of complex
modalities. We provide a common generalisation: a logic that is ‘dynamic’ in bothsenses, and one that is not limited to S5 as its modal base. It also incorporates,and significantly generalises, all the features of existing extensions of DEL such as
BMS [3] and LCC [21]. Our dynamic operators work in two steps. First, they provide
a multiplicity of transformations of the original model, one for each ‘action’ in apurely syntactic ‘action structure’ (in the style of BMS). Second, they specify how
to combine these multiple copies to produce a new model. In each step, we use thegenerality of PDL to specify the transformations. The main technical contributionof the paper is to provide an axiomatisation of this ‘general dynamic dynamic logic’(GDDL). This is done by providing a computable translation of GDDL formulas toequivalent PDL formulas, thus reducing the logic to PDL, which is decidable. The
proof involves switching between representing programs as terms and as automata.
We also show that both BMS and LCC are special cases of GDDL, and that there areinteresting applications that require the additional generality of GDDL, namely themodelling of private belief update. More recent extensions and variations of BMS and
LCC are also discussed.
Keywords: Dynamic logic, BMS, LCC, PDL, belief change.

Recent research in epistemic logic extends the classical S5-analysis of knowledge
with dynamic operators that model the epistemically relevant changes brought
about by various acts of communication. These are represented as extensionsof the basic epistemic language with expression of the form [a]ϕ interpreted
as ‘after action a is performed, ϕ is the case’. The primary example of suchan action is the ‘public announcement’ of a proposition ψ, written !ψ, which
achieves the right effect by simply removing the ¬ϕ-states (those states of the240

General Dynamic Dynamic Logic

model in which ψ is false), so that everyone subsequently knows that these
possibilities are no longer open. 1 A rich array of dynamic operators havebeen introduced to deal with private communications of various sorts, and also
actions that affect more than just the epistemic states of agents, the so-called‘real world changes’. 2
Meanwhile, interest has grown in applying similar techniques to other branchesof modal logic, such as doxastic logic (the logic of belief) [4,18] and preference
logic [7,11,12,20]. A significant difference from the epistemic setting is theneed to describe dynamic operators that change the relational structure of theunderlying model, not just the size of its domain (announcement) or the propositional valuations (real-world change). For example, if one models the doxastic
state of an agent by a plausibility relation between epistemically possible state,‘upgrading’ a proposition ϕ, so that it is believed, may be modelled by an operator that transforms the plausibility relation by removing links from ϕ-statesto ¬ϕ-states and adding links from ¬ϕ-states to ϕ-states. This ensures thatevery possible state in which ϕ is true becomes more plausible (for the given
agent) than every possibility in which ϕ is false. Currently, however, there is
no way of adapting the technology of BMS to model the doxastic effect on amultiplicity of agents of one or more of those agents privately upgrading theirbeliefs as a response to a less-than-public communication.
We solve this problem by providing a more general framework, inspired by
Theorem 4.11 in [12], first noted in [20], which states that any dynamic operator
whose effect on a model can be described in PDL (without Kleene’s iteration
operator ∗) can be reduced to the underlying modal logic using essentially only
the standard axioms of PDL. We show how this idea can be used to extend
BMS (and LCC), so that a vast range of dynamic operators can be modelled ina way that allows for private changes and real-world changes in epistemic logic,
doxastic logic, preference logic, and any other normal modal logic. 3 We also
extend it by adding the Kleene star, so that certain desirable frame conditions(such as transitivity) can be imposed. 4
Section 1 introduces the concept of a ‘PDL-transformation’, which is a general
1 Notoriously, it is not guaranteed that the announced proposition is subsequently known
because its very announcement may change its truth value, e.g. announcing ‘the sun isshining but you don’t know it’ results in your knowing that the sun is shining and so making
the announcement false.
2 See for example, the textbooks [23] and [19]. The initial paper on public announcement
was [15] and the most significant advance came with the eponymously acronymed BMS [3].
A recent extension of BMS, incorporating real-world changes, is LCC [21], the ‘Logic ofCommunication and Change’.
3 In particular, we can have dynamic operators over epistemic logics weaker than S5, socatering for those who wish to avoid the controversial properties of positive or negative
introspection.
4 There are various ways in which the Kleene star can be used in dynamics. Our sense
will become clear but, for example, it is not the sense of [13], which is known to give an
undecidable logic.

Girard, Seligman and Liu

241

way of changing models using PDL terms. These transformation are used extensively in Section 2, in which GDDL is defined semantically and then axiomatised,using a technique that exploits the possibility of representing programs bothby PDL-terms and by finite state automata. We illustrate GDDL by showing
how it can be used to model private belief change. Finally, Section 3 shows
how BMS and LCC are special cases of GDDL, and then goes on to discuss otherrecent variations and extensions such as [2,9,10,22,24].

1

Preliminaries

A Kripke signature is a pair hP, Ri of sets of symbols. The elements of P arepropositional variables and those of R are relation symbols. A model of thissignature, M = hW, V i consists of a set W (of states) and a valuation function
V mapping each p ∈ P to V (p) ⊆ W and each r ∈ R to V (r) ⊆ W 2 . To
describe such structures, we define T (P, R) to be the set of programs π andL(P, R) to be the set of formulas ϕ in the usual way:
π ::=
ϕ ::=

r | E | ϕ? | (π; π) | (π ∪ π) | π ∗p | ¬ϕ | (ϕ ∨ ϕ) | hπiϕwhere r ∈ R and p ∈ P . Here, E, is the universal program that jumps between
arbitrary states. In each model M , semantic values [[ϕ]]M ⊆ W and [[π]]M ⊆ W 2
are given by:[[p]]M[[¬ϕ]]M[[(ϕ ∧ ψ)]]M[[hπiϕ]]M= V (p)= W \ [[ϕ]]M= [[ϕ]]M ∩ [[ψ]]M= {u ∈ W | u[[π]]M v and v ∈ [[ϕ]]M , for some v ∈ W }[[r]]M[[E]]M[[ϕ?]]M[[π1 ; π2 ]]M[[π1 ∪ π2 ]]M

=
=
=
=
=

[[π ∗ ]]M

=

V (r)
W2
{hu, ui | u ∈ [[ϕ]]M }{hu, vi | u[[π1 ]]M w and w[[π2 ]]M v, for some w ∈ W }[[π1 ]]M ∪ [[π2 ]]M{hu, vi|u = v or ui [[π]]M ui+1 for some n ≥ 0, u0 , . . . , un ∈ Wsuch that u0 = u and un = v}

As usual, we also write u[[π]]M v for hu, vi ∈ [[π]]M and M, u |= ϕ for u ∈ [[ϕ]]M .
PDL-transformations We will use expressions from our language to describechanges to models. Given a model M of signature hP, Ri, we will show how
to obtain a model ΛM of a possibly different signature hQ, Si in such a waythat we retain some control over which formulas are satisfied in the new model.
Specifically, we will also define a (computable) translation ϕΛ of each formulaϕ ∈ L(Q, S) such thatM, u |= ϕΛ iff ΛM, u |= ϕ

242

General Dynamic Dynamic Logic

This is the content of Lemma 1.1, below. Specifically, we say that a PDLtransformation Λ from signature hP, Ri to signature hQ, Si consists of(i) a formula |Λ| ∈ L(P, R),(ii) an algorithm 5 for calculating Λ(q) ∈ L(P, R) for each q ∈ Q and(iii) an algorithm for calculating a term Λ(s) ∈ T (P, R) for each s ∈ S.
Now, given a model M = hW, Ri of signature hP, Ri, we define the model ΛMof signature hQ, Si to be hΛW, ΛV i, whereΛWΛV (q)
ΛV (s)= [[|Λ|]]M= [[Λ(q)]]M ∩ ΛW for each q ∈ Q= [[Λ(s)]]M ∩ ΛW 2 for each s ∈ S

In other words, the domain of the new model is simply a restriction of thedomain of the old model (defined by |Λ|) and the interpretation of the symbolsof hQ, Si are given by evaluating the corresponding PDL-expressions provided
by Λ, and then restricting them to the new domain.
For the translation, we can inductively compute formulas ϕΛ and terms π Λ ofsignature hP, Ri from each formula ϕ and term π of signature hQ, Si, as follows:qΛ(¬ϕ)Λ
(ϕ ∧ ψ)Λ
(hπiϕ)Λ

= Λ(q)= ¬ϕΛ= (ϕΛ ∧ ψ Λ )= hπ Λ iϕΛ

sΛ
EΛ
(ϕ?)Λ
(π1 ; π2 )Λ
(π1 ∪ π2 )Λ
(π ∗ )Λ

= Λ(s); |Λ|?
= E; |Λ|?
= (ϕΛ )?
= π1Λ ; π2Λ= π1Λ ∪ π2Λ
= (π Λ )∗Most of the clauses in this definition are fairly obviously what is required. Note,however, the role of formula |Λ|, which acts as a restriction on the quantifier
hπi in sΛ , as can be seen by expanding the semantic definition of hsΛ iϕ, sinceM, u |= hsΛ iϕiff∃v : M, v |= |Λ|, u[[sΛ ]]M v & M, v |= ϕ.

As remarked above, the definition is designed precisely so that the following
result holds:
Lemma 1.1 For each state u of ΛM and v of M , and for each formula ϕ ∈L(Q, S),M, u |= ϕΛ iff ΛM, u |= ϕ, andu[[π Λ ]]M v
iff v ∈ ΛW and u[[π]]ΛM v.
5 We refer to ‘algorithms’ here in an informal way, which could be made precise, but doing
so would require us to be boringly pedantic about the way the symbols of the signature,for example, are presented, and to choose arbitrarily between many equally good ways ofrepresenting these algorithms. Besides, in most cases of interest, the signature hQ, Si isfinite, and in this case, it is enough merely to list the various components of Λ.

Girard, Seligman and Liu

243,

Proof: See Appendix.

Example Let P = {p1 , p2 }, R = {r1 , r2 }, Q = {q1 , q2 }, and S = {s}. Let Λ
be the transformation from hP, Ri to hQ, Si given by|Λ| = hr1 ip1 ∨ hr2 ip2
Λ(q1 ) = hr2 i¬p1 and Λ(q2 ) = hp2 ?; r1 i¬p2
Λ(s) = (r1 ; r2 ) ∪ (p1 ?; r2 )Then with model M as shown below, we get ΛM as follows:
r2
p1

M

r2

r1

a
s

q1

p2

;

r1
r2

ΛM

q1 , q2s

As a simple example of Lemma 1.1 in action, let ϕ be the formula hsi(q1 ∧ q2 ).
Then ϕΛ is h((r1 ; r2 ) ∪ (p1 ?; r2 )); (hr1 ip1 ∨ hr2 ip2 )?i(hr2 i¬p1 ∧ hp2 ?; r1 i¬p2 ). A
bit of checking will confirm that [[ϕ]]ΛM and [[ϕΛ ]]M are both equal to the setof states depicted in the left columns of these diagrams.
In what follows we will use a concise notation for PDL transformations, which
we illustrate by rewriting Λ, from the above example, ash|hr1 ip1 ∨ hr2 ip2 |, q1 := hr2 i¬p1 , q2 := hp2 ?; r1 i¬p2 , s := (r1 ; r2 ) ∪ (p1 ?; r2 )i
To simplify notation further, we will omit trivial domain restriction (>) andthose parts of a PDL-transformation that do not change anything. For example, the action of ‘public announcement of ϕ’ is just h|ϕ|i. Finally, the identity
transformation is written as I. Some PDL-transformations found in the literature [12,18,20,26] are listed below:2

Add ¬p → p links=

hr := (r ∪ (¬p?; E; p?))∗ i(∗ used to preserve transitivity)

Delete p → ¬p links(‘suggestion’ )=hr := ((¬p?; r; ¬p?) ∪ (p?; r; p?)∪(¬p?; r; p?)i

Delete p → ¬p links
Add ¬p → p links(‘radical upgrade’ )=hr := ((¬p?; r; ¬p?) ∪ (p?; r; p?)∪(¬p?; E; p?)i

General Dynamic Dynamics

Given a signature hP, Ri, we will define a class of dynamic operators to add to
PDL to produce our dynamic dynamic logic, GDDL. Just as with the ‘action

244

General Dynamic Dynamic Logic

structures’ of BMS, we think of these operators as syntactic objects, albeit
somewhat complex ones. A GDDL dynamic operator [A, G, H, a] consists offour components:(i) a finite structure A = hD, U i of some finite signature hQ, Si (distinct fromhP, Ri), whose nodes d ∈ D are called program nodes,(ii) a PDL-transformation Gd from hP, Ri to hP, Ri for each d ∈ D,(iii) a PDL-transformation H from hP ∪ Q, R ∪ Si to hP, Ri, and(iv) a distinguished element a ∈ D.
We can represent the dynamic operator [A, G, H, a] in the following diagrammatic style:
q
Ga

s

Gb

H
The upper section contains a representation of the structure A, with each nodecontaining its associated PDL-transformation. Relations U (s) are indicatedby arrows labelled with ‘s’, a symbol of S, and U (q) is shown by labelling
nodes with ‘q’ from Q. (The above labels and arrows are merely illustrative.)
The distinguished node a is highlighted with darker edges. The lower section
contains the PDL-transformation H.
The language of GDDL is given by:
π ::=
ϕ ::=

r | E | ϕ? | (π; π) | (π ∪ π) | π ∗p | ¬ϕ | (ϕ ∨ ϕ) | hπiϕ | [A, G, H, a]ϕwhere, again, r ∈ R, p ∈ P , and [A, G, H, a] is a GDDL dynamic operator. Let
T + (P, R) and L+ (P, R) be the set of GDDL terms and formulas so defined.
Notice, in particular, how the two senses in which the language is ‘dynamic’are captured by hπi and [A, G, H, a]. L(P, R) is already dynamic in the first
sense but not in the second.
We think of each element d of D as representing a possible action whose effecton M is to transform it to Gd M . This could be an announcement, a belief
or preference change, or something far more complex, depending on the application. The particular element a is the one that actually occurs. The only
restriction is that the transformation is definable by PDL expressions. 6
6

In BMS elements of action structures are associated with formulas, called ‘pre-conditions’
which act to restrict the domain but which have no effect on the relational structure of theGirard, Seligman and Liu

245

We represent the interaction between A = hD, U i and M = hW, V i by constructing the model GM = hGW, GV i of combined signature hP ∪ Q, R ∪ Si,
as follows:
GW = {hu, di | u ∈ [[|Gd |]]M }Then, for hu, di and hv, ei in GW :hu, di ∈ GV (p)hu, di ∈ GV (q)hu, di GV (r) hv, eihu, di GV (s) hv, ei

iff u ∈ [[p]]Gd M
iff d ∈ U (q)iff d = e and u [[r]]Gd M v
iff u = v and d U (s) e

for each p ∈ P
for each q ∈ Q
for each r ∈ R
for each s ∈ S

We can think of GM as resulting from the process of replacing each program
node d ∈ D by the transformed model Gd M that results from applying the PDLtransformation Gd to M . The structure of A remains, linking these transformedmodels together. 7
Finally, we use the transformation H to recover a model of signature hP, Ri
from GM , defining[A, G, H]M=

HGM

H encodes the way in which the structure of A coordinates the different programs represented by the elements of D. Again, there is great generality here.
All that is required is that this means of coordination is, in some sense, PDLdefinable. 8 Then, we can specify the semantics for our new dynamic operators
in a standard way: 9
M, u |= [A, G, H, a]ϕiff[A, G, H]M, hu, ai |= ϕBecause of the generality of the approach, it is useful to consider the special casein which a GDDL-operator [A, G, H, a] is defined by a single PDL-transformation
Λ, defining

model. See Section 3 for details.
7 Another useful metaphor for visualising GM is that it is a two-dimensional model in which
the S links run in a horizontal direction and the R links run in a vertical direction. Whereas
the S links are merely copies of their projection on to D, the R links vary. In the dth placein the horizontal direction the vertical R links form a copy of those in Gd M .
8 In BMS, the coordination is built into the details of the model construction, not a parameterof the dynamic operators. Also, the signature used for A can be taken to be the same asthat for M , since both are simply families of equivalence relations. Again, see Section 3 fordetails.
9 Although a is not relevant to computing [A, G, H]M , we define [A, G, H, a]M =[A, G, H]M , for uniformity of notation when we consider arbitrary operators.

246

General Dynamic Dynamic Logic

Λ

[Λ] =
I
Example 2: For a purely abstract example, illustrating various aspects of thedefinition, take Λ to be the PDL-transformationh|hr1 ip1 ∨ hr2 ip2 |, p1 := hr2 i¬p1 , p2 := hp2 ?; r1 i¬p2 , r2 := (r1 ; r2 ) ∪ (p1 ?; r2 )iTake the model M of example 1 (shown left) and the dynamic operator[A, G, H, a] (shown right):
r2
p1

r2

r1

s

Λ

I

p2
r1

|(p1 ∨ p2 )|, r1 := (s; r2 )∗ ,r2 := r2 ∪ (p1 ?; >; (p1 ∧ p2 )?)r2

We first compute GM , then HGM :

p1

GM
r1

r2

s

s

p1 , p2

p1

r2

r2
r2

p2

r1

r1
r2

s
r1
r1

HGM
p1

2.1

r1

r1 , r2
r2

p1 , p2

r1 , r2

r1
r2

p1

r2

p2

Private Belief Change

As an example of what can be done with GDDL, and a concrete illustrationof the definitions in action, we will consider an application to doxastic logic.
For the basic logic of belief change, we follow van Benthem’s [18] account, inwhich the effect of a belief update is to change an agent’s judgements aboutGirard, Seligman and Liu

247

the relative plausibility (≤) of different epistemic possibilities. The basic idea
is that when updating with p, an agent should judge any p-state to be strictly
more plausible than any ¬p-state, while retaining her earlier judgements about
relative plausibility among p-states and among ¬p-states. Belief is defined astruth in maximally plausible states. We extend this to a multi-agent context inwhich belief changes are private. There are many options here, but we choose
to add a separate relation (∼) modelling knowledge (epistemic indistinguishability). In this example, we will assume that it is an equivalence relation, as is
standard, but it should be clear that many variations are possible within thepresent framework.
Given a finite sets of agents I, consider a Kripke signature hP, Ri with R ={∼i , ≤i , βi | i ∈ I}, the class D of models M = hW, V i of this signature forwhich, for each agent i, V (∼i ) is a equivalence relation, V (≤i ) ⊆ V (∼i ) is apreorder, anduβi v iff u ∼i v and w ≤i v for each w ∈ W such that v ≤i w.
In other words, a state v is βi -accessible from u iff it is maximally plausible
among those states that are epistemically indistinguishable from u. In this way,
the formula [βi ]ϕ states that ϕ is believed by i, according to the analysis of[18]. 10 Updating agent i’s beliefs with ϕ results in a new plausibility relation
defined by 11 (ϕ?; ≤i ; ϕ?) ∪ (¬ϕ?; ≤i ; ¬ϕ?) ∪ (¬ϕ?; ∼i ; ϕ?).
The PDL-transformation ⇑i ϕ (‘update i’s beliefs with ϕ’) maps ≤i to this PDL
term, keeping everything else the same. The fact that agent i believes ψ after
upgrading her beliefs with ϕ should then expressed in GDDL as [⇑i ϕ][βi ]ψ.
But there is a problem. Not only is [⇑i p][βi ]p valid (as expected), but so too
is [⇑i p][βj ][βi ]p, for any other agent j. In other words, it is logically true thatafter i doxastically updates with p, not only does she believe that p but everyone
else believes that she believes p. In this way, [⇑i ϕ] is not really private at all.
This situation is familiar from BMS, and we adopt a similar solution, but one
that exploits the relation-change potential of PDL-transformations, defining theoperator (↑i ϕ) = [A, G, H, a] as follows:
j

⇑i ϕ

j
I

a

for all j 6= ib∗∼j := (∼j ∪ j )≤j := (≤j ∪ j )∗10 Note that although β is in some sense redundant, in that it is fully determined by ∼ andii≤i , the operator [βi ] is not modally definable from the operators [∼i ] and [≤i ]; nonetheless,the relationship between the three operators can easily be acclimatised.
11 This differs slightly from [18] because of the restriction to the ∼ -equivalence class discussed
iabove.

248

General Dynamic Dynamic Logic

Here, A is a two-state structure with domain D = {a, b}. It has signature hQ, Si, where Q is empty and S = {j , j | j ∈ I}, and interpretsj as an equivalence relation and j as a preorder, although not all of thelinks are shown in the diagram. The distinguished node a contains the PDLtransformation ⇑i ϕ, representing the action of updating i’s belief’s with ϕ,and the other node, b, contains the identity transformation I, representing theaction of doing nothing. Only agent i knows which of the two possible actions
were performed, so a j b for all j 6= i. Likewise, we will assume (although
there is room for more subtlety here) that each of these other agents regards it
as more plausible that i’s beliefs have not changed. This is captured by making
a j b and not b j a for all those j. Finally, the integrating transformation
H is defined by taking the (reflexive, transitive closure of) the unions of thetwo epistemic and the two doxastic relations.
To see how this works, we will consider an application of (↑i ϕ) to the model
M displayed below: 12≤1 , ≤2∼1 , ∼2ru

β1 , β2
¬r

r

v

u

β1 , β2¬rv

We will think of M as representing a scenario with two agents, called 1 and 2,
who both falsely believe ¬r: ‘it hasn’t rained today’. Now, the operator ↑1 r
should represent the action of agent 1 privately upgrading her belief in r, in a
way that is unobserved by agent 2; perhaps she takes a furtive glance out of
the window and sees someone closing an umbrella. The resulting model (↑1 r)
is shown below (with βi displayed separately):≤2hu, air∼1 , ∼2

β1¬rhv, ai

r

β1

¬r

≤1
2

2

2

r
hu, bi∼1 , ∼2≤1 , ≤2

¬r

β2

2

r

β1 , β2

β2¬rhv, biβ1 , β212 Throughout this section reflexive loops and compositions of arrows for ∼ and ≤ are suppressed in diagrams, and the relations β1 and β2 , which are defined in terms of the others,
are shown separately.

Girard, Seligman and Liu

249

Here, the designated state satisfies [β1 ]r (agent 1 believes it to be raining),[β2 ]¬r (agent 2 still believes it is not raining) and [β2 ][β1 ]¬r (agent 2 also
believes, falsely, that agent 1 still believes it not to be raining). 13
2.2

Axiomatisation

The key to understanding the logic of GDDL is to find a computable translation
ϕ[A,G,H,a] of each formula ϕ in L(P, R) such that
[A, G, H, a]ϕ ↔ ϕ[A,G,H,a]is valid as a formula of GDDL. From this (and the replacement of logicalequivalents) it follows that every formula of L+ (P, R) is equivalent to a formulaof L(P, R), and can be proved to be so using these equivalences as axioms. We
can reduce the two senses of ‘dynamic’ in dynamic dynamic logic to one.
How, then, to define ϕ[A,G,H,a] ? Our approach will be to define a formula
ϕ[A,G,d] of L(P, R) for each ϕ of L(P ∪ Q, R ∪ S) and a program π [A,G,d,e] ofT (P, R) for each π of T (P ∪ Q, R ∪ S) such that for any model M of signature
hP, Ri, the following result holds:
Lemma 2.1 For each hu, di, hv, ei ∈ GW ,(i) GM, hu, di |= ϕ iff M, u |= ϕ[A,G,d] , and(ii) hu, di[[π]]GM hv, ei iff u[[π [A,G,d,e] ]]M v
This will be proved below. We can then define ϕ[A,G,H,d] = ϕH

[A,G,d]so that

Lemma 2.2 For each operator [A, G, H, a] of GDDL and each formula ϕ ofL(P, R), the following is valid:[A, G, H, a]ϕ ↔ ϕ[A,G,H,a]
Proof: From Lemmas 2.1 and 1.1. (Note that, since GM is of signature hP ∪Q, R ∪ Si and [A, G, H, d]M = HGM is of signature hP, Ri, the formula ϕH isin L(P ∪ Q, R ∪ S), as required by Lemma 2.1.),

To define π [A,G,d,e] we need a small excursion into automata theory. 14 For
13 Although the definition of a private belief update operator is only an example to showwhat can be done in GDDL, it illustrates the need for some constraints in getting sensible
results for epistemic logic. In particular, it is important that the epistemic relation i in
the operator constrains the definition of the various transformations Gd so that each agent
knows that actions affecting her own psychological state have occurred, namely, that d i e
implies both Gd (i ) = Ge (i ) and Gd (≤i ) = Ge (≤i ).
14 This excursion into automata theory is solely for the purpose of producing the reduction
axioms, in a recursive way. Once the axioms are produced, however, no essential use of
automata remains in the logic. We find the technique useful and illuminating but recognisethat there may be an alternative approach that provides reduction axioms in a more direct
way. We leave this as an open problem.

250

General Dynamic Dynamic Logic

each signature, say that σ is a basic program of that signature if it is either
a relation symbol, E, or a test. Then for each model N and a program π,
define Σ(N, u, v, π) to be the set of strings σ1 . . . σn of basic subprograms of πsuch that ui [[σi ]]N ui+1 for some sequence u0 , . . . , un of states in N with u0 = u
and un = v. Say that a finite state automaton A over an alphabet of basic
subprograms of a program π represents π iff for all models N and states u andv,
u[[π]]N v iff some word of Σ(N, u, v, π) is accepted by A.
It has been well known since [16] that every PDL program is represented by some
automaton and every automaton represents some PDL program. 15 Moreover,each can be computed from the other. 16 Now, given ϕ in L(P ∪ Q, R ∪ S) andπ in T (P ∪ Q, R ∪ S) and states d, e ∈ D, we will define ϕ[A,G,d] and π [A,G,d,e]
by mutual induction.
The definition of ϕ[A,G,d] is straightforwardly inductive:
p[A,G,d]q[A,G,d][A,G,d](¬ϕ)[A,G,d](ϕ ∧ ψ)[A,G,d](hπiϕ)=G d (p)> if d ∈ U (q)=⊥ otherwise= ¬ϕ[A,G,d]= (ϕ[A,G,d] ∧ ψ [A,G,d] )W= e∈D hπ [A,G,d,e] i(|Ge | ∧ ϕ[A,G,e] )The program π [A,G,d,e] is obtained by constructing a corresponding automaton, which will refer to ψ [A,G,d] for subprograms ψ? of π, which is inductively
legitimate. This will take the next couple of paragraphs.
First, consider an automaton Aπ which represents π. Let Aπ have states X, ofwhich X0 ⊆ X are initial states, X1 ⊆ X are accepting states, and for each σ(a basic subprogram of π), T (σ) ⊆ X 2 is such that there is a transition fromx1 to x2 labelled by σ iff hx1 , x2 i ∈ T (σ).
Now for each symbol σ in the alphabet of Aπ (a basic subprogram of π) andeach c1 , c2 ∈ D, define σ c1 ,c2 as follows:ψ [A,G,c] ?
if σ = ψ? and c1 = c2 = cif σ ∈ R and c1 = c2 = c
 Gc (σ)σ c1 ,c2 = |Gc1 |?; E; |Gc2 |? if σ = Eif σ ∈ S and hc1 , c2 i ∈ U (σ)
 >?


⊥?
otherwise
15 The representation depends only on the compositional structure of the program not on
the particular choice of basic programs, so additions to PDL such as tests and E are not a
problem.
16 The complexity of translating between the two representations has been investigated in[8].

Girard, Seligman and Liu

251

Construct a new automaton Bπd,e , whose alphabet consists of the basic programs
σ c1 ,c2 where σ is in the alphabet of Aπ , with states X 0 = X × D, initial states
X00 = X0 × {d}, accepting states X10 = X1 × {e}, and transition function T 0
defined by
T 0 (τ )={hhx1 , c1 i, hx2 , c2 ii | for some σ, hx1 , x2 i ∈ T (σ) and σ c1 ,c2 = τ }Now, let π [A,G,d,e] be the program of T (P, R) represented by Bπd,e .
The two automata are designed to be synchronised in the sense given by thefollowing technical lemma:
Lemma 2.3 Assume that for each test ψ? occurring in π, and each hw, ci ∈GW , GM, hw, ci |= ψ iff M, w |= ψ [A,G,c] . Then, given x1 , x2 ∈ X andhu, c1 i, hv, c2 i ∈ GW , consider the following properties of the labels of the automata Aπ and Bπd,e :γ(σ) :

hx1 , x2 i ∈ T (σ)
andhu, c1 i[[σ]]GM hv, c2 i

γ 0 (τ ) : hhx1 , c1 i, hx2 , c2 ii ∈ T 0 (τ )andu[[τ ]]M v

Then for each symbol τ of the alphabet of Bπd,e ,γ 0 (τ ) iff γ(σ) and σ c1 ,c2 = τ for some σ in the alphabet of Aπ
Proof: See Appendix.
We are now ready to prove Lemma 2.1.

,

Proof of Lemma 2.1: The rank of a formula or program is defined as follows.
Formulas of rank n are not of rank n − 1 but contain no programs of rankn, and programs of rank n not of rank n − 1 but contain no test formulas ofrank n. (In particular, formulas of rank 0 contain no programs and programsof rank 0 contain no test formulas; formulas of rank 1 contain at least one
program of rank 0 but none of rank 1 and programs of rank 1 contain at least
one test formula of rank 0 but none of rank 1, etc.) To prove the lemma weshow, by induction on the rank n of a formula ϕ of L(P ∪ Q, R ∪ S), that forhu, di, hv, ei ∈ W 0 ,(i) GM, u, d |= ϕ iff M, u |= ϕ[A,G,d] , and(ii) for any program π of rank ≤ n, hu, di[[π]]GM hv, ei iff u[[π [A,G,d,e] ]]M v
We prove part 1 by induction on the structure of ϕ.
For propositional variables:
GM, u, d |= p iff u ∈ Vd (p) iff u ∈ [[Gd (p)]]M iff M, u |= Gd (p) iff M, u |=p[A,G,d]GM, u, d |= q iff d ∈ U (q) iff q [A,G,d] = > iff M, u |= q [A,G,d] (given thatq [A,G,d] ∈ {>, ⊥})252

General Dynamic Dynamic Logic

For Booleans (¬ and ∧), the proof is straightforwardly inductive.
For formulas of the form hπiψ, note that π must be of rank < n and so foreach hw, f i ∈ W 0
hu, di[[π]]GM hw, f i iff u[[π [A,G,d,f ] ]]M v
and by the (inner, structural) inductive hypothesis,
GM, w, f |= ψ iff M, w, |= ψ [A,G,f ]But then the following are equivalent:
GM, u, d |= hπiψ
hu, di[[π]]GM hw, f i and GM, w, f |= ψ for some hw, f i ∈ W 0u[[π [A,G,d,f ] ]]M w and M, w, |= ψ [A,G,f ] for some hw, f i ∈ W 0
M, w |= W|Gf |, u[[π [A,G,d,f ] ]]M w and M, w, |= ψ [A,G,f ] for some f ∈ D, w ∈ W
M, u |= f ∈D hπ [A,G,d,f ] i(|Gf | ∧ ψ [A,G,f ] )[A,G,d]M, u |= hπiψFor part 2, we know that any test formula in π is of rank < n. So suppose
hu, di[[π]]GM hv, ei. Then by choice of Aπ we have that some word σ1 . . . σn inΣ(GM, hu, di, hv, ei, π) is accepted by Aπ . This implies that(i) there are u0 , . . . , un and c0 , . . . , cn ∈ D such that u0 = u, c0 = d, un = v
cn = e and hui , ci i[[σi ]]GM hui+1 , ci+1 i for 0 ≤ i < n, and(ii) there are x0 , . . . , xn ∈ X and such that x0 ∈ X0 , xn ∈ X1 , and hxi , xi+1 i ∈T (σi ) for 0 ≤ i < n.
Now for each i we have γi (σi ):hxi , xi+1 i ∈ T (σi )andhui , ci i[[σi ]]GM hui+1 , ci+1 i

c ,cSo, by Lemma 2.3, for τi = σi i i+1 , we have γi0 (τi ):hhxi , ci i, hxi+1 , ci+1 ii ∈ T 0 (τi )andui [[τi ]]M ui+1

Also, since c0 = d, cn = e, x0 ∈ X0 , xn ∈ X1 , we have that hx0 , c0 i ∈ X00 and
hxn , cn i ∈ X10 . Thus:(i) there are u0 , . . . , un such that u0 = u, un = v and ui [[τi ]]M ui+1 for 0 ≤i < n, and(ii) there are x0 , . . . , xn ∈ X and c0 , . . . , cn ∈ D such that hx0 , c0 i ∈ X0 ,hxn , cn i ∈ X1 , and hhxi , ci i, hxi+1 , ci+1 ii ∈ T 0 (τi ) for 0 ≤ i < n.
This is precisely what is required for τ1 . . . τn to be accepted by Bπd,e . Then bydefinition of π [A,G,d,e] , we have that u[[π [A,G,d,e] ]]M v, as required. The converse
is proved similarly.
,Girard, Seligman and Liu

253

Theorem 2.4 The logic of GDDL is completely axiomatised by the axioms andrules of PDL (see Definition 4.78 in [5]) and the schema` [A, G, H, a]ϕ ↔ ϕ[A,G,H,a]
Corollary 2.5 GDDL is decidable.
Proof: We have a computable reduction of GDDL to its PDL fragment, which
is itself decidable.
,

3

Applications

In the remainder of the paper, we show how two well-known systems for dynamic epistemic logic (BMS and LCC) are special cases of GDDL and makefurther connections to more recent developments.
3.1

BMS

For BMS [3], we will be working with a signature hP, Ri for which P is a(countably infinite) set of propositional variables and R = {Ki | i ∈ I} is a setof epistemic relations, one for each agent i ∈ I, with I finite. The BMS system is
not dynamic in the first (PDL) sense and so we will refer to basic modal language(in which the only terms are the atoms Ki ) as L− (P, R). A model M = hW, V iof this signature is an epistemic model iff all the relations V (Ki ) are equivalence
relations. So far, this is all just standard epistemic logic. The innovation was
to define an action structure to be a structure of the form hD, U, prei for which
hD, U i is an epistemic structure and pre: D → L− (P, R) assigns a formula toeach element of D that expresses the ‘precondition’ of performing the action
it represents. For example, if d represents the announcement of ϕ, then it isusually assumed that, as a precondition, the announcement must be true, andso pre(d) = ϕ. Action structures are finite and so can be added to the syntax
as dynamic operators. The full language of BMS is thusϕ ::=p | ¬ϕ | (ϕ ∨ ϕ) | hKi iϕ | [D, U, pre, a]ϕwhere hD, U, prei is an action structure and a ∈ D is the designated action.
Given action structure ∆ = hD, U, prei and epistemic model M = hW, V i, theproduct model ∆M is defined to be h∆W, ∆V i, where∆W∆V (p)∆V (Ki )= {hu, di | M, u |= pre(d)}= {hu, di ∈ ∆W | u ∈ V (p)} for each p ∈ P= {hhu, di, hv, eii ∈ (∆W )2 | hu, vi ∈ V (Ki ) and hd, ei ∈ U (Ki )}Finally, the semantics of the BMS operator [D, U, pre, a] is given by
M, u |= [D, U, pre, a]ϕ iff

hD, U, preiM, hu, ai |= ϕ

254

General Dynamic Dynamic Logic

This can be seen as a special case of our general construction. First, we takea copy Ki0 of each symbol Ki , because we need to keep the signature of theepistemic model distinct from that of the action structure. Then we define thestructure A = hD, U 0 i of signature hQ, Si, with Q = ∅ and S = {Ki0 | i ∈ I},
such that U 0 (Ki0 ) = U (Ki ), for each i ∈ I. For each d ∈ D we define thetransformation Gd by h|Gd | = pre(d)i. This captures the idea of a precondition.
Finally, we take H to be the PDL-transformation given by hKi := Ki ; Ki0 i. To
show that [D, U, pre, a]ϕ is logically equivalent to [A, G, H, a]ϕ, the following
theorem is sufficient.
Theorem 3.1 With ∆ = hD, U, prei and A, G and H defined as above,∆M = [A, G, H]M
Proof: See Appendix.

,

It follows that every function on the class of models of a given signature thatis definable by a BMS operator is also definable by a GDDL operator.
3.2

LCC

LCC [21], the Logic of Communication and Change, extends BMS in two ways:
by expanding the base language to include PDL modalities, and by introducing ‘real-world’ change. The first extension is relatively straightforward. It
just amounts to moving from L− (P, R) to L(P, R), and the argument that theresulting system is a fragment of GDDL goes through as above. The second
extension, to model ‘real-world’ change, is achieved using ‘propositional substitutions’, which are functions σ : P → L(P, R) with a finite base, meaning that
σ is the identity function on all but a finite number of propositional variables.
An action that changes something other than just the psychological states of
agents can thus be represented by a propositional substitution σ such that, after
the change, p is true of state u iff σ(p) were true of it before the change. 17
A LCC action structure ∆ = hD, U, pre, subi consists of a BMS-like 18 action
structure hD, U, prei and a propositional substitution function subd for eachd ∈ D. Given an epistemic model M = hW, V i, the LCC product model ∆M isdefined to be h∆W, ∆V i as for BMS, except that
∆V (p)= {hu, di ∈ ∆W | u ∈ V (subd (p))} for each p ∈ P

To extend our earlier representation of BMS operators in GDDL requires only
one small change: the PDL-transformation Gd is now defined by hpre(d), p :=17 The restriction to σ of finite base requires the changes to be, in some sense, local. However,
the embedding of LCC in GDDL shows that what is important here is only that there is somefinite representation of σ, on the basis of which σ can be recovered algorithmically.
18 The only difference is that pre(d) is not restricted to L− (P, R); it may be any formula ofL(P, R).

Girard, Seligman and Liu

255

subd (p)i. With A and H defined as for BMS, we have the required result:
Theorem 3.2 With ∆ = hD, U, pre, subi and A, G and H defined as above,∆M = [A, G, H]M
Proof: See Appendix.

,

It follows that every function on the class of models of a given signature thatis definable by a BMS operator is also definable by a GDDL operator.
3.3

Other approaches

LCC was extended in [24] by basing it on PDL with relational converse (whichis still decidable). While GDDL does not include relational converse in the baselanguage, we can think of no reason why it could not be added, in a similarmanner to our addition of E over the vanilla PDL. We conjecture that otherdecidable extensions of PDL could be taken as the base logic. The combinationof converse with nominals (which is decidable from [14,1], p.12, Theorem 3.5)
should present no further difficulty. Another particularly useful decidable addition would be atomic negation on programs (see [25]) on the basis of which
E and the ‘window’ operators are definable.
There have been several attempts to extend dynamic logic to cope with relationchanging dynamic operators. Firstly, [22] shows how, for given finite epistemic
models M1 and M2 , it is possible to define a BMS operator [D, U, pre, a]ϕ of
BMS such that [D, U, pre, a]ϕM1 = M2 but this is far from what is needed torepresent relation-changing operators that have a uniform action on all models.
Next, [2] presents an interesting extension of modal logic with ‘graphmodification’ operators for models of arbitrary signature (as with GDDL).
There are three kinds of operator: ‘label modifications’ p + ϕ and p − ϕ, which
increase (and respectively decrease) V (p) by {u | M, u |= ϕ}; ‘edge label modification’ operators r + (ϕ, ψ) and r − (ϕ, ψ), which increase (resp. decrease)
V (r) by the set {hu, vi | M, u |= ϕ and M, u |= ψ}; and ‘new state’ operators→ which add a new isolated state to the domain (and shifts the pointnw and −nw,→ Of these, the label modification andof evaluation to it, in the case of −nw).
edge label modification operators define PDL-transformations and so can be
represented in GDDL. The new state operators are more tricky. Instead, in
GDDL, we can represent the addition of a set of (isolated) states, either withor without a shift in evaluation point, but we know of no way to ensure that
this set is a singleton. 19 Importantly, GDDL extends the approach of [2] by
19 For the analogue of nw, use the operator [A, G, H, a] in which A has domain {a, b} with anempty signature, Ga is the identity, Gb maps all propositional variables to ⊥ and all relation
symbols to ⊥?, and H is also the identity. Then if M = hW, V i, [A, G, H, a]M is isomorphic→ use [A, G, H, b]. The size of W 0 can
to hW ∪ W 0 , V i with W 0 disjoint from W . For −nw,
be diminished using a domain restriction component to Gb but without formulas that are

256

General Dynamic Dynamic Logic

including all PDL-transformations and products. 20
Finally, [9] and [10] propose a system of ‘arrow update’ operators with a novel
syntax in which new transitions for a relation are introduced by specifying theirpre- and post-conditions. They show that the resulting system is dynamicallyequivalent to BMS, and so can be seen as a way of giving an explicit syntax
for the part of BMS that allows a limited form of relation-change. GDDL is agenuine extension of both, as can be seen from the example of private beliefchange in Section 2.1. 21

4Conclusion

GDDL achieves our objective of generalising existing approaches to dynamic
epistemic logic to allow relational change and opens up a number of possibilities
for further work. Firstly, it would be interesting to look at fragments that canbe expressed in a more restricted syntax. Even the syntactically promiscuous
logics of BMS and LCC exploit only a small part of the generality of GDDL
operators, suggesting that other restrictions may be equally interesting in theirown right. A proper study of these would require a better understanding of
the class of model-transforming functions defined by GDDL. A good place tostart with this investigation is the category of PDL-transformations of models
of arbitrary signatures.
Secondly, we propose that many applications would profit from the ability tocode appropriate GDDL operators. For example, the study of the relationshipbetween first and higher-order psychological attitudes requires the interplay
between levels available in GDDL. This arises in preference logic when trying
to account for weakness of will, one analysis of which is the preference forhaving different preferences: I may prefer an action in which my preference forsmoking is downgraded to one in which it is not. Moving from the personalsetting, similar level-distinctions occur when reflecting on normative systems.
Certain changes to the law, for example, may be regarded as permissible, whileothers are not. And with a multi-agent perspective, one could try to devise
GDDL operators to model changes to conflicting normative systems, and so
provide a logic for reasoning about the effect of those changes, potentially givinga new approach to reasoning about conflict resolution. When the relations in aguaranteed to be true at only one state (such as the nominals of hybrid logic), we cannot
ensure that it is a singleton.
20 [2] also discusses ‘local’ graph modification operators, which significantly extend the expressive power of their system, sufficient to express the hybrid binder ↓ x, and so leads toundecidability ([6]). Augmentation of GDDL with a distinguished nominal for the point ofevaluation should have a similar effect.
21 [9] only allows a uniform update for all agents (the ‘common update policy’) but hints at
the possibility of providing distinct updates for each agent ‘privately’. This is done in [10],but these updates are not really ‘private’, just as our ⇑i operator (Section 2.1) is not private.
To achieve the genuine privacy of ↑i , some (as yet unformulated) hybrid of BMS and arrow
update logic would be needed.

Girard, Seligman and Liu

257

model are understood as state-transitions of some process (as in the standard
computational interpretation of PDL), GDDL operators encode operations forchanging what is possible to do, and so give a basis for reasoning about design.
Thirdly, from a technical point of view, the interaction between levels raises
interesting questions about the framing of general constraints on those interactions so as to ensure sensible results. We saw an example of this in our brief
exploration of private belief change (Footnote 13) but as yet we have no idea
about how to frame a general theory of such constraints.
These suggestions are of course very speculative but they give a sense of how
GDDL could be used to open up a new area for applications. Our motivations fordeveloping the system arose from technical considerations in an ongoing projectcalled ‘logic in the community’ [17], which aims at studying the consequencesof social relationships for our understanding of rational procedures. We expect
there to be many further uses for GDDL in that project.

References[1] Areces, C., P. Blackburn and M. Marx, The computational complexity of hybrid temporal
logics, Logic Journal of the IGPL 8 (2000), pp. 653–679.
[2] Aucher, G., P. Balbiani, L. F. del Cerro and A. Herzig, Global and local graph modifiers,
in: Proceedings of the 5th workshop on methods for modalities (MAM5 2007), Electronic
notes in theoretical computer science 231 (2009), pp. 293–307.
[3] Baltag, A., L. S. Moss and S. Solecki, The logic of public announcements, common
knowledge and private suspicious, Technical Report SEN-R9922, CWI, Amsterdam(1999).
[4] Baltag, A. and S. Smets, The logic of conditional actions, in: R. van Rooij and
K. Apt, editors, New perspective on games and interaction, Texts in logic and games 4,
Amsterdam University Press, 2008 pp. 9–31.
[5] Blackburn, P., M. de Rijke and Y. Venema, “Modal Logic,” Cambridge University Press,
Cambridge, Mass., 2001.
[6] Blackburn, P. and J. Seligman, What are hybrid languages?, in: M. Kracht, M. de Rijke,
H. Wansing and M. Zakharyaschev, editors, Advances in Modal Logic, 1, CSLI
Publications, Stanford University, 1998 pp. 41–62.
[7] Girard, P., “Modal Logic for Belief and Preference Change,” Ph.D. thesis, Stanford
University (2008).
[8] Harel, D. and R. Sherman, Propositional dynamic logic of flowcharts, Information andControl 64 (1985), pp. 119–135.
[9] Kooi, B. and B. Renne, Arrow update logic, Review of Symbolic Logic 4 (2011), pp. 536–
559.
[10] Kooi, B. and B. Renne, Generalized arrow update logic, in: Proceedings of the 13th
Conference on Theoretical Aspects of Rationality and Knowledge, TARK XIII (2011),
pp. 205–211.
[11] Liu, F., “Changing for the Better: Preference Dynamics and Agent Diversity,” Ph.D.
thesis, Institute for logic, Language and Computation, Universiteit van Amsterdam,
Amsterdam, The Netherlands (2008), ILLC Dissertation series DS-2008-02.
[12] Liu, F., “Reasoning about Preference Dynamics,” Synthese Library 354, Springer, 2011.
[13] Miller, J. S. and L. S. Moss, The undecidability of iterated modal relativization, Studia
Logica 68 (2001), pp. 1–37.

258

General Dynamic Dynamic Logic[14] Passy, S. and T. Tinchev, An essay in combinatory dynamic logic, Information andComputation 93 (1991), pp. 263–332.
[15] Plaza, J., Logics of public communications, Synthese 158 (2007), pp. 165–179.
[16] Pratt, V. R., Using graphs to understand PDL, in: Logic of Programs, Workshop (1982),
pp. 387–396.
[17] Seligman, J., F. Liu and P. Girard, Logic in the community, in: M. Banerjee and A. Seth,editors, ICLA, Lecture Notes in Computer Science 6521, 2011, pp. 178–188.
[18] van Benthem, J., Dynamic logic for belief revision, Journal of Applied Non-classical
Logic 17 (2007), pp. 129–155.
[19] Van Benthem, J., “Modal Logic for Open Minds,” CSLI lecture notes, Center for the
Study of Language and Information, 2010.
[20] van Benthem, J. and F. Liu, The dynamics of preference upgrade, Journal of Applied
Non-Classical Logics 17 (2007), pp. 157–182.
[21] van Benthem, J., J. van Eijck and B. Kooi, Logics of communication and change,
Information and computation 204 (2006), pp. 1620–1662.
[22] van Ditmarsch, H. and B. Kooi, Semantic results for ontic and epistemic change, in:
G. Bonanno, W. van der Hoek and M. Wooldridge, editors, Logic and the foundationsof game and decision theory (LOFT 7), Texts in logic and games (2008), pp. 87–117.
[23] van Ditmarsch, H., W. van der Hoek and B. Kooi, “Dynamic Epistemic Logic,” Berlin:
Springer, 2007.
[24] van Eijck, J. and Y. Wang, Propositional dynamic logic as a logic of belief revision, in:W. Hodges and R. de Queiroz, editors, WoLLIC 2008 (2008), pp. 136–148.
[25] Walther, D., “Propositional Dynamic Logic with Negation on Atomic Programs,”
Master’s thesis, Dresden University of Technology (2004).
[26] Zhen, L. and J. Seligman, A logical model of the dynamics of peer pressure, Electronic
Notes in Theoretical Computer Science 278 (2011), pp. 275–288.

Appendix
Proof of Lemma 1.1: We prove the two claims simultaneously by induction.
Assume that u ∈ ΛW .
M, u |= q Λ

iff
iff
iff
iff

M, u |= Λ(q)u ∈ [[Λ(q)]]M ∩ ΛWu ∈ ΛV (q)ΛM, u |= q

(definition of q Λ )(u ∈ ΛW )(definition ΛV (q))(definition ΛM )Negation and conjunction are straightforward.
M, u |= (hπiψ)Λ

u[[sΛ ]]M v

iff
iff
iff
iff
iff
iff

iff
iff
iff
iff

M, u |= hπ Λ iψ Λ
(def. (hπiψ)Λ )Λ M
Λu[[π ]] v and M, v |= ψ for some v ∈ W(def.)u[[π]]ΛM v and ΛM, v |= ψ for some v ∈ ΛW (IH)ΛM, u |= hπiψ(def.)u[[Λ(s); |Λ|?]]M v∃w : u[[Λ(s)]]M w & w[[|Λ|?]]M v
u[[Λ(s)]]M v & v[[|Λ|?]]M v
u[[Λ(s)]]M v & v ∈ [[|Λ|]]Mu[[Λ(s)]]M v & v ∈ ΛWu[[s]]ΛM v & v ∈ ΛW

(definition of sΛ )(definition of [[Λ(s); |Λ|?]]M )(w[[|Λ|?]]M v ⇒ w = v)
(definition of [[|Λ|?]]M )(definition of ΛW )(definition of [[Λ(s)]]M )Girard, Seligman and Liuu[[(ψ?)Λ ]]M v

iff
iff
iff
iff
iff

u = v and v[[(ψ Λ )?]]M v
u = v, v ∈ [[ψ Λ ]]M
u = v, v ∈ ΛW and v ∈ [[ψ]]ΛM
u = v, v ∈ ΛW and v[[ψ?]]ΛM v
v ∈ ΛW & u[[ψ?]]ΛM v

259(u[[(ψ?)Λ ]]M v ⇒ u = v)
(definition of [[(ψ Λ )?]]M )(IH, and u ∈ ΛW )(definition of [[ψ?]]ΛM )(u[[ψ?]]ΛM v ⇒ u = v)

The remaining cases are straightforward.
,

Proof of Lemma 2.3: In the first direction, assume that hhx1 , c1 i, hx2 , c2 ii ∈T 0 (τ ) and u[[τ ]]M v. Then, for some σ, hx1 , x2 i ∈ T (σ) and σ c1 ,c2 = τ . Since σ
is a basic program, it is either a relation symbol, E, or a test.
•

If σ = ψ? and c1 = c2 = c, then σ c1 ,c2 = ψ [A,G,c] ?. So u[[ψ [A,G,c] ?]]M v implies
that u = v and M, u |= ψ [A,G,c] . Hence, GM, hu, ci |= ψ, by assumption, so
hu, c1 i[[σ]]GM hv, c2 i.

•

If σ = r ∈ R, c1 = c2 = c, then σ c1 ,c2 = Gc (σ) = rGc . By Lemma 1.1,
u[[rGc ]]v implies that u[[σ]]Gc M v. Hence, hu, c1 i[[σ]]GM hv, c2 i, by definition.

•

If σ = E, then σ c1 ,c2 = |Gc1 |?; E; |Gc2 |?. So u[[|Gc1 |?; E; |Gc2 |?]]M v implies
that u ∈ [[|Gc1 |]]M and v ∈ [[|Gc2 |]]M , so hu, c1 i ∈ GW and hv, c2 i ∈ GW .
Therefore, hu, c1 i[[E]]GM hv, c2 i.

•

If σ ∈ S and hc1 , c2 i ∈ U (σ), then σ c1 ,c2 = >?, so u[[>?]]M v implies thatu = v. Thus, hu, c1 i[[σ]]GM hv, c2 i, by definition.

•

In any other case, σ c1 ,c2 = ⊥?. But this contradicts our assumption thatu[[σ c1 ,c2 ]]M v.

Therefore, hx1 , x2 i ∈ T (σ) and hu, c1 i[[σ]]GM hv, c2 i.
In the other direction, assume that γ(σ) and σ c1 ,c2 = τ for some σ. But
hx1 , x2 i ∈ T (σ) and σ c1 ,c2 = τ implies that hhx1 , c1 iihx2 , c2 i ∈ T 0 (τ ) by definition, so we only need to show that u[[σ c1 ,c2 ]]M v. Again, since σ is a basic
program, it is either a relation symbol, E, or a test.
•

If σ = ψ?, c1 = c2 = c, then σ c1 ,c2 = ψ [A,G,c] ?. Now, hu, ci[[ψ?]]GM hv, ci
implies that u = v and GM, hu, ci |= ψ. By assumption, M, u |= ψ [A,G,c] , sou[[σ c1 ,c2 ]]M v, by definition.

•

If σ = r ∈ R, c1 = c2 = c, then σ c1 ,c2 = Gc (σ). But hu, ci[[r]]GM hv, ci implies
that hu, vi ∈ Vc (r), by definition, so u[[Gc (r)]]M v. Hence, u[[σ c1 ,c2 ]]M v.

•

If σ = E, then σ c1 ,c2 = |Gc1 |?; E; |Gc2 |?. Now, hu, c1 i[[E]]GM hv, c2 i implies
that hu, c1 i ∈ GW and hv, c2 i ∈ GW , so u ∈ [[|Gc1 |]]M and v ∈ [[|Gc2 |]]M .
But u[[E]]M v, so u[[|Gc1 |?; E; |Gc2 |?]]M v.

•

If σ = s ∈ S and hc1 , c2 i ∈ U (σ), then σ c1 ,c2 = >?. Thus, hu, c1 i[[s]]GM hv, c2 i
implies that u = v. But M, u |= >, so u[[>?]]M u. Hence, u[[σ c1 ,c2 ]]M v.

260

•

General Dynamic Dynamic Logic

In any other case, σ c1 ,c2 = ⊥?. But this contradicts our assumption thathu, c1 i[[σ]]GM hv, c2 i.

Therefore, u[[σ c1 ,c2 ]]M v.

0

,

00

Proof of Theorem 3.1: Let ∆M = hW , V i and [A, G, M ]M = hΛGW, ΛGV i.
Then,
ΛGW

ΛGV (p)

=
=
=
=
=
=
=

GW
{hu, di | u ∈ [[|Gd |]]}
{hu, di | u ∈ [[|pre(d)|]]}∆W(|Λ| = >)(definition)(assumption)[[ΛG(p)]]M ∩ ΛGW[[p]]M ∩ ∆W
∆V (p)(definition)(ΛGW = ∆W )(definition)[[ΛGd (ri )]]ΛGM==[[Λ(ri )]]ΛGM[[ri ; si ]]GM

(Gd (ri ) = ri )(assumption)

But hu, di[[ri ; si ]]GM hv, ei iff there exists hw, f i ∈ GW such thathu, di[[ri ]]GM hw, f i and hw, f i[[si ]]GM hv, ei, iff d = f and w = v, by definition. Hence, hu, di[[ri ; si ]]GM hv, ei iff hu, di[[ri ]]GM hv, di and hv, di[[si ]]GM hv, ei
iff u[[Gd (ri )]]M v and d[[si ]]A e, by definition, iff u[[ri ]]M v and d[[si ]]A e. Therefore,[[ΛGd (ri )]]ΛGM = ∆V (r).
,Proof of Theorem 3.2: The proof is the same as the previous theorem but forthe propositional case:ΛGd V (p)===[[ΛGd (p)]]M ∩ ΛGW[[subd (p)]]M ∩ ∆W
∆V (p)(definition)(ΛGW = ∆W )(definition),

Acknowledgements: We would like to thank the anonymous referees fortheir valuable comments. Fenrong Liu is supported by the Major Programof the National Social Science Foundation of China (NO. 11&ZD088) and the
National Natural Science Foundation of China (NO.81173464). Jeremy Seligman was supported by the National Social Science Foundation Key Project ofChina (NO.11AZD57). He is also grateful to Auckland University for allowing
a period of absence during which time the research was completed.