Dynamic Epistemic Temporal Logic

Dynamic Epistemic Temporal Logic∗ Bryan Renne†

Joshua Sack‡§

Audrey Yap¶

March 25, 2010

Abstract We propose Dynamic Epistemic Temporal Logic, a dynamic-protocol framework that overcomes the Problem of Synchronicity in the popular Dynamic Epistemic Logic approach to reasoning about multi-agent belief change. Dynamic Epistemic Temporal Logic not only extends the domain of applicability of standard Dynamic Epistemic Logic, but it also clarifies how certain structural properties (such as synchronicity) arise from the inherent structure of the standard “update frames” (or “action models”) of Dynamic Epistemic Logic.

1

Introduction

Epistemic Logic [5] is a modal-logic approach to reasoning about beliefs, including beliefs about basic assertions (“Alice believes that the train stops at Chongqing”) and higher-order beliefs (beliefs about others’ beliefs: “Bob believes that Alice believes that the train stops at Chongqing”). Dynamic Epistemic Logic [1, 2, 3, 13, 14] is an extension of Epistemic Logic used for reasoning about changes in belief that arise as a result of certain “informational events” such as public announcements or private communications. An informational event may change an agent’s beliefs about which basic assertions are true or false in the world: after a public announcement that “the train stops at Chongqing,” Alice will believe that the train stops at Chongqing. But informational events may also change higher-order beliefs: after the public announcement that “the train stops at Chongqing,” Bob will believe that Alice believes that the train stops at Chongqing. The characteristic feature of the Dynamic Epistemic Logic approach is its use of update modals, which are modal operators [U, s] that describe operations on Kripke models. These operations, called updates, represent “informational events” in which the agents receive information that may bring about changes in their beliefs. The basic idea is that an update modal ∗

This paper is a revised and extended version of [9]. Faculty of Philosophy, University of Groningen, The Netherlands. http://bryan.renne.org/ ‡ School of Computer Science, Reykjav´ık University, Iceland. http://www.joshuasack.info/ § Joshua Sack was partly supported by the projects “New Developments in Operational Semantics” (nr. 080039021) and “Processes and Modal Logic” of The Icelandic Research Fund along with a grant from Reykjav´ık University’s Development Fund. ¶ Department of Philosophy, University of Victoria, Canada. http://web.uvic.ca/∼ayap/ †

1

[U, s] describes a specific partial function f[U,s] that maps a pointed Kripke model (M,
w) in the domain of f[U,s] to another pointed Kripke model that we write as M [U ], (w, s) . This allows us to view a sequence (M0 , w0 ), (M1 , w1 ), (M2 , w2 ), . . . , (Mn , wn )

(1)

of pointed Kripke models, with (Mi+1 , wi+1 ) generated from (Mi , wi ) by the update f[Ui+1 ,si+1 ] described by update modal [Ui+1 , si+1 ], as a discrete-time distributed multi-agent system in which the state of the system at time i is described by (Mi , wi ). Defining the time of a world w in Mi within the sequence (1) to be the index i, we obtain a notion of time that is external to the pointed Kripke model (Mi , wi ). One consequence of adopting this external notion of time is that all of the worlds that an agent considers possible relative to a world w in Mi have time i. This implies that at every world, every agent knows the current time. Systems in which the current time is known at every world are called synchronous [11, 12]. Dynamic Epistemic Logic frameworks that adopt this external notion of time are consequently restricted to the study of synchronous multi-agent systems [11, 12]. Such frameworks are therefore unable to represent systems in which agents can become mistaken or uncertain about time; we call this limitation the Problem of Synchronicity. An important multi-agent system framework that avoids the Problem of Synchronicity is Epistemic Temporal Logic [11, 12], which has close connections with the knowledge-based message semantics of [8] and the related interpreted systems approach of [5]. In fact, the Problem of Synchronicity is avoided even in a very basic Epistemic Temporal Logic whose only temporal modality is a discrete one-step–past operator. We call this basic logic Simple Epistemic Temporal Logic. Like Epistemic Temporal Logic, Simple Epistemic Temporal Logic uses epistemic temporal models, which are Kripke models in which one of the relational components is designated as a time-keeping relation. We label the time-keeping relation using the symbol Y (a mnemonic for “yesterday”). When a world w is related to a world w0 according to the time-keeping relation (so there is a “Y -arrow” from w to w0 ) the intended interpretation is that w0 is a possible way the system might have been “yesterday,” meaning one time-step before w. Defining the time of a world w in an epistemic temporal model M to be the maximum number of Y -arrows that can be taken from w, we obtain an internal notion of time because the time of a world is determined solely based on the time-keeping relation, which is internal to the model. Since Simple Epistemic Temporal Logic is arguably the most basic Epistemic Temporal Logic in which the time of a world can be expressed, we will focus on this basic Epistemic Temporal Logic in this paper. And in order to make clear whether a given Kripke model is one that has a designated time-keeping relation (called the Y -relation), we adopt the following terminology: epistemic temporal models are Kripke models with a designated Y -relation—these have an internal notion of time—whereas epistemic models are Kripke models without a designated Y -relation—these have an external notion of time. One key strength of epistemic temporal models is that the internal notion of time can be used to describe multi-agent systems that need not be synchronous. Since Dynamic Epistemic Logic uses epistemic models (having external time) and hence suffers from the Problem of Synchronicity, we see that even Simple Epistemic Temporal Logic can handle a wider class of multi-agent systems than that which can be handled by Dynamic Epistemic Logic. This observation might suggest that Epistemic Temporal Logic is more useful than Dynamic Epistemic Logic. But in Epistemic Temporal Logic, every possible way in which 2

the system can evolve must be determined in advance within the model using the internal time-keeping relation; said informally, the protocol is fixed in Epistemic Temporal Logic. In contrast, the protocol in Dynamic Epistemic Logic is dynamic, as the way the system progresses is determined on-the-fly by the choice of the update modal that is used to produce the next pointed Kripke model appearing in the sequence (1). And although Dynamic Epistemic Logic is expressively equivalent to Epistemic Logic, the succinctness result of Lutz [7] showed that an important multi-agent fragment of Dynamic Epistemic Logic is exponentially more succinct than Epistemic Logic in handling this dynamics. To summarize, there is an important trade-off between the two approaches: Epistemic Temporal Logic can handle asynchronicity but is limited to fixed protocols, whereas Dynamic Epistemic Logic has (succinct) dynamic protocols but suffers from the Problem of Synchronicity. In this paper, we propose a solution to the Problem of Synchronicity in a dynamicprotocol framework. Our solution is the framework we call Dynamic Epistemic Temporal Logic. Dynamic Epistemic Temporal Logic keeps track of time internally using epistemic temporal models, thereby permitting the possibility of asynchronous multi-agent systems. To maintain dynamic protocols, Dynamic Epistemic Temporal Logic extends the updates of Dynamic Epistemic Logic from the class of epistemic models (having external time) to the class of epistemic temporal models (having internal time). To achieve this, Dynamic Epistemic Temporal Logic adds a new structural component to update modals [U, s]: the Y -arrow. Y -arrows are used to specify exact positions in which the update f[U,s] is to insert Y -arrows in the updated model M [U ]. Whereas standard Dynamic Epistemic Logic updates ensure that each world in M [U ] is one time-step ahead of any world in M , our Y -arrows allow for greater flexibility in modeling the passage of time. In particular, using the internal notion of time associated with the Y -relation, Y -arrows allow us to give worlds in M [U ] any natural-number time. For example, in certain updates that embed M into M [U ], each world in M [U ] can be seen either as a world in M or else as an arbitrarily distant possible future of a world in M . This flexibility is essential in the study of asynchronous systems and is the key to our solution to the Problem of Synchronicity. After describing Dynamic Epistemic Temporal Logic and its use of Y -arrows, will show that it is possible to identify sufficient conditions on our new update modals [U, s] that will guarantee that the update f[U,s] embeds M into M [U ] or preserves properties such as synchronicity in the resulting epistemic temporal model M [U ]. We shall then use these conditions to show that epistemic temporal models that result from sequentially applying a proper subclass of our new Y -arrow–based updates are isomorphic to the generated sequences of epistemic models from standard Dynamic Epistemic Logic that have been studied by a number of authors [6, 10, 11, 12, 15]. While [11, 12] showed that properties such as synchronicity are necessary of sequences generated in standard Dynamic Epistemic Logic, our Isomorphism Theorem (Theorem 6.13) demonstrates that the necessity of these properties stems from the inherent structure of standard Dynamic Epistemic Logic update modals [U, s] themselves. This provides a new perspective on the results of [11, 12] as well as a method of circumventing the restrictions that such properties can impose. In particular, this provides us with a solution to the Problem of Synchronicity in the dynamic-protocol framework of Dynamic Epistemic Temporal Logic. In the next section, we introduce the language LDETL and the theory TDETL of Dynamic Epistemic Temporal Logic. So as to maintain readability of the text, we have moved all 3

proofs to an appendix.

2

Syntax

Notation 2.1 (A, Y , Y ). A is a finite nonempty set of symbols not containing the symbols Y and Y . The members of A will be called agents. To define LDETL , we must first define the internal structure of update modals [U, s]. This structure is built on top of finite Kripke frames. If S is a nonempty set of symbols, then a Kripke frame F (for S) is a pair (W F , RF ) consisting of a nonempty set W F whose members F are called worlds and a function RF : S → (W F → 2W ) mapping each symbol m ∈ S to F a function Rm : W F → 2W ; to say that F is finite means that W F is finite.1 The internal structure of update modals [U, s] is given by the structure of the object U , called an update frame. Definition 2.2. For a language L, whose formulas we call L-formulas, an L-update frame is a tuple U = (W, R, p) satisfying the following: (W, R) is a finite Kripke frame for A ∪ {Y, Y } said to be underlying U , and p : W → L is a function mapping each world s ∈ W to an L-formula p(s). A state in U is just a world in the Kripke frame underlying U . Notation: for an L-update frame U , we write W U to denote the first component of the tuple U , we write RU to denote the second component of the tuple U , and we write pU to denote the third component of the tuple U . A pointed L-update frame is a pair (U, s) consisting of an L-update frame U and a state s ∈ W U that will be called the point of (U, s). Update frames are also called “action models” (or “event models”) in the Dynamic Epistemic Logic literature [1, 2, 3, 13, 14]. For an update frame U , a state s ∈ W U represents the communication of the formula pU (s). For an agent a ∈ A, the function RaU represents agent a’s conditional uncertainty as to which formula is communicated: if s0 ∈ RaU (s) and the formula pU (s) was in fact communicated, then agent a will think that the formula pU (s0 ) is one of the formulas that might have been communicated. We now define our language LDETL as an extension of the language LSETL of Simple Epistemic Temporal Logic. Notation 2.3. N is the set {0, 1, 2, 3, . . . } of natural numbers (this includes 0), and N+ is the set {1, 2, 3, . . . } of positive natural numbers (this excludes 0). Z is the set {. . . , −3, −2, −1}∪ N of integers. Definition 2.4 (LSETL ). LSETL , the Language of Simple Epistemic Temporal Logic, consists of the formulas formed by the following grammar. ϕ ::= ⊥ | > | pk | ϕ ? ϕ | ¬ϕ | [a]ϕ

k ∈ N, ? ∈ {→, ∨, ∧, ≡}, a ∈ A ∪ {Y } Terminology: we call [Y ] the yesterday modal. For each agent a ∈ A, we read the formula [a]ϕ as “agent a believes that ϕ is true.” We read the formula [Y ]ϕ as “ϕ is true in all ¯ aF def The function RaF gives rise to a binary relation R = {(x, y) ∈ W F × W F | y ∈ RaF (x)} on W F . We F F ¯ ¯ aF as a-arrows. will conflate Ra and Ra whenever it is convenient. We will often refer to the members of R 1

4

CL. Ka .

Basic Schemes Schemes for Classical Propositional Logic [a](ϕ → ψ) → ([a]ϕ → [a]ψ) for a ∈ A

[Y ](ϕ → ψ) → ([Y ]ϕ → [Y ]ψ)
UA. [U, s]q ≡ pU (s) → q for q ∈ {pk , ⊥, >}
U?. [U, s](ϕ ? ψ) ≡ [U, s]ϕ ? [U, s]ψ for ? ∈ {→, ∨, ∧, ≡}
U¬. [U, s]¬ϕ ≡ pU (s) → ¬[U, s]ϕ
V U[a]. [U, s][a]ϕ ≡ pU (s) → s0 ∈RaU (s) [a][U, s0 ]ϕ for a ∈ A
V U[Y ]. [U, s][Y ]ϕ ≡ pU (s) → s0 ∈RU (s) [Y ][U, s0 ]ϕ ∧ Y
V pU (s) → s0 ∈RU (s) [U, s0 ]ϕ

KY .

Y

Rules `ϕ→ψ

`ψ

`ϕ

(MP)

a ∈ A ∪ {Y }

` [a]ϕ

`ϕ

(MN)

`ϕ

` [U, s]ϕ

(UN)

Figure 1: The theory TDETL possible yesterdays.” Notation: for each a ∈ A ∪ {Y }, we let hai abbreviate ¬[a]¬; we define def def for each i ∈ N the formula [a]i ϕ by setting [a]0 ϕ = ϕ and [a]i+1 ϕ = [a]([a]i ϕ); for i ∈ N, the formula haii ϕ is defined analogously. Definition 2.5 (LDETL , TDETL ). LDETL is the Language of Dynamic Epistemic Temporal Logic. The LDETL -formulas are the formulas that may be formed by the grammar obtained from that in Definition 2.4 by adding the following formula-formation rule: if ϕ is an LDETL formula and (U, s) is a pointed L-update frame with ∅ = 6 L ⊆ LDETL , then [U, s]ϕ is an LDETL -formula. LDETL consists of the LDETL -formulas along with the L-update frames for which ∅ 6= L ⊆ LDETL . Terminology: we call [U, s] an update modal. Notation: we let hU, si abbreviate ¬[U, s]¬. We read the formula [U, s]ϕ as “after update f[U,s] , ϕ is true.” An update frame is an LDETL -update frame. A formula is a LDETL -formula. TDETL , the Theory of Dynamic Epistemic Temporal Logic, is defined in Figure 1. Since our interest here is in implementing update mechanisms on Kripke models with a designated Y -relation, we do not impose any of the usual properties on belief or on time that one might expect [5, 6, 10, 11, 12, 15]. So TDETL should be viewed as the minimal theory that brings update mechanisms to Simple Epistemic Temporal Logic. Future work will investigate extensions of this theory that include familiar restrictions on belief and on time, though we do address the preservation of certain time-related properties in Section 5. Definition 2.6 (LDETL Complexity; adapted from [14]). To each formula ϕ ∈ LDETL , we assign a positive natural number c(ϕ) ∈ N+ , called the complexity of ϕ, as follows: letting |W U | denote the (nonzero, finite) number of states in an update frame U , we make the 5

q◦

= q if q ∈ {pk , ⊥, >}

(ϕ ? ψ)◦

= ϕ◦ ? ψ ◦

(¬ϕ)◦

= ¬(ϕ◦ )

([a]ϕ)◦

= [a](ϕ◦ ) if a ∈ A

([Y ]ϕ)◦

= [Y ](ϕ◦ )

([U, s]q)◦ ([U, s](ϕ ? ψ))◦ ([U, s]¬ϕ)◦ ([U, s][a]ϕ)◦ ([U, s][Y ]ϕ)◦

= (pU (s))◦ → q if q ∈ {pk , ⊥, >} = ([U, s]ϕ)◦ ? ([U, s]ψ)◦

= (pU (s))◦ → ¬([U, s]ϕ)◦ V = (pU (s))◦ → s0 ∈RaU (s) [a]([U, s0 ]ϕ)◦ if a ∈ A
V = (pU (s))◦ → s0 ∈RU (s) [Y ]([U, s0 ]ϕ)◦ ∧ Y
V (pU (s))◦ → s0 ∈RU (s) ([U, s0 ]ϕ)◦ Y

([U, s][U 0 , s0 ]ϕ)◦ = ([U, s]([U 0 , s0 ]ϕ)◦ )◦

Figure 2: Function ◦ taking LDETL -formulas to LSETL -formulas, Theorem 2.8 following definitions. c(q)

def

c(ϕ ? ψ)

def

c(¬ϕ)

def

c([a]ϕ)

def

= 1 for q ∈ {pk , ⊥, >}

= 1 + max{c(ϕ), c(ψ)} = 1 + c(ϕ) = 1 + c(ϕ) for a ∈ A ∪ {Y }

def

c([U, s]ϕ) = (4 + c(U )) · c(ϕ) c(U )

def

= (1 + |W U |) · maxs∈W U c(pU (s))

Notation 2.7 (Ln ). For each fragment L of LTDEL and each n ∈ N, we let Ln denote the set of L-formulas ϕ with c(ϕ) ≤ n. Theorem 2.8 (LDETL Reduction). The equations in Figure 2 define a function that maps each LDETL -formula ϕ to an LSETL -formula ϕ◦ such that ` ϕ ≡ ϕ◦ . Further, the equations in Figure 2 are complexity-respecting: for each equation in Figure 2, ◦ is applied on the left-hand side to a formula whose complexity is strictly larger than that of any formula on the right-hand side to which ◦ is applied.

3

Semantics

Having defined the language LDETL and theory TDETL of Dynamic Epistemic Temporal Logic, we now define the semantics of LDETL . A Kripke model M is a tuple (W M , RM , V M ) consisting of a Kripke frame (W M , RM ) said to be underlying M and a function V M : {pk | k ∈ N} → M 2W called a (propositional) valuation. A pointed Kripke model is a pair (M, w) consisting 6

of a Kripke model M and a world w ∈ W M . The notion of LDETL -truth extends the standard semantics for Dynamic Epistemic Logic [1, 2, 3, 13, 14] in the following way. Definition 3.1 (LDETL -Truth, LDETL -Validity). For a pointed Kripke model (M, w) and a formula ϕ, we write M, w |=LDETL ϕ to mean that ϕ is true at (M, w), and we write M, w 6|=LDETL ϕ to mean that ϕ is not true at (or false at) (M, w). The notion of truth of a formula at a pointed Kripke model is defined by the following induction on formula construction. • M, w 6|=LDETL ⊥ and M, w |=LDETL >. • M, w |=LDETL pk means that w ∈ V M (pk ). • M, w |=LDETL ϕ ? ψ means that M, w |=LDETL ϕ star M, w |=LDETL ψ, where “star” is to be replaced by the (mathematical) English reading for the binary Boolean connective ?.2 • M, w |=LDETL ¬ϕ means that M, w 6|=LDETL ϕ. • M, w |=LDETL [a]ϕ means that M, x |=LDETL ϕ for each x ∈ RaM (w). • M, w |=LDETL [U, s]ϕ means that if M, w |=LDETL pU (s), then M [U ], (w, s) |=LDETL ϕ, where M [U ] is defined as follows. def

W M [U ] = {(x, t) ∈ W M × W U : M, x |=LDETL pU (t)}

For a ∈ A: M [U ]

Ra

M [U ]

RY

def

(x, t) = {(y, u) ∈ W M [U ] : y ∈ RaM (x) and u ∈ RaU (t)} def

(x, t) = {(y, u) ∈ W M [U ] : y ∈ RYM (x) and u ∈ RYU (t)} ∪ def

{(y, u) ∈ W M [U ] : y = x and u ∈ RYU (t)}

V M [U ] (pk ) = {(x, t) ∈ W M [U ] : M, x |=LDETL pk }

To say that a formula ϕ is valid in a Kripke model M , written M |=LDETL ϕ, means that M, w |=LDETL ϕ for each world w ∈ W M . To say that a formula ϕ is valid, written |=LDETL ϕ, means that M |=LDETL ϕ for each Kripke model M . When it ought not cause confusion, we may omit the subscript “LDETL ” when writing |=LDETL . Given a pointed Kripke model (M, w) representing a multi-agent situation and
a pointed U update frame (U, s) with M, w |= p (s), the pointed Kripke model M [U ], (w, s) represents the situation after the occurrence of the update described by [U, s]. According to Definition 3.1, a world (x, t) must satisfy the property that M, x |= pU (t). The set {x ∈ W M | M, x |= pU (t)} of worlds x in M that satisfy pU (t) intuitively represents the set of worlds in M at which the formula pU (t) can truthfully be communicated—these are the worlds at which t can take place. M [U ] For each a ∈ A, Definition 3.1 tells us that the relation Ra is determined by two factors: agent a’s uncertainty as to which world was the case before the communication (represented 2

Read → as “implies,” read ∨ as “or,” read ∧ as “and,” and read ≡ as “if and only if.”

7

by RaM ) and agent a’s uncertainty as to which communication has occurred (represented M [U ] by RaU ). In particular, suppose (x0 , t0 ) ∈ Ra (x, t). Then if the communication pU (t) corresponding to t actually occurred at world x, then agent a will think it possible that the communication pU (t0 ) corresponding to t0 occurred at world x0 . M [U ] According to Definition 3.1, the relation RY is determined by two factors. The first M [U ] U M is the interaction between the relations RY and RY , which adds pairs to RY just as the M [U ] M U for a ∈ A. The second factor is the relation interaction between Ra and Ra did to Ra U RY : if there is a Y -arrow from state t to state t0 in U , then there will be a Y -arrow from world (x, t) to world (x, t0 ) in M [U ]. The presence of a Y -arrow from t to t0 in U thus says that the communication corresponding to t0 is to be thought of as occurring one time-step before the communication corresponding to t. This addition to the standard definition of updates in Dynamic Epistemic Logic [1, 2, 3, 13, 14] allows us to control how an update affects the time of worlds in the model M [U ]. Finally, we see that the valuation V M [U ] after the update simply inherits its truth conditions from the valuation V M before the update, making our updates purely temporalepistemic. Theorem 3.2 (Correctness). For each formula ϕ, we have ` ϕ if and only if |= ϕ.

4

A Simple Example

Suppose Passengers a and b are traveling together by train in China. Further, suppose Passenger a understands Mandarin but that Passenger b does not, though Passenger b mistakenly believes that they are both equally ignorant of the language. Now consider two scenarios in which an announcement in Mandarin about a delay in arrival is made over the loudspeaker. 1. Passengers a and b are both awake and alert during the announcement. 2. Passenger a is awake and alert, but Passenger b, who is sleepy, dozes off and sleeps through the announcement. Waking up a few minutes later without knowing that the announcement occurred, Passenger b mistakenly thinks that instead of sleeping for a few minutes, he merely blinked. Taking p to be a propositional letter denoting the statement about late arrival, we represent the first and the second scenarios in our framework using update frames (U1 , t1 ) and (U2 , t2 ), respectively pictured on the left and on the right in Figure 3. In the first scenario, Passenger b knows that an announcement has taken place, but it provides him with no new (non-temporal) information, nor does he believe that a gained any (non-temporal) information. In effect, this is a synchronous private announcement to a; after all, both a and b know that an announcement occurred—so the event is synchronous—but only a knows the content of the announcement—so the event is private to a. In Figure 3, s1 and u are states in which no new (non-temporal) information is conveyed (since > is always true and thus conveys no new non-temporal information), while t1 is a state in which the message p is communicated. Since t1 and u are each connected to s1 using a Y -arrow, the 8

t1 Y

p

a

s1 a, b, Y

s2

⊤

a, b, Y

b Y

U1

Y

t2

p

⊤

a

b

⊤

a, b

u

U2

Figure 3: Update frames for the synchronous (U1 , t1 ) and asynchronous (U2 , t2 ) private announcement of p to a. communications they represent occur one time-step after the communication represented by s1 . Since s1 is labeled by >, has a reflexive x-arrow for every x ∈ {a, b, Y }, and has no exiting Y -arrows, we see by the definition of truth (Definition 3.1) that any Kripke model M is embedded into the Kripke model M [U1 ] by the mapping taking each world y ∈ W M to the world (y, s1 ) ∈ W M [U1 ] . This embedding preserves a copy of the “past situation” M within the “current situation” M [U1 ], which leads us to call s1 a “past state.” So the role of the past state s1 is to preserve a copy of a given situation M . The states t1 and u then represent communications that occur one time-step after the situation M . At state t1 , Passenger a believes that t1 represents the only possible communication, while Passenger b believes that u represents the only possible communication. Since both u and t1 are one time-step after the past state s1 , the update f[U1 ,t1 ] describes the private communication of p to Passenger a in which it is common knowledge that one time-step occurs. So we see that
|= (¬hY i> ∧ ¬[b]p) → [U1 , t1 ] [a]hY i> ∧ [a]p ∧ [b]hY i> ∧ ¬[b]p . That is, if no event has yet occurred and Passenger b does not believe p, then, after the occurrence of f[U1 ,t1 ] , Passenger a believes that an event occurred and that p is true, whereas Passenger b believes that an event occurred but does not believe that p is true. In contrast, the second scenario is in effect an asynchronous private announcement to a. After all, while Passenger a knows that an announcement occurred and she knows its content, Passenger b has two mistaken beliefs: first, that no announcement occurred, and second, that the amount of time between closing and later opening his eyes is essentially negligible. b thus does not even think it possible that an event has occurred. Since the announcement results in b having a mistaken belief about the number of events that have occurred, the announcement event is asynchronous. At state t2 in Figure 3, Passenger a knows that p is communicated, but Passenger b mistakenly believes that no event took place because the only state he considers possible is the past state s2 . Accordingly, we see that
|= (¬hY i> ∧ ¬[b]p) → [U2 , t2 ] [a]hY i> ∧ [a]p ∧ ¬[b]hY i> ∧ ¬[b]p . 9

That is, if no event has yet occurred and Passenger b does not believe that p is true, then, after the occurrence of f[U2 ,t2 ] , Passenger a believes that an event occurred and that p is true, whereas Passenger b believes neither that an event occurred nor that p is true. These scenarios demonstrate the way in which our framework uses Y -arrows to describe synchronous and asynchronous private communications. In particular, we see that Y -arrows can be used to describe updates that need not preserve synchronicity, as is the case with the asynchronous private announcement.

5

Properties and Preservation

In this section, we define several properties of Kripke models and update frames and then study sufficient conditions for the preservation of these properties after the occurrence of an update. Definition 5.1 (T -Runs, T -Histories, T -Depth). Fix a symbol T ∈ {Y, Y } and let F = (W, R) be a Kripke frame for A ∪ {Y, T }. A T -run (in F ) is a finite nonempty sequence {wi }ni=0 of worlds in F satisfying the property that n ∈ N and for each i ∈ N with i < n, we have that wi+1 ∈ RTF (wi ). We say that a T -run {wi }ni=0 begins at w0 and ends at wn . The length of a T -run {wi }ni=0 is defined as the number n. (Observe that the length of a T -run is one less than the number of worlds that make up the T -run.) To say that a T -run σ 0 end-extends a T -run σ means that σ is a (not necessarily proper) prefix of σ 0 . (Note that each T -run end-extends itself.) To say that a T -run σ is end-maximal (in F ) means that no T -run in F end-extends σ other than σ itself. A T -history (in F ) is a T -run in F that is end-maximal. (Note that a nonempty suffix of a T -history is itself a T -history.) A world appearing at the end of a T -history in F is said to be T -terminal (in F ). We define a function dFT : W F → N ∪ {∞} as follows: if there is a maximum n ∈ N such that there is a T -history in F of length n that begins at w, then dFT (w) is this maximum n; otherwise, if no such maximum n ∈ N exists, then dFT (w) is ∞. We will call dFT (w) the T -depth of w. Definition 5.2. Fix T ∈ {Y, Y } and let F = (W, R) be a Kripke frame for A ∪ {Y, T }. • T -Depth–Defined (T -DD). To say that F is T -depth–defined (T -DD) means that for each world w in F , we have that dFT (w) 6= ∞.3 • Non–T -Branching. To say that F is non–T -branching means that for each w ∈ W F , the set RTF (w) has at most one member. • T -Synchronous. To say that F is T -synchronous means that F is T -DD and for each a ∈ A, each w ∈ W F , and each w0 ∈ RaF (w), we have that dFT (w0 ) = dFT (w). The negation of “T -synchronous” is T -asynchronous. 3

We observe that if F is T -depth–defined, then F is T -converse well-founded (that is, for every nonempty set S of worlds in F , there is a nonempty subset S 0 ⊆ S such that each world w ∈ S 0 is T -terminal). However, if F is T -converse well-founded, it need not be the case that F is also T -depth–defined. So the notion of T -depth–definedness is strictly stronger than the notion of T -converse well-foundedness.

10

• T –Memory-Preserving. To say that F is T –memory-preserving means that F is T -DD and for each a ∈ A, each w ∈ W F , each v ∈ RaF (w), and each w0 ∈ RTF (w), there is a world v 0 ∈ RaM (w0 ) ∩ (RTF )∗ (v), where (RTF )∗ is the reflexive transitive closure of RTM .4 Diagrammatically: T

w′

w

a

a

v′

T∗

v

In a T -synchronous Kripke frame, T –memory-preservation is equivalent to the wellknown property of Perfect Recall (for T ) [11, 12].5 Convention: for tuples J having a Kripke frame (W J , RJ ) underlying J, any use of a property or concept from Definition 5.1 or Definition 5.2 in reference to J is meant to be a use of that property or concept in reference to the Kripke frame (W J , RJ ) underlying J. Example: for an update frame U , the expression “Y -run in U ” is to be identified with the expression “Y -run in (W U , RU ).” Definition 5.3 (Kripke Model Properties). Let M be a Kripke model. • Synchronicity. To say that M is synchronous means that M is Y -synchronous. The negation of “synchronous” is asynchronous. • Non–Past-Branching. To say that M is non–past-branching means that M is non–Y branching. • Forest-like. branching.

To say that M is forest-like means that M is Y -DD and non–past-

• Memory-Preserving. To say that M is memory-preserving means that M is Y –memorypreserving.6 In a synchronous Kripke model, memory-preservation is equivalent to the well-known property of Perfect Recall [11, 12]. Definition 5.4 (Update Frame Properties and Concepts). Let U be an update frame. • Path-Preserving. A path-preserving run (in U ) is a Y -run {si }ni=0 in U satisfying the property that for each i ∈ N with i < n, we have |= pU (si ) → pU (si+1 ). To say that U is a path-preserving update frame means that each Y -run in U is path-preserving. The reflexive transitive closure R∗ : A → (W → 2W ) of R : A → (W → 2W ) is given as follows: v ∈ R∗ (v) means that there is a finite sequence {vi }ni=0 with n ∈ N such that v0 = v, vn = v 0 , and vi+1 ∈ R(vi ) for each i ∈ N with i < n. 5 In words, to say that F satisfies Perfect Recall for T means that for each a ∈ A, each w ∈ W F , each v ∈ RaF (w), each w0 ∈ RTF (w), and each v 0 ∈ RTF (v), we have that v 0 ∈ RaM (w0 ). The diagram for Perfect Recall for T is obtained from the T –memory-preservation diagram by replacing the dashed T ∗ -arrow with a solid T -arrow. 6 Informally, in a memory-preserving Kripke model, an agent considers a world possible at time t only if that world was a future of a world considered possible at time t − 1. 4

0

11

• Depth-Respecting. To say that U is depth-respecting means that U is Y -DD and for each s ∈ W U and each s0 ∈ RYU (s), we have that dUY (s0 ) ≤ dUY (s). • Past State. To say that a state s ∈ W U is a past state means we have that |= pU (s) ≡ >, that RYU (s) = ∅, and that RaU (s) = {s} for each a ∈ A ∪ {Y }. • Past-Preserving. To say that U is past-preserving means U is Y -DD, path-preserving, and every Y -run in U can be end-extended to a Y -history in U that ends at a past state. • Non–Past-Splitting. To say that U is non–past-splitting means that for each s ∈ W U , we have that RYU (s) ∪ RYU (s) has at most one member and that RYU (s) ∩ RYU (s) = ∅.

Having defined these properties, we investigate their preservation under the presence of updates in the following two theorems. Theorem 5.5 concerns the behavior of past states in update frames, and Theorem 5.6 concerns the preservation of properties in Kripke models. Theorem 5.5 (Past State). Let U be an update frame and M be a Kripke model. • If s is a past state in U , then for each ϕ ∈ LDETL and each w ∈ W M , we have that M [U ], (w, s) |= ϕ if and only if M, w |= ϕ. • If U is past-preserving and non–past-spliting, s ∈ W U satisfies dUY (s) = n, and w ∈ W M satisfies M, w |= pU (s), then for each ϕ ∈ LDETL , we have that M [U ], (w, s) |= hY in ϕ if and only if M, w |= ϕ.

Theorem 5.5 tells us that past states play the role of “maintaining a link to the past” within past-preserving, non–past-splitting update frames. In particular, if s is a past state, then the submodel of M [U ] consisting of the worlds of the form (w, s) for some world w ∈ W M is LDETL -indistinguishable from the Kripke model M itself. So the operation (M, w) 7→
M [U ], (w, s) retains a copy of the “past” state of affairs (M, w). Furthermore, if U is past-preserving, then from any world in W M [U ] , there is a finite sequence of Y -arrows that leads back to this “past” state of affairs, thereby “maintaining a link to the past.” Let us now examine the preservation of properties of the Kripke model M in the presence of the operation M 7→ M [U ]. Theorem 5.6 (Preservation). Let U be an update frame and M be a Kripke model such that M, w |= pU (s) for some w ∈ W M and s ∈ W U . • Y -DD Preservation: if M is Y -DD and U is depth-respecting, then M [U ] is Y -DD.

• Synchronicity Preservation: if M is synchronous and U is depth-respecting, pastpreserving, and Y -synchronous, then M [U ] is synchronous. • Non–Past-Branching Preservation: if M is non–past-branching and U is non–pastsplitting, then M [U ] is non–past-branching. • Forest-likeness Preservation: if M is forest-like and U is depth-respecting and non– past-splitting, then M [U ] is forest-like. • Memory Preservation: if M is memory-preserving and U is depth-respecting, pastpreserving, non–past-splitting, and Y –memory-preserving, then M [U ] is memory-preserving. 12

6

Embedding Standard DEL

In this section, we show that standard (Temporal) Dynamic Epistemic Logic, whose update modals contain neither Y - nor Y -arrows, can be embedded in our framework in a natural way. This provides clear connections between our work and the work in [6, 10, 11, 12, 15] on (Temporal) Dynamic Epistemic Logic, which will be described at the end of this section. Definition 6.1 (Standard). Choose T ∈ {Y, Y }. To say that a Kripke frame F for A∪{Y, T } is standard means that the set W F of worlds in F does not contain the special symbol [ and F (s) = ∅. To say that a Kripke model for each s ∈ W F and each m ∈ {Y, T }, we have Rm or an L-update frame is standard means that the Kripke frame underlying that model or Lupdate frame is standard. To say that a pointed Kripke model or a pointed L-update frame is standard means that the Kripke model or L-update frame making up the first component of the pair is standard. Notation 6.2 (Sequences). Let τ be a finite possibly empty sequence. We write τ · x to denote the sequence obtained from τ by adding x at the end. |τ | denotes the number of elements in τ . When convenient, we shall use the empty set symbol ∅ to denote the empty sequence. For each integer k ∈ Z, we define the sequence τk as follows: τk = ∅ if k < 0, τk is τ if |τ | ≤ k, and τk is the prefix of τ having k elements if 0 ≤ k < |τ |.

6.1

Temporal Dynamic Epistemic Logic

The language LTDEL of Temporal Dynamic Epistemic Logic [6, 11, 12] adds to the language LSETL of Simple Epistemic Temporal Logic update modals [U, s] whose update frames U are standard. Definition 6.3 (LTDEL ; [6]). LTDEL is the Language of Temporal Dynamic Epistemic Logic. The LTDEL -formulas are the formulas that may be formed by the grammar obtained from that in Definition 2.4 (the definition of LSETL ) by adding the following formula-formation rule: if ϕ is an LTDEL -formula and (U, s) is a standard pointed L-update frame with ∅ = 6 L ⊆ LTDEL , then [U, s]ϕ is an LTDEL -formula. LTDEL consists of the LTDEL -formulas along with the Lupdate frames for which ∅ = 6 L ⊆ LTDEL .

LTDEL makes explicit the external notion of time that is present in standard Dynamic Epistemic Logic. In particular, LTDEL -formulas are evaluated using certain sequences of Kripke models, which allows us to identify the amount of time that has passed with how far along the current position is in the sequence. Definition 6.4 (Runs; projection functions π1 , π2 ; adapted from [8, 10, 11, 12, 15]). A run is a nonempty finite sequence {Mi }ni=0 of standard Kripke models satisfying the property that for each i ∈ N with 0 < i ≤ n and each w ∈ W Mi , we have that w is a pair (v, s) for which v ∈ W Mi−1 . For an arbitrary pair (x1 , x2 ), we define the projection functions π1 and def def π2 by setting π1 (x1 , x2 ) = x1 and π2 (x1 , x2 ) = x2 . Hence for a run {Mi }ni=0 and a world w ∈ W Mi such that i ∈ N and 0 < i ≤ n, we have that π1 (w) ∈ W Mi−1 . For each k ∈ N and each i ∈ {1, 2}, we define the iterated projection function πik by ( x if k = 0 or x is not a pair, def πik (x) = k−1 πi (πi (x)) otherwise. 13

Hence for a run {Mi }ni=0 and a world w ∈ W Mi such that i ∈ N and 0 < i ≤ n, for each k ∈ N with k ≤ n, we have that π1k (w) ∈ W Mi−k . A pointed run is a pair (r · M, w) consisting of a run r · M and a world w ∈ W M ; the world w is called the point of (r · M, w). Definition 6.5 (LTDEL -Truth; [6, 11, 12]). We define a notion of truth for LTDEL -formulas at pointed runs (r · M, w) by an induction on the construction of LTDEL -formulas. • r · M, w 6|=LTDEL ⊥ and r · M, w |=LTDEL >. • r · M, w |=LTDEL pk means that w ∈ V M (pk ). • r · M, w |=LTDEL ϕ ? ψ means that r · M, w |=LTDEL ϕ star r · M, w |=LTDEL ψ, where “star” is to be replaced by the (mathematical) English reading for the binary Boolean connective ?. • r · M, w |=LTDEL ¬ϕ means that r · M, w 6|=LTDEL ϕ. • For a ∈ A: r · M, w |=LTDEL [a]ϕ means that r · M, x |=LTDEL ϕ for each x ∈ RaM (w). • r · M, w |=LTDEL [Y ]ϕ means that if |r| > 0, then r, π1 (w) |=LTDEL ϕ. • r · M, w |=LTDEL [U, s]ϕ means that if we have r · M, w |=LTDEL pU (s), then, letting def r0 = r · M , it follows that r0 · r0 [U ], (w, s) |=LTDEL ϕ, where r0 [U ] is the standard Kripke model defined as follows. 0

def

W r [U ] = {(x, t) ∈ W M × W U | r0 , x |=LTDEL pU (t)}

For a ∈ A : r0 [U ]

Ra

r0 [U ]

RY

0

0

def

(x, t) = {(y, u) ∈ W r [U ] | y ∈ RaM (x) and u ∈ RaU (t)} def

(x, t) = ∅

0

def

V r [U ] (pk ) = {(x, t) ∈ W r [U ] | r0 , x |=LTDEL pk } Validity for LTDEL is defined just as is validity for LDETL (Definition 3.1), except that each subscript LDETL is replaced by a subscript LTDEL . When it ought not cause confusion, we may omit the subscript “LTDEL ” in writing |=LTDEL . The ↓ operation, which we will define in a moment, provides a connection between LTDEL truth and LDETL -truth for LSETL -formulas. This connection is described by the Collapse Lemma (Lemma 6.7). Definition 6.6 (↓). Let r = {Mi }ni=0 be a run. We define the Kripke model r↓ as follows. W r↓

def

=

def

Rar↓ (v) =

Sn

Mi i=0 W RaMi (v), where

( RYr↓ (v) =

def

a ∈ A and v ∈ W Mi

{π1 (v)} if v ∈ W Mi and i > 0, ∅

otherwise.

14

q•

= q if q ∈ {pk , ⊥, >}

(ϕ ? ψ)•

= ϕ• ? ψ •

(¬ϕ)•

= ¬(ϕ• )

([a]ϕ)• ([Y ]ϕ)• ([U, s]q)• ([U, s](ϕ ? ψ))• ([U, s]¬ϕ)• ([U, s][a]ϕ)• ([U, s][Y ]ϕ)•

= [a](ϕ• ) if a ∈ A = [Y ](ϕ• )

= (pU (s))• → q if q ∈ {pk , ⊥, >} = ([U, s]ϕ)• ? ([U, s]ψ)•

= (pU (s))• → ¬([U, s]ϕ)• V = (pU (s))• → s0 ∈RaU (s) [a]([U, s0 ]ϕ)• if a ∈ A = (pU (s))• → ϕ•

([U, s][U 0 , s0 ]ϕ)• = ([U, s]([U 0 , s0 ]ϕ)• )• Figure 4: Function • taking LTDEL -formulas to LSETL -formulas, Theorem 6.8 Lemma 6.7 (Collapse). For each pointed run (r, w) and each ϕ ∈ LSETL , we have r, w |=LTDEL ϕ if and only if r↓, w |=LDETL ϕ. We conclude this subsection with the LTDEL Reduction Theorem, which tells us that every LTDEL -formula is equivalent to an LSETL -formula. Theorem 6.8 (LTDEL Reduction). The equations in Figure 4 define a function that maps each LTDEL -formula ϕ to an LSETL -formula ϕ• such that |=LTDEL ϕ ≡ ϕ• . Further, the equations in Figure 4 are complexity-respecting: for each equation in Figure 4, • is applied on the left-hand side to a formula whose complexity is strictly larger than that of any formula on the right-hand side to which • is applied.

6.2

Embedding Generated Standard DEL Structures

In this subsection, we prove that standard (Temporal) Dynamic Epistemic Logic is closely connected with our Dynamic Epistemic Temporal Logic. In particular, we show that the process of generating runs in LTDEL from standard Kripke models can be done in an isomorphic manner within LDETL . This shows that the framework of standard (Temporal) Dynamic Epistemic Logic can be embedded within our framework of Dynamic Epistemic Temporal Logic in a natural manner. To show this, we begin with a few preliminary definitions. Definition 6.9 (Adapted from [8, 10, 11, 12, 15]). An L event-run is a finite possibly empty sequence {(Ui , si )}ni=1 of pointed L-update frames. A standard L event-run is an L event-run whose constituent pointed L-update frames are all standard. Definition 6.10 (Generated Structures). Let (M, w) be a standard pointed Kripke model. • Let σ = {(Ui , si )}ni=1 be an LDETL event-run. We define
˙ m(M, w, σ), m(M, w, σ) , 15

called the pointed Kripke model generated from (M, w) by σ, to be the pointed Kripke model (Mm , wm ) appearing at the end of the sequence {(Mi , wi )}m i=0 having the largest integer m ≤ n subject to the following conditions: (M0 , w0 ) = (M, w) and for each j ∈ N with j < m, we have – Mj , wj |=LDETL pUj+1 (sj+1 ) and


– (Mj+1 , wj+1 ) = Mj [Uj+1 ], (wj , sj+1 ) . Note: “|=LDETL ” and Mj [Uj+1 ] are given by LDETL -truth (Definition 3.1). • Let σ = {(Ui , si )}ni=1 be a standard LTDEL event-run. We define
r(M, w, σ), r˙ (M, w, σ) , called the pointed run generated from (M, w) by σ, to be the pointed run ({Mi }m i=0 , wm ) obtained from the sequence {(Mi , wi )}m of pointed Kripke models having the largest i=0 integer m ≤ n subject to the following conditions: (M0 , w0 ) = (M, w) and for each j ∈ N with j < m, we have – {Mi }ji=0 , wj |=LTDEL pUj+1 (sj+1 ) and


– (Mj+1 , wj+1 ) = {Mi }ji=0 [Uj+1 ], (wj , sj+1 ) .

Note: “|=LTDEL ” and {Mi }ji=0 [Uj+1 ] are given by LTDEL -truth (Definition 6.5). In the remainder of this subsection, we will show that a pointed run generated from a standard Kripke model (M, w) by a standard LTDEL event-run σ is isomorphic with a pointed Kripke model generated from (M, w) by a LDETL event-run σ ] built from σ. This ]-translation will also provide mappings between LTDEL -formulas and LDETL -formulas in a way that preserves formula truth under the isomorphism. Accordingly, we shall see that standard (Temporal) Dynamic Epistemic Logic is naturally embedded within our framework of Dynamic Epistemic Temporal Logic. Proceeding, we begin by defining the ]-translation. Definition 6.11 (]n, ]). For n ∈ N, we define the function ]n : LTDEL → LDETL in Figure 5. def ](i−1) If σ = {(Ui , si )}ni=1 is a standard LTDEL event-run, then we define σ ] = {(Ui , si )}ni=1 . For synchronous, non–past-branching Kripke models, there is a natural connection (described in the Connection Lemma, Lemma 6.12) between the LDETL -reduced ]-translation of a LTDEL -formula ϕ and the LTDEL -reduced version of ϕ. This connection plays a crucial role in the proof of our key result: the Isomorphism Theorem (Theorem 6.13). Lemma 6.12 (Connection). For each formula ϕ ∈ LTDEL , each synchronous and non–pastbranching Kripke model M , and each n ∈ N, we have
M |=LDETL hY in [Y ]⊥ → (ϕ]n )◦ ≡ ϕ• . Theorem 6.13 (Isomorphism). Let (M, w) be a standard pointed Kripke model and let σ def be a standard LTDEL event-run. Defining m = |r(M, w, σ)| − 1, we have each of the following. 16

def

q ]n = q if q ∈ {pk , ⊥, >} def

(ϕ ? ψ)]n = ϕ]n ? ψ ]n def

(¬ϕ)]n = ¬(ϕ]n ) def

([a]ϕ)]n = [a](ϕ]n ) if a ∈ A def

([Y ]ϕ)]0 = [Y ]ϕ]0 def

([Y ]ϕ)]n = [Y ]ϕ](n−1) if n > 0 def

([U, s]ϕ)]n = [U ]n, s](ϕ](n+1) ) def

W U ]n = W U ] {[} (disjoint union)  U Ra (s) if a 6= Y and s 6= [, for a ∈ A ∪ {Y, Y },    {[} if a 6= Y and s = [, def RaU ]n (s) =  {[} if a = Y and s 6= [,    if a = Y and s = [. (∅ def

pU ]n (s) =

(pU (s))]n ∧ hY in [Y ]⊥ if s 6= [, > if s = [.

Figure 5: Definition of ]n : LTDEL → LDETL for n ∈ N ˙ 1. (r(M, w, σ)↓, r˙ (M, w, σ)) and (m(M, w, σ ] ), m(M, w, σ ] )) are isomorphic.7 2. For each ϕ ∈ LTDEL , the following are equivalent. (a) r(M, w, σ), r˙ (M, w, σ) |=LTDEL ϕ.

˙ (b) m(M, w, σ ] ), m(M, w, σ ] ) |=LDETL ϕ]m . The Isomorphism Theorem (Theorem 6.13) provides a strong connection between runs generated in a standard (Temporal) Dynamic Epistemic Logic setting and certain Kripke models generated in our Dynamic Epistemic Temporal Logic setting. In particular, [11, 12] studies certain structural properties of the forest structure given by a run r(M, w, σ) generated from a standard pointed Kripke model (M, w) by a standard LSETL event-run σ. For example, in [11, 12], the authors of define what it means for the run r(M, w, σ) to be synchronous (among other properties) and then show that every run generated from a standard pointed Kripke model by a standard LSETL event-run is synchronous.8 Our Preservation Theorem (Theorem 5.6) works together with the Isomorphism Theorem (Theorem 6.13) to 7

To say that two (pointed) Kripke models are isomorphic means that there exists an isomorphism between 0 them. An isomorphism between Kripke models M and M 0 is a bijection f : W M → W M satisfying each 0 of the following: (i) v ∈ V M (pk ) if and only if f (v) ∈ V M (pk ) for each k ∈ N, and (ii) u ∈ RaM (v) if and 0 only if f (u) ∈ RaM (f (v)) for each a ∈ A ∪ {Y }. An isomorphism between pointed Kripke models (M, w) and (M 0 , w0 ) is an isomorphism f between M and M 0 for which f (w) = w0 . See [4] for more information. 8 If r(M, w, σ) is a run generated from a standard pointed Kripke model (M, w) by a standard LSETL event-run σ, then the definition in [11, 12] would have us say that r(M, w, σ) is synchronous if and only if r(M, w, σ)↓ is synchronous (according to our Definition 5.3).

17

provide a different perspective on this synchronicity result (and on the other results in those papers). In particular, our work shows that the results of [11, 12] can be viewed as a consequence of the structural properties that are present in the update frame U ]n produced from a standard update frame U , thereby pinpointing the source of their result: synchronicity is a necessary consequence of the ]-translation.

7

Conclusion

In its technical essence, this paper is about studying what we can do when we extend the standard Dynamic Epistemic Logic operation M 7→ M [U ] [1, 3] to epistemic temporal models using our Y -arrow mechanism. Essentially, the Y -arrow describes a sufficient condition for the creation of Y -arrows in the model M [U ]: when there is a Y -arrow in the update frame U from state s to state s0 , there will be a Y -arrow in M [U ] from world (x, s) to world (x, s0 ). Another way to understand this is by way of the hybrid scheme ^
[U, s][a]ϕ ≡ pU (s) → ∀z. aUa (s, s0 ) → @z (pU (s0 ) → [U, s0 ]ϕ) , s0 ∈W U

where aUa is a function mapping each modal label a and each pair (s, s0 ) of states in U to a formula aUa (s, s0 ) that may contain the free variable z. This scheme uses the formula aUa (s, s0 ) to describe the precondition for the creation of a-arrows. For example, the standard Dynamic Epistemic Logic precondition for the creation of a-arrows is given by setting ( haiz if s0 ∈ RaU (s), def aUa (s, s0 ) = ⊥ if s0 ∈ / RaU (s), which ensures that there is an a-arrow in M [U ] from world (x, s) to world (x0 , s0 ) if and only if there is an a-arrow both in U from state s to state s0 and in M from world x to world x0 . In Dynamic Epistemic Temporal Logic, the precondition aUY (s, s0 ) for the creation of Y -arrows is given by setting  z ∨ hY iz if s0 ∈ RYU (s) and s0 ∈ RYU (s),    z if s0 ∈ RYU (s) and s0 ∈ / RYU (s), U 0 def aY (s, s ) = hY iz if s0 ∈ / RYU (s) and s0 ∈ RYU (s),    ⊥ if s0 ∈ / RYU (s) and s0 ∈ / RYU (s), which takes the standard Dynamic Epistemic Logic precondition hY iz as sufficient for Y arrow creation if there is a Y -arrow in U from s to s0 and takes our new Dynamic Epistemic Temporal Logic precondition z as sufficient for Y -arrow creation if there is a Y -arrow in U from s to s0 . This way of understanding our work suggests one natural direction for future work: the study of other interesting sufficiency conditions (for example, the condition aUa (s, s0 ) = > always creates an a-arrow from world (x, s) to world (x0 , s0 ), making it so that agent a entertains new possibilities that she may not have entertained before). But in our view, the main contribution of this paper is our introduction of Dynamic Epistemic Temporal Logic as a dynamic-protocol framework that avoids the Problem of Synchronicity. Dynamic Epistemic Temporal Logic extends the updates of Dynamic Epistemic 18

Logic so that they operate not just on epistemic models (having an external notion of time) but also on epistemic temporal models (having an internal notion of time) in a way that allows us to control how an update affects the time of worlds in the model M [U ]. We presented two scenarios contrasting synchronous and asynchronous private announcements. This contrast indicates how it is that our framework can be used to reason about discretetime multi-agent distributed systems that need not be synchronous, thereby illustrating how our framework avoids the Problem of Synchronicity. We then studied sufficient conditions for the preservation of various properties of Kripke models, such as synchronicity. Identifying an isomorphism that connects epistemic temporal models generated in our framework with epistemic temporal models generated by standard updates as in [11, 12], we saw that the necessity of synchronicity in standardly generated epistemic temporal models stems from the structure that standard updates possess from the perspective of Dynamic Epistemic Temporal Logic. This analysis not only clarifies the way in which these preservation results arise but it also provides us with a natural and elegant solution to the Problem of Synchronicity in Dynamic Epistemic Logic. For these reasons, we propose the Y -arrow mechanism as a straightforward and simple means of bringing temporal considerations within the reach of the Dynamic Epistemic Logic framework. The payoff of our approach is a framework that uses dynamic protocols in harmony with the internal time-keeping mechanism of (Simple) Epistemic Temporal Logic, thereby avoiding the Problem of Synchronicity in a dynamic-protocol framework.

A A.1

Appendix: the Proofs Proof of the LDETL Reduction Theorem (Theorem 2.8)

Theorem. The equations in Figure 2 define a function that maps each LDETL -formula ϕ to an LSETL -formula ϕ◦ such that ` ϕ ≡ ϕ◦ . Further, the equations in Figure 2 are complexityrespecting: for each equation in Figure 2, ◦ is applied on the left-hand side to a formula whose complexity is strictly larger than that of any formula on the right-hand side to which ◦ is applied. Proof. To show that equations in Figure 2 define a function that takes each LDETL -formula ϕ to an LSETL -formula ϕ◦ , we argue by induction on n ∈ N+ that the equations in Figure 2 define a function ◦n mapping LnDETL -formulas to LSETL -formulas.9 We then define a function def ◦ mapping LDETL -formulas to LSETL -formulas by setting ϕ◦ = ϕ◦c(ϕ) and argue that ◦ is the unique function satisfying the equations in Figure 2.10 Along the way, it is shown that the 9

In a bit more detail, the equations defining ◦n are obtained from those in Figure 2 as follows: the ◦ on the left-hand side of an equation is to be replaced by ◦n , each ◦ on the right-hand side of an equation is to be replaced by ◦n−1 , and any equation that then contains ◦n−1 on its right-hand side with n − 1 ≤ 0 is to be omitted. We then see that ◦1 is well-defined, and we show that ◦n+1 is well-defined if ◦n is well-defined. The latter requires us to prove that our equations in Figure 2 are complexity-respecting. So by induction on n, we conclude that ◦n is well-defined for each n ∈ N+ . 10 In a bit more detail, making frequent use of the fact that the equations in Figure 2 are complexityrespecting, we proceed in the following way. First, we argue by induction on n ∈ N+ that for each ϕ ∈ LnDETL def and each k ∈ N, we have ϕ◦c(ϕ) = ϕ◦c(ϕ)+k . Using this, we argue that the function ◦ defined by ϕ◦ = ϕ◦c(ϕ)

19

equations in Figure 2 are complexity-respecting. We then argue by induction on n ∈ N+ that for each ϕ ∈ LnDETL , we have ` ϕ ≡ ϕ◦ . The argument is a straightforward adaptation of the standard argument in Dynamic Epistemic Logic [14].

A.2

Proof of the Correctness Theorem (Theorem 3.2)

Theorem. For each formula ϕ, we have ` ϕ if and only if |= ϕ. Proof. All but one case of the soundness argument (` ϕ implies |= ϕ) are straightforward adaptations of the standard Dynamic Epistemic Logic arguments [14], so we shall only prove this one case here. Proceeding, we are to show that V (2) |= [U, s][Y ]ϕ ≡ (pU (s) → s0 ∈RU (s) [Y ][U, s0 ]ϕ) ∧ Y V (pU (s) → s0 ∈RU (s) [U, s0 ]ϕ) . Y

Let us first prove the left-to-right direction of this equivalence. So assuming M, w |= [U, s][Y ][ϕ] and M, w |= pU (s) and choosing t ∈ RYU (s) and u ∈ RYU (s) arbitrarily, we prove that M, w |= [Y ][U, t]ϕ and M, w |= [U, u]ϕ. It follows from our assumptions by the M [U ] definition of truth that M [U ], (w0 , s0 ) |= ϕ for each (w0 , s0 ) ∈ RY (w, s). If v ∈ RYM (w) M [U ] and M, v |= pU (t), then (v, t) ∈ RY (w, s) and hence M [U ], (v, t) |= ϕ. We therefore have M [U ] that M, w |= [Y ][U, t]ϕ. Further, if M, w |= pU (u), then (w, u) ∈ RY (w, s) and hence M [U ], (w, u) |= ϕ. We therefore have that M, w |= [U, t]ϕ. This completes the left-to-right direction of the equivalence (2). We now show the right-to-left direction of the equivalence (2). So assuming M, w |= pU (s), M, w |= [Y ][U, t]ϕ for each t ∈ RYU (s), and M, w |= [U, u]ϕ for each u ∈ RYU (s), we M [U ] prove that M [U ], (w, s) |= [Y ]ϕ. So choose (w0 , s0 ) ∈ RY (w, s) arbitrarily, from which it follows that M, w0 |= pU (s0 ). If w0 ∈ RYM (w) and s0 ∈ RYM (s), then we have that M, w |= [Y ][U, s0 ]ϕ and hence that M [U ], (w0 , s0 ) |= ϕ. If it is not the case that w0 ∈ RYM (w) and s0 ∈ RYM (s), then it must be that w0 = w and s0 ∈ RYM (s), from which it follows that M [U ], (w0 , s0 ) |= ϕ. So we have shown that we have M [U ], (w0 , s0 ) |= ϕ for each (w0 , s0 ) ∈ M [U ] RY (w, s), from which it follows that M [U ], (w, s) |= [Y ]ϕ. This completes the right-to-left direction of the equivalence (2). We have therefore shown that Axiom U [Y ] is valid. The completeness argument (|= ϕ implies ` ϕ) follows by the LDETL Reduction Theorem, the standard modal logic canonical model argument for the language LSETL [4], and the combination of the LDETL Reduction Theorem with the soundness argument.

A.3

Proof of the Past State Theorem (Theorem 5.5)

Theorem. Let U be an update frame and M be a Kripke model. • If s is a past state in U , then for each ϕ ∈ LDETL and each w ∈ W M , we have that M [U ], (w, s) |= ϕ if and only if M, w |= ϕ. satisfies the equations in Figure 2. Finally, we argue by induction on n ∈ N+ that if † is another function satisfying the equations in Figure 2, then ϕ† = ϕ◦ for each ϕ ∈ LnDETL .

20

• If U is past-preserving and non–past-spliting, s ∈ W U satisfies dUY (s) = n, and w ∈ W M satisfies M, w |= pU (s), then for each ϕ ∈ LDETL , we have that M [U ], (w, s) |= hY in ϕ if and only if M, w |= ϕ. Proof. We first prove the first item of this theorem. Let s ∈ W U be a past state and let w ∈ W M be a world. Applying the LDETL Reduction Theorem (Theorem 2.8) and the Correctness Theorem (Theorem 3.2), it sufficies for us to prove that M [U ], (w, s) |= ϕ if and only if M, w |= ϕ for each LSETL -formula ϕ. But this follows by observing that the definitions of past state and LDETL -truth imply that the unraveling of the pointed Kripke
model (M, w) is isomorphic to the unraveling of the pointed Kripke model M [U ], (w, s) [4]. We now proceed to the proof of the second item of this theorem. Suppose that U is past-preserving and non–past-splitting, s ∈ W U satisfies dUY (s) = n, and w ∈ W M satisfies M, w |= pU (s). Since U is past-preserving and dUY (s) = n, there is a path-preserving Y def history σ = {si }ni=0 in U that begins at s and ends at a past state. Since M, w |= pU (s), it follows from the fact that σ is path-preserving that M, w |= pU (si ) for each i ∈ N with i ≤ n. Applying LDETL -truth and the fact that U is past-preserving (and hence path-preserving), def we then have that σ 0 = {(w, si )}ni=0 is a Y -history in M [U ]. Since U is non–past-splitting, it follows that σ 0 is the unique Y -run in M [U ] that begins at (w, s) and has length n. We therefore have that M [U ], (w, s) |= hY in ϕ if and only if M [U ], (w, sn ) |= ϕ for each ϕ ∈ LDETL . Since sn is a past state, we then have by the first item of this theorem that M [U ], (w, sn ) |= ϕ if and only if M, w |= ϕ for each ϕ ∈ LDETL . The result follows.

A.4

Proof of the Preservation Theorem (Theorem 5.6)

Theorem. Let U be an update frame and M be a Kripke model such that M, w |= pU (s) for some w ∈ W M and s ∈ W U . • Y -DD Preservation: if M is Y -DD and U is depth-respecting, then M [U ] is Y -DD. • Synchronicity Preservation: if M is synchronous and U is depth-respecting, pastpreserving, and Y -synchronous, then M [U ] is synchronous. • Non–Past-Branching Preservation: if M is non–past-branching and U is non–pastsplitting, then M [U ] is non–past-branching. • Forest-likeness Preservation: if M is forest-like and U is depth-respecting and non– past-splitting, then M [U ] is forest-like. • Memory Preservation: if M is memory-preserving and U is depth-respecting, pastpreserving, non–past-splitting, and Y –memory-preserving, then M [U ] is memory-preserving. Proof. We prove each item in turn. • Y -DD Preservation: if M is Y -DD and U is depth-respecting, then M [U ] is Y -DD.

Assume that M is a Y -DD Kripke model and that U is a depth-respecting (and hence M Y -DD) update frame. We then have that dM and that Y (w) ∈ N for each world w ∈ W U U dY (s) ∈ N for each state s ∈ W . So to show that M [U ] is Y -DD, it suffices for us to 21

M [U ]

U M [U ] prove that dY (w, s) ≤ dM . The argument is by Y (w) + dY (s) for each (w, s) ∈ W U M an induction on the sum dY (w) + dY (s) ∈ N that breaks up into two cases: w0 = w and w0 6= w. We omit the details due to space constraints.

• Synchronicity Preservation: if M is synchronous and U is depth-respecting, pastpreserving, and Y -synchronous, then M [U ] is synchronous. Let us first assume the following claim: if M is synchronous (and hence Y -DD) and U is depth-respecting (and hence Y -DD), past-preserving, and Y -synchronous, then M [U ] U M [U ] dY (w, s) = dM . Proceeding under the assumpY (w) + dY (s) for each (w, s) ∈ W M [U ] tion of this claim, if we have that (w0 , s0 ) ∈ Ra (w, s) with a ∈ A, it follows that M 0 w0 ∈ RaM (w) and s0 ∈ RaU (s) by LDETL -truth. But since we have that dM Y (w) = dY (w ) by the synchronicity of M and that dUY (s) = dUY (s0 ) by the Y -synchronicity of U , it M [U ] M [U ] follows by the claim that dY (w, s) = dY (w0 , s0 ), which is what we wished to show. So all that remains is for us to prove the claim. Now we showed in the above argument for Y -DD Preservation that having M synchronous (and hence Y -DD) and U depthM [U ] U respecting (and hence Y -DD) all together imply dY (w, s) ≤ dM Y (w) + dY (s) for each (w, s) ∈ W M [U ] . So it suffices for us to show that the additional condition of synchronicity on M and the additional conditions of past-preservation and Y -synchronicity on U M [U ] U (w, s) for each (w, s) ∈ W M [U ] . This is all together imply that dM Y (w) + dY (s) ≤ dY U argued by induction on the sum dM Y (w) + dY (s) ∈ N; in the induction step, we consider two cases: RYU (s) 6= ∅ and RYU (s) = ∅. We omit the details due to space constraints. • Non–Past-Branching Preservation: if M is non–past-branching and U is non–pastsplitting, then M [U ] is non–past-branching. Suppose that U is non–past-splitting and that M is non–past-branching. Given an M [U ] arbitrary (w, s) ∈ W M [U ] , we wish to show that RY (w, s) contains at most one member. We argue this by showing that under the membership assumptions (w1 , s1 ) ∈ M [U ] M [U ] RY (w, s) and (w2 , s2 ) ∈ RY (w, s), we have that (w1 , s1 ) = (w2 , s2 ). Proceeding with these membership assumptions, it follows by LDETL -truth that we have relations R1 ∈ {RYU , RYU } and R2 ∈ {RYU , RYU } such that s1 ∈ R1 (s) and s2 ∈ R2 (s). But to have U non–past-splitting means that RYU (s) ∪ RYU (s) contains at most one member and that RYU (s) ∩ RYU (s) = ∅. It therefore follows that R1 = R2 and that s1 = s2 . Now if R1 = R2 = RYU , then it follows that w1 = w = w2 by LDETL -truth and our membership assumptions. Otherwise, if R1 = R2 = RYU , then it follows that w1 ∈ RYM (w) and w2 ∈ RYM (w) by LDETL -truth and our membership assumptions, and we again conclude that w1 = w2 because M is non–past-branching. We therefore conclude that (w1 , s1 ) = (w2 , s2 ). • Forest-likeness Preservation: if M is forest-like and U is depth-respecting and non– past-splitting, then M [U ] is forest-like. A forest-like Kripke model is a Kripke model that is Y -DD and non–past-branching. The proof therefore follows by our arguments on Y -DD Preservation and Non–PastBranching Preservation. 22

• Memory Preservation: if M is memory-preserving and U is depth-respecting, pastpreserving, non–past-splitting, and Y –memory-preserving, then M [U ] is memory-preserving. Suppose that M is memory-preserving (and hence Y -DD) and that U is depth-respecting, past-preserving, non–past-splitting, and Y –memory-preserving. M [U ] is memorypreserving if we have (1) that M [U ] is Y -DD, and (2) that for each a ∈ A, each M [U ] M [U ] (w, s) ∈ W M [U ] , each (v, t) ∈ Ra (w, s), and each (w0 , s0 ) ∈ RY (w, s), there is a M [U ] M [U ] world (v 0 , t0 ) ∈ Ra (w0 , s0 ) ∩ (RY )∗ (v, t). Item (1) follows immediately from our assumptions by our argument in the previous item on Y -DD Preservation. So all that remains is for us to prove Item (2), which we express for convenience using the following diagram. (w ′ , s′ )

Y

(w, s)

a

a

(v ′ , t′ )

(v, t)

Y∗

Proceeding with our proof of Item (2), suppose we are given (w, s) ∈ W M [U ] , (v, t) ∈ M [U ] M [U ] Ra (w, s), and (w0 , s0 ) ∈ RY (w, s). It follows by LDETL -truth that v ∈ RaM (w) and t ∈ RaU (s). Our argument now breaks up into two cases. – Case: s0 ∈ RYU (s).

Since U is Y –memory-preserving, there exists a t0 ∈ RaU (s0 ) ∩ (RYU )∗ (t): s′

Y

s a

a

t′

Y∗

t

Since U is past-preserving, it follows that (v, t0 ) ∈ W M [U ] . Applying LDETL -truth, M [U ] M [U ] we then have that (v, t0 ) ∈ (RY )∗ (v, t) and (v, t0 ) ∈ Ra (w, s0 ): (w, s′)

Y

a

(w, s) a

(v, t′)

Y∗

(v, t)

Conclusion: M [U ] is Y –memory-preserving. – Case: s0 ∈ / RYU (s)

In this case, it follows by LDETL -truth that w0 ∈ RYM (w) and s0 ∈ RYU (s). Since M is Y –memory-preserving there exists a v 0 ∈ RaM (w0 ) ∩ (RYM )∗ (v):

23

w′

Y

w

a

a

v

′

Y∗

v

Since U is past-preserving, the singleton Y -run {s} can be end-extended to a Y -history σ that ends at a past state. Since s0 ∈ RYU (s) and U is non–pastsplitting, RYU (s) = ∅. We therefore have that σ = {s} and hence that s is itself a past state. Applying LDETL -truth and the definition of past state, it follows that s0 = s = t, that |= pU (s) ≡ >, that s ∈ RaU (s), and that s ∈ RYU (s). Applying M [U ] LDETL -truth, it then follows that (v 0 , s) ∈ W [U ] , that (v 0 , s) ∈ (RY )∗ (v, s), and M [U ] that (v 0 , s) ∈ Ra (w0 , s): (w ′, s)

Y

a

(w, s) a

(v ′ , s)

Y∗

(v, s)

Conclusion: M [U ] is Y –memory-preserving.

A.5

Proof of the Collapse Lemma (Lemma 6.7)

Lemma. For each pointed run (r, w) and each ϕ ∈ LSETL , we have r, w |=LTDEL ϕ if and only if r↓, w |=LDETL ϕ. Proof. This can be proved by induction on the construction of ϕ ∈ LSETL . The key case is M2 ϕ = [Y ]ψ, which makes use of the fact that r1 = r2 ·M2 , w ∈ W M1 , and π1 (w)
∈ W together imply that the unraveling of the pointed Kripke model (r2
· M2 )↓, π1 (w) is isomorphic to the unraveling of the pointed Kripke model (r1 ·M1 )↓, π1 (w) [4]. Since ψ ∈ LSETL , it follows that (r2 · M2 )↓, π1 (w) |=LDETL ψ is equivalent to (r1 · M1 )↓, π1 (w) |=LDETL ψ if r1 = r2 · M2 . The induction hypothesis is then applied to the left side of this equivalence.

A.6

Proof of the LTDEL Reduction Theorem (Theorem 6.8)

Theorem. The equations in Figure 4 define a function that maps each LTDEL -formula ϕ to an LSETL -formula ϕ• such that |=LTDEL ϕ ≡ ϕ• . Further, the equations in Figure 4 are complexity-respecting: for each equation in Figure 4, • is applied on the left-hand side to a formula whose complexity is strictly larger than that of any formula on the right-hand side to which • is applied. Proof. This proof is similar to the proof of the LDETL Reduction Theorem, Theorem 2.8, though the last part of the proof uses LTDEL -truth “|=LTDEL ” in place of provability “`”.

24

A.7

Proof of the Connection Lemma (Lemma 6.12)

Lemma. For each formula ϕ ∈ LTDEL , each synchronous and non–past-branching Kripke model M , and each n ∈ N, we have
M |=LDETL hY in [Y ]⊥ → (ϕ]n )◦ ≡ ϕ• . Proof. We argue by induction on m ∈ N+ that for each ϕ ∈ Lm TDEL (Notation 2.7), each synchronous and non–past-branching Kripke model M , and each n ∈ N, the validity in the statement of this theorem holds. Most cases are straightforward, so we shall only address the most interesting inductive cases. • Case: ϕ = [a]ψ with a ∈ A.

To begin, let us argue that M, v |=LDETL hY in [Y ]⊥ for each v ∈ RaM (w). Proceeding, M, w |=LDETL hY in [Y ]⊥ implies that there is a Y -history σ in M that begins at w and has length n. Since M is non–past-branching, σ is the unique Y -history that begins at w, and hence it follows that dM Y (w) = n. Since M is synchronous, it follows M M that dY (v) = n for each v ∈ Ra (w) and hence that M, v |=LDETL hY in [Y ]⊥ for each v ∈ RaM (w).

We now prove that M, w |=LDETL (([a]ψ)]n )◦ ≡ ([a]ψ)• . Proceeding, since c(ψ) < c([a]ψ), it follows by the induction hypothesis, our result from the previous paragraph, and LDETL -truth that M, v |=LDETL (ψ ]n )◦ ≡ ψ • for each v ∈ RaM (w). Applying LDETL truth and modal reasoning, it follows that M, w |=LDETL [a](ψ ]n )◦ ≡ [a]ψ • . Applying the definitions of ◦, ]n, and •, we conclude that M, w |=LDETL (([a]ψ)]n )◦ ≡ ([a]ψ)• . • Case: ϕ = [Y ]ψ and n = 0.

We prove that M, w |=LDETL (([Y ]ψ)]0 )◦ ≡ ([Y ]ψ)• . Proceeding, our assumption that M, w |=LDETL hY i0 [Y ]⊥ means that M, w |=LDETL [Y ]⊥ and hence that RYM (w) = ∅. It follows by LDETL -truth that M, w |=LDETL [Y ](ψ ]0 )◦ and M, w |=LDETL [Y ]ψ • and hence that M, w |=LDETL [Y ](ψ ]0 )◦ ≡ [Y ]ψ • . Applying the definitions of ◦, ]0, and •, it follows that M, w |=LDETL (([Y ]ψ)]0 )◦ ≡ ([Y ]ψ)• .

• Case: ϕ = [Y ]ψ and n > 0.

To begin, we note that our assumptions M, w |=LDETL hY in [Y ]⊥ and n > 0 together imply that RYM (w) 6= ∅ and that M, v |=LDETL hY in−1 [Y ]⊥ for each v ∈ RYM (w). Since M is non–past-branching, RYM (w) 6= ∅ implies that RYM (w) = {u} for some u ∈ W M . Hence M, u |=LDETL hY in−1 [Y ]⊥ and RYM (w) = {u}. We now prove that M, w |=LDETL (([Y ]ψ)]n )◦ ≡ ([Y ]ψ)• . Since c(ψ) < c([Y ]ψ), it follows by the induction hypothesis, the results of the previous paragraph, and LDETL -truth that M, u |=LDETL (ψ ](n−1) )◦ ≡ ψ • and RYM (w) = {u}. Applying LDETL -truth and modal reasoning, M, w |=LDETL [Y ](ψ ](n−1) )◦ ≡ [Y ]ψ • . Applying the definitions of ◦, ]n (for n > 0), and •, we conclude that M, w |=LDETL (([Y ]ψ)]n )◦ ≡ ([Y ]ψ)• .

25

• Case: ϕ = [U, s][a]χ with a ∈ A.

Choose an arbitrary v ∈ RaM (w). It follows by our argument in the case “[a]ψ” above that M, v |= hY in [Y ]⊥. (Note that this argument made use of our assumption that M is synchronous and non–past-branching.) Now choose an arbitrary s0 ∈ RaU ]n (s). Since we have that RaU ]n (s) = RaU (s) by the definition of ]n and the fact that [U, s][a]χ ∈ LTDEL (and hence that s 6= [), it follows that c([U, s0 ]χ) < c([U, s][a]χ) and thus that M, v |=LDETL (([U, s0 ]χ)]n )◦ ≡ ([U, s0 ]χ)• by the induction hypothesis and LDETL -truth. Since v ∈ RaM (w) and s0 ∈ RaU ]n (s) = RaU (s) were chosen arbitrarily, it follows by LDETL -truth, modal reasoning, and the definition of ]n that V 0 ](n+1) ◦ ) ≡ (3) M, w |=LDETL s0 ∈RaU ]n (s) [a]([U ]n, s ]χ V 0 • . U (s) [a]([U, s ]χ) s0 ∈Ra Further, since (pU ]n (s))◦ = (pU (s)]n )◦ ∧ hY in [Y ]⊥ by the definitions of ]n and ◦, and since M, w |=LDETL hY in [Y ]⊥ by LDETL -truth, it follows that M, w |=LDETL (pU (s)]n )◦ ≡ (pU ]n (s))◦ . In addition, as c(pU (s)) < c([U, s][Y ]χ), it follows by the induction hypothesis that M, w |=LDETL (pU ]n (s))◦ ≡ pU (s)• . Applying (3), it follows by LDETL -truth and the definitions of ◦, •, and ]n that M, w |=LDETL (([U, s][a]χ)]n )◦ ≡ ([U, s][a]χ)• .

• Case: ϕ = [U, s][Y ]χ.

We prove that M, w |=LDETL (([U, s][Y ]χ)]n )◦ ≡ ([U, s][Y ]χ)• . Proceeding, since [ is a past state in U ]n, it follows by LDETL -truth and the Past State Theorem (Theorem 5.5) that |=LDETL ([U ]n, []χ]n ) ≡ χ]n . It therefore follows by the LDETL Reduction Theorem (Theorem 2.8), the Correctness Theorem (Theorem 3.2), and the definition of ◦ that |=LDETL ([U ]n, []χ]n )◦ ≡ (χ]n )◦ . Since we have that c(χ) < c([U, s][Y ]χ) and that M, w |=LDETL hY in [Y ]⊥, it follows by the induction hypothesis and LDETL -truth that M, w |=LDETL (χ]n )◦ ≡ χ• . Hence M, w |=LDETL ([U ]n, []χ]n )◦ ≡ χ• . Since we have c(pU (s)) < c([U, s][Y ]χ) and M, w |=LDETL hY in [Y ]⊥, the induction hypothesis and LDETL -truth imply that M, w |=LDETL (pU (s)]n )◦ ≡ pU (s)• . Combining this with our result from two sentences ago, we have that
M, w |=LDETL (pU (s)]n )◦ → ([U ]n, []χ]n )◦ ≡ (pU (s)• → χ• ) . By the same reasoning as given in the case “[U, s][a]χ”, we have that M, w |=LDETL (pU (s)]n )◦ ≡ (pU ]n (s))◦ , whence by LDETL -truth and the definition of •, it follows that
M, w |=LDETL (pU ]n (s))◦ → ([U ]n, []χ]n )◦ ≡ ([U, s][Y ]χ)• . (4)

Further, we have that RYU ]n (s) = RYU (s) = ∅ by the definition of ]n and the fact that U ∈ LTDEL (and hence that U is standard), and we have that RYU ]n (s) = {[} by the definition of ]n. Accordingly, V 0 ]n ◦ = > and U ]n s0 ∈RY (s) [Y ]([U ]n, s ]χ ) V 0 ]n ◦ = ([U ]n, []χ]n )◦ . s0 ∈RU ]n (s) ([U ]n, s ]χ ) Y

26

It therefore follows from (4) by LTDEL -truth and the definition of ◦ that M, w |=LDETL ([U ]n, s][Y ]χ]n )◦ ≡ ([U, s][Y ]χ)• and hence that M, w |=LDETL (([U, s][Y ]χ)]n )◦ ≡ ([U, s][Y ]χ)• by the definition of ]n. • Case: ϕ = [U, s][U 0 , s0 ]χ.

M, w |= pU ]n ([) by LDETL -truth and the fact that pU ]n ([) = >. Further, U ]n is depthrespecting, past-preserving, Y -synchronous, and non–past-splitting. So since M is synchronous and non–past-branching, it follows from the Preservation Theorem (Theorem 5.6) that M [U ]n] is synchronous and non–past-branching. Since we have that c([U 0 , s0 ]χ) < c([U, s][U 0 , s0 ]χ), it follows by the induction hypothesis that M [U ]n] |=LDETL hY in+1 [Y ]⊥ →

(([U 0 , s0 ]χ)](n+1) )◦ ≡ ([U 0 , s0 ]χ)

(5)
•

.

We wish to argue that
M, w |=LDETL [U ]n, s] (([U 0 , s0 ]χ)](n+1) )◦ ≡ ([U 0 , s0 ]χ)• .

(6)

If M, w 6|=LDETL pU ]n (s), it is immediate that (6) holds. Let us assume that M, w |=LDETL pU ]n (s). Then M, w |=LDETL hY in [Y ]⊥ implies that there exists a Y -history {wi }ni=0 in M with w0 = w. So since M, w |=LDETL pU ]n (s), we have that (w, s) · {(wi , [)}ni=0 is a Y history in M [U ]n] having length n + 1. It therefore follows that M [U ]n], (w, s) |=LDETL hY in+1 [Y ]⊥ and hence that M [U ]n], (w, s) |= (([U 0 , s0 ]χ)](n+1) )◦ ≡ ([U 0 , s0 ]χ)•

(7)

by (5) and LDETL -truth. But (7) implies (6) by LDETL -truth. Applying Axiom U?, the Correctness Theorem (Theorem 3.2), and LDETL -truth, it follows from (6) that M, w |=LDETL [U ]n, s](([U 0 , s0 ]χ)](n+1) )◦ ≡ [U ]n, s]([U 0 , s0 ]χ)• . Since ([U 0 , s0 ]χ)• ∈ LSETL and δ ](n+1) = δ for each δ ∈ LSETL , we have M, w |=LDETL [U ]n, s](([U 0 , s0 ]χ)](n+1) )◦ ≡ [U ]n, s](([U 0 , s0 ]χ)• )](n+1) .

Applying the definitions of ]n and ](n + 1), we have M, w |=LDETL [U ]n, s]([U 0 ](n + 1), s0 ]χ](n+2) )◦ ≡ ([U, s]([U 0 , s0 ]χ)• )]n .

Applying the LDETL Reduction Theorem (Theorem 2.8), the Correctness Theorem, and LDETL -truth, it follows that M, w |=LDETL ([U ]n, s]([U 0 ](n + 1), s0 ]χ](n+2) )◦ )◦ ≡ (([U, s]([U 0 , s0 ]χ)• )]n )◦ . 27

Since c([U, s]([U 0 , s0 ]χ)• ) < c([U, s][U 0 , s0 ]χ), it follows by the induction hypothesis, the fact that M, w |=LDETL hY in [Y ]⊥, and LDETL -truth that M, w |=LDETL ([U ]n, s]([U 0 ](n + 1), s0 ]χ](n+2) )◦ )◦ ≡ ([U, s]([U 0 , s0 ]χ)• )• .

Applying the definitions of ◦ and •, we have M, w |=LDETL ([U ]n, s][U 0 ](n + 1), s0 ]χ](n+2) )◦ ≡ ([U, s][U 0 , s0 ]χ)• .

Applying the definitions of ](n + 1) and then the definition of ]n, we conclude that M, w |=LDETL (([U, s][U 0 , s0 ]χ)]n )◦ ≡ ([U, s][U 0 , s0 ]χ)• .

A.8

Proof of the Isomorphism Theorem (Theorem 6.13)

Theorem. Let (M, w) be a standard pointed Kripke model and let σ be a standard LTDEL def event-run. Defining m = |r(M, w, σ)| − 1, we have each of the following. ˙ 1. (r(M, w, σ)↓, r˙ (M, w, σ)) and (m(M, w, σ ] ), m(M, w, σ ] )) are isomorphic. 2. For each ϕ ∈ LTDEL , the following are equivalent. (a) r(M, w, σ), r˙ (M, w, σ) |=LTDEL ϕ.

˙ (b) m(M, w, σ ] ), m(M, w, σ ] ) |=LDETL ϕ]m . Proof. For each Y -DD Kripke model N and each pair (i, j) ∈ Z2 of integers, we define def N (i..j) = {w ∈ W N | i ≤ dN Y (w) ≤ j}. Notice that N (i..j) = ∅ if j < i or j < 0. We also let N (..j) abbreviate N (0..j) and we let N (i) abbreviate N (i..i). We fix a standard pointed Kripke model (M, w) for the remainder of the proof. Using the Preservation Theorem, it is not difficult to see that for each standard LTDEL eventrun σ, the Kripke models r(M, w, σ)↓ and m(M, w, σ ] ) are Y -DD and hence that the sets r(M, w, σ)↓(i..j) and m(M, w, σ ] )(i..j) are defined for each (i, j) ∈ Z2 . To prove the statement of this theorem, we first argue by induction on n ∈ N that for each standard LTDEL event-run σ satisfying |σ| ≤ n and |σ| = |r(M, w, σ)| − 1, we have the following items. |σ|

1. Let σ = {(Ui , si )}i=1 and let k range over N. |σ|−k

|σ|−k−1

(a) r(M, w, σk ), π1 (x) |=LTDEL pUk+1 π2 (π1 and each k < |σ|.


(x)) for each x ∈ r(M, w, σ)↓(|σ|)

(b) r(M, w, σk )[Uk+1 ] = r(M, w, σk+1 ) for each k < |σ|. |σ|−k

|σ|−k−1

(c) m(M, w, σk] ), π1 (y) |=LDETL pUk+1 ]k π2 (π1 and each k < |σ|.


(y)) for each y ∈ m(M, w, σ ] )(|σ|)

] (d) m(M, w, σk] )[Uk+1 ]k] = m(M, w, σk+1 ) for each k < |σ|.

28

def

2. Let τ = σ|σ|−1 . Define the function fσ by ( (fτ (v), [) if v ∈ r(M, w, σ)↓(..|σ| − 1), def fσ (v) = v if v ∈ r(M, w, σ)↓(|σ|). fσ is an isomorphism between ˙ (r(M, w, σ)↓, r˙ (M, w, σ)) and (m(M, w, σ ] ), m(M, w, σ ] )) |σ|

with π1d (v) = π1 (fσ (v)) ∈ W M for d ∈ N and v ∈ r(M, w, σ)↓(d). 3. For each ϕ ∈ LTDEL , d ∈ N, and x ∈ r(M, w, σ)↓(d), we have r(M, w, σ), x |=LTDEL ϕ iff m(M, w, σ ] ), fσ (x) |=LDETL ϕ]d . In the base case of this induction, σ = ∅. Item 1 is immediate and item 2 follows because r(M, w, ∅)↓ = M = m(M, w, ∅] ) and f∅ : W M → W M is the identity. Choosing x ∈ W M , we prove Item 3 as follows. • r(M, w, ∅), x |=LTDEL ϕ iff M, x |=LDETL ϕ• .

By the LTDEL Reduction Theorem (Theorem 6.8), the fact that r(M, w, ∅)↓ = M and that ϕ• ∈ LSETL , and the Collapse Lemma (Lemma 6.7).

• M, x |=LDETL ϕ• iff M, x |=LDETL (ϕ]0 )◦ .

By the Connection Lemma (Lemma 6.12).

• M, x |=LDETL (ϕ]0 )◦ iff m(M, w, ∅] ), x |=LDETL ϕ]0

By the LDETL Reduction Theorem (Theorem 2.8), the Correctness Theorem (Theorem 3.2), LDETL -truth (Definition 3.1), and the equality m(M, w, ∅] ) = M .

For the induction step, we assume the following induction hypothesis: 1, 2, and 3 hold for every standard LTDEL event-run σ satisfying |σ| ≤ n and |σ| = |r(M, w, σ)| − 1. We wish to prove that 1, 2, and 3 hold for an arbitrarily chosen standard LTDEL event-run σ satisfying |σ| = n + 1 and |σ| = |r(M, w, σ)| − 1. The proof that item 1 holds for σ follows by the definition of r(M, w, σ), items 2 and 3 of the induction hypothesis for τ = σn , and the definition of ]n. |σ| We now prove that 2 holds for σ. First, it follows that π1d (v) = π1 (fσ (v)) ∈ W M for d ∈ N and v ∈ r(M, w, σ)↓(d) by considering the cases v ∈ r(M, w, σ)↓(..|τ |) and v ∈ r(M, w, σ)↓(|σ|). In the first case, we use the induction hypothesis for item 2 to show that |τ | π1d (v) = π1 (fτ (v)) ∈ W M . In the second case, v = (v 0 , s) with v 0 ∈ r(M, w, σ)↓(..|τ |), so we apply the argument in the first case to v 0 . Next, to prove that fσ is the desired isomorphism between pointed Kripke models, we must show a number of properties about fσ . The most ] difficult of these are the proofs that fσ is onto the set W m(M,w,σ ) , which comes up in showing ˙ that fσ is a bijection mapping r˙ (M, w, σ) to m(M, w, σ ] ), and that fσ preserves the epistemic and temporal relations. (Note that the proof that fσ preserves the propositional valuation |σ| follows easily because π1d (v) = π1 (fσ (v)) ∈ W M for d ∈ N and v ∈ r(M, w, σ)↓(d).) In the interest of space, we shall sketch the proofs just for these difficult arguments. 29

]

• fσ is onto the set W m(M,w,σ ) .

]

We prove that v ∈ W r(M,w,σ)↓ implies fσ (v) ∈ W m(M,w,σ ) , considering the cases v ∈ r(M, w, σ)↓(..|τ |) and v ∈ r(M, w, σ)↓(|σ|). The first case uses item 2 of the induction ] hypothesis to show that fτ (v) ∈ W m(M,w,τ ) ; since pU|σ| ](|σ|−1) ([) = >, it follows by item ] 1d that fσ (v) = (fτ (v), [) ∈ W m(M,w,σ ) . The second case uses item 2 of the induction ] hypothesis to show that fτ (π1 (v)) ∈ W m(M,w,τ ) ; since m(M, w, τ ] ), fτ (π1 (v)) |=LDETL pU|σ| ](|σ|−1) (π2 (v)) by item 1c of the induction hypothesis, it follows by item 1d that ] fσ (v) = v ∈ W m(M,w,σ ) . ]

We now prove that for each u ∈ W m(M,w,σ ) , there is a u0 ∈ W r(M,w,σ)↓ such that fσ (u0 ) = u. As in the previous paragraph, we consider two cases: u ∈ r(M, w, σ)↓(..|τ |) and u ∈ r(M, w, σ)↓(|σ|). In the first case, we use item 2 of the induction hypothesis to conclude def that fτ is a bijection; we may then define u0 = fτ−1 (π1 (u)), and
it follows that fσ (u0 ) = (fτ (u0 ), [) = u. In the second case, fσ (u) = fτ (π1 (u)), π2 (u) = (π1 (u), π2 (u)) = u, with the second equality following by item 2 of the induction hypothesis and the fact that π1 (u) ∈ r(M, w, σ)↓(|τ |). r(M,w,σ)↓

• u ∈ Ra

m(M,w,σ ] )

(v) iff fσ (u) ∈ Ra

(fσ (v)) for each a ∈ A.

It is not difficult to see that r(M, w, τ )↓ is synchronous. To prove the statement above, we consider two cases. Case one: v ∈ r(M, w, σ)↓(..|τ |). We have the following. r(M,w,σ)↓

r(M,w,τ )↓

– u ∈ Ra (v) iff u ∈ Ra (v). Since v ∈ r(M, w, σ)↓(..|τ |) and r(M, w, τ )↓ is synchronous. r(M,w,τ )↓

m(M,w,τ ] )

– u ∈ Ra (v) iff fτ (u) ∈ Ra (fτ (v)). By item 2 of the induction hypothesis. m(M,w,τ ] )

m(M,w,σ ] )

– fτ (u) ∈ Ra (fτ (v)) iff fσ (u) ∈ Ra (fσ (v)). Since the assumption v ∈ r(M, w, σ)↓(..|τ |) and the synchronicity of r(M, w, τ )↓ together imply the equality fσ (x) = (fτ (x), [) for x ∈ {u, v}, the result follows by the equality pU|σ| ](|σ|−1) ([) = > and item 1d. Case two: v ∈ r(M, w, σ)↓(|σ|). We have the following. r(M,w,σ)↓

– u ∈ Ra (v) iff U r(M,w,τ )↓ π1 (u) ∈ Ra (π1 (v)) and π2 (u) ∈ Ra |σ| (π2 (v)). By item 1b, LTDEL -truth, and the fact v ∈ r(M, w, σ)↓(|σ|). r(M,w,τ )↓

U

m(M,w,τ ] )

U

– π1 (u) ∈ Ra (π1 (v)) and π2 (u) ∈ Ra |σ| (π2 (v)) iff U ](|σ|) m(M,w,τ ] ) π1 (u) ∈ Ra (π1 (v)) and π2 (u) ∈ Ra |σ| (π2 (v)). By the definition of U|σ| ](|σ|), item 2 of the induction hypothesis, and the fact that v ∈ r(M, w, σ)↓(|σ|) and the synchronicity of r(M, w, τ )↓ together imply that fτ (π1 (x)) = π1 (x) for x ∈ {u, v}. – π1 (u) ∈ Ra (π1 (v)) and π2 (u) ∈ Ra |σ| ] m(M,w,σ ) u ∈ Ra (v). By LDETL -truth and item 1d. 30

](|σ|)

(π2 (v)) iff

r(M,w,σ)↓

• u ∈ RY

m(M,w,σ ] )

(v) iff fσ (u) ∈ RY

(fσ (v)).

We consider two cases.

Case one: v ∈ r(M, w, σ)↓(..|τ |). The proof of this case is similar to the proof of the analogous case of the previous item (note that synchronicity is not needed here). r(M,w,σ)↓

Case two: v ∈ r(M, w, σ)↓(|σ|). We first show u ∈ RY (v) implies fσ (u) ∈ m(M,w,σ ] ) r(M,w,σ)↓ RY (fσ (v)). Assume u ∈ RY (v) and hence that u ∈ r(M, w, σ)↓(|τ |). Then π2 (fσ (u)) = [ and hence m(M,w,σ ] )

fσ (u) = (u, [) ∈ RY U

because [ ∈ RY |σ| (u, π2 (v)).

](|σ|−1)

(u, π2 (v))

(π2 (fσ (v))). The result follows from the fact that fσ (v) = v = m(M,w,σ ] )

(fσ (v)). Then π2 (fσ (v)) 6= [, To prove the converse, we assume fσ (u) ∈ RY U|σ| ](|σ|−1) U|σ| ](|σ|−1) and hence as {[} = RY (π2 (fσ (v))) and ∅ = RY (π2 (fσ (v))), we have the middle equality of fτ (u) = π1 (fσ (u)) = π1 (fσ (v)) = π1 (v) . Since m(M, w, τ ] ), π1 (v) |=LDETL pU|σ| ](|σ|−1) (π2 (fσ (v))) implies that π1 (v) ∈ m(M, w, τ ] )(|τ |), and since item 3 of the inductive hypothesis guarantees that fτ preserves the depth of a world, we have that u ∈ r(M, w, τ )↓(|τ |), and hence fτ (u) = u, whence π1 (v) = u. r(M,w,σ)↓ By the definition of r(M, w, σ)↓, we conclude that u ∈ RY (v). This completes the proof of item 2 for σ. To prove item 3 for σ, we choose d ∈ N and x ∈ r(M, w, σ)↓(d). If d < |σ|, then we have the following. • r(M, w, σ), x |=LTDEL ϕ iff r(M, w, τ ), x |=LTDEL ϕ. Since d < |σ|.

• r(M, w, τ ), x |=LTDEL ϕ iff m(M, w, τ ] ), fτ (x) |=LDETL ϕ]d . By item 3 of the induction hypothesis.

• m(M, w, τ ] ), fτ (x) |=LDETL ϕ]d iff m(M, w, σ ] ), fσ (x) |=LDETL ϕ]d .

By the Past State Theorem (Theorem 5.5), the equality fσ (x) = (fτ (x), [), and item 1d.

If d = |σ|, then we have the following.

• r(M, w, σ), x |=LTDEL ϕ iff r(M, w, τ ), π1 (x) |=LTDEL [U|σ| , s|σ| ]ϕ.

By the equality σ = τ · (U|σ| , s|σ| ), item 1b for σ, and LTDEL -truth.

• r(M, w, τ ), π1 (x) |=LTDEL [U|σ| , s|σ| ]ϕ iff m(M, w, τ ] ), fτ (π1 (x)) |=LDETL ([U|σ| , s|σ| ]ϕ)](|τ |) . By item 3 of the induction hypothesis.

31

• m(M, w, τ ] ), fτ (π1 (x)) |=LDETL ([U|σ| , s|σ| ]ϕ)](|τ |) iff m(M, w, σ ] ), fσ (x) |=LDETL ϕ](|σ|) .

By the definition of ](|σ|) (Figure 5), LDETL -truth, item 1d for σ, and the equality σ = τ · (U|σ| , s|σ| ).

This completes the inductive argument. To prove the statement of the theorem, first define def m = |r(M, w, σ)| − 1. Apply items 1, 2, and 3 to σm . Then observe that r(M, w, σm ) = ] ) = m(M, w, σ ] ) r(M, w, σ) by the definition of r(M, w, σ) and that this implies that m(M, w, σm by items 1 and 3. The statement of the theorem follows.

References [1] Alexandru Baltag and Lawrence S. Moss. Logics for epistemic programs. Synthese, 139(2):165–224, 2004. [2] Alexandru Baltag, Lawrence S. Moss, and Slawomir Solecki. The logic of public announcements, common knowledge, and private suspicions. In Itzhak Gilboa, editor, Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge (TARK VII), pages 43–56, Evanston, Illinois, USA, 1998. [3] Alexandru Baltag, Hans P. van Ditmarsch, and Lawrence S. Moss. Epistemic logic and information update. In Pieter Adriaans and Johan van Benthem, editors, Handbook on the Philosophy of Information, pages 369–463. Elsevier, 2008. [4] Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic. Cambridge University Press, 2001. [5] Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning about Knowledge. The MIT Press, 1995. [6] Tomohiro Hoshi and Audrey Yap. Dynamic epistemic logic with branching temporal structures. Synthese, 169(2):259–281, 2009. [7] Carsten Lutz. Complexity and succinctness of public announcement logic. In Proceedings of the 5th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS-06), pages 137–144, Hakodate, Japan, May 8–12, 2006. Association for Computing Machinery (ACM), New York, New York, USA. [8] Rohit Parikh and Ramaswamy Ramanujam. A knowledge based semantics of messages. Journal of Logic, Language, and Information, 12:453–467, 2003. [9] Bryan Renne, Joshua Sack, and Audrey Yap. Dynamic epistemic temporal logic. In X. He, J. Horty, and E. Pacuit, editors, Logic, Rationality, and Interaction, Second International Workshop, LORI 2009, Chongqing, China, October 8–11, 2009, Proceedings, volume 5834/2009 of Lecture Notes in Computer Science, pages 263–277. Springer Berlin/Heidelberg, 2009.

32

[10] Joshua Sack. Temporal languages for epistemic programs. Journal of Logic, Language, and Information, 17(2):183–216, 2008. [11] Johan van Benthem, Jelle Gerbrandy, Tomohiro Hoshi, and Eric Pacuit. Merging frameworks for interaction. Journal of Philosophical Logic, 38(5):491–526, 2009. [12] Johan van Benthem, Jelle Gerbrandy, and Eric Pacuit. Merging frameworks for interaction: DEL and ETL. In Proceedings of the 11th Conference on Theoretical Aspects of Rationality and Knowledge (TARK XI), pages 72–81, 2007. [13] Johan van Benthem, Jan van Eijck, and Barteld Kooi. Logics of communication and change. Information and Computation, 204(11):1620–1662, 2006. [14] Hans van Ditmarsch, Wiebe van der Hoek, and Barteld Kooi. Dynamic Epistemic Logic. Synthese Library. Springer, 2007. [15] Audrey Yap. Dynamic epistemic logic and temporal modality. Forthcoming in Proceedings of Dynamic Logic Montr´eal, 2007.

33