Convergence, Continuity and Recurrence in Dynamic Epistemic Logic Dominik Klein1 and Rasmus K. Rendsvig2 1 Department of Philosophy, Bayreuth University, and Department of Political Science, University of Bamberg dominik.klein@uni-bayreuth.de 2 Theoretical Philosophy, Lund University, and Center for Information and Bubble Studies, University of Copenhagen rendsvig@gmail.com Abstract. The paper analyzes dynamic epistemic logic from a topological perspective. The main contribution consists of a framework in which dynamic epistemic logic satisfies the requirements for being a topological dynamical system thus interfacing discrete dynamic logics with continuous mappings of dynamical systems. The setting is based on a notion of logical convergence, demonstratively equivalent with convergence in Stone topology. Presented is a flexible, parametrized family of metrics inducing the latter, used as an analytical aid. We show maps induced by action model transformations continuous with respect to the Stone topology and present results on the recurrent behavior of said maps. Keywords: dynamic epistemic logic, limit behavior, convergence, recurrence, dynamical systems, metric spaces, general topology, modal logic 1 Introduction Dynamic epistemic logic is a framework for modeling information dynamics. In it, systematic change of Kripke models are punctiliously investigated through model transformers mapping Kripke models to Kripke models. The iterated application of such a map may constitute a model of information dynamics, or be may be analyzed purely for its mathematical properties [6, 8, 10,11,13,16,18,40–43]. Dynamical systems theory is a mathematical field studying the long-term behavior of spaces under the action of a continuous function. In case of discrete time, this amounts to investigating the space under the iterations of a continuous map. The field is rich in concepts, methodologies and results developed with the aim of understanding general dynamics. The two fields find common ground in the iterated application of maps. With dynamic epistemic logic analyzing very specific map types, the hope is that general results from dynamical systems theory may shed light on properties of the former. There is, however, a chasm between the two: Dynamical systems theory revolves around spaces imbued with metrical or topological structure with respect to which maps are continuous. No such structure is found in dynamic epistemic logic. This chasm has not gone unappreciated: In his 2011 Logical Dynamics of Information and Interaction [10], van Benthem writes Copy-Pastable BibTeX: @inproceedings{KleinRendsvigLORI2017, author = {Klein, Dominik and Rendsvig, Rasmus K.}, title = {{Convergence, Continuity and Recurrence in Dynamic Epistemic Logic}}, editor = {Baltag, Alexandru and Seligman, Jeremy and Yamada, Tomoyuki}, booktitle = {Logic, Rationality, and Interaction (LORI 2017, Sapporo, Japan)}, series = {LNCS}, year = {2017}, publisher = {Springer} } ar X iv :1 70 9. 00 35 9v 1 [ cs .L O ] 1 S ep 2 01 7 From discrete dynamic logics to continuous dynamical systems "We conclude with what we see as a major challenge. Van Benthem [7, 8] pointed out how update evolution suggests a long-term perspective that is like the evolutionary dynamics found in dynamical systems. [...] Interfacing current dynamic and temporal logics with the continuous realm is a major issue, also for logic in general." [10, Sec. 4.8. Emph. is org. heading] This paper takes on the challenge and attempts to bridge this chasm. We proceed as follows. Section 2 presents what we consider natural spaces when working with modal logic, namely sets of pointed Kripke models modulo logical equivalence. These are referred to as modal spaces. A natural notion of "logical convergence" on modal spaces is provided. Section 3 seeks a topology on modal spaces for which topological convergence coincides with logical convergence. We consider a metric topology based on n-bisimulation and prove it insufficient, but show an adapted Stone topology satisfactory. Saddened by the loss of a useful aid, the metric inducing the n-bisimulation topology, a family of metrics is introduced that all induce the Stone topology, yet allow a variety of subtle modelling choices. Sets of pointed Kripke models are thus equipped with a structure of compact metric spaces. Section 4 considers maps on modal spaces based on multi-pointed action models using product update. Restrictions are imposed to ensure totality, and the resulting clean maps are shown continuous with respect to the Stone topology. With that, we present our main contribution: A modal space under the action of a clean map satisfies the standard requirements for being a topological dynamical system. Section 5 applies the now-suited terminology from dynamical systems theory, and present some initial results pertaining to the recurrent behavior of clean maps on modal spaces. Section 6 concludes the paper by pointing out a variety of future research venues. Throughout, we situate our work in the literature. Remark 1. To make explicit what may be apparent, note that the primary concern is the semantics of dynamic epistemic logic, i.e., its models and model transformation. Syntactical considerations are briefly touched upon in Section 6. Remark 2. The paper is not self-contained. For notions from modal logic that remain undefined here, refer to e.g. [14, 27]. For topological notions, refer to e.g. [37]. For more on dynamic and epistemic logic than the bare minimum of standard notions and notations rehearsed, see e.g. [2–5, 10, 20, 22, 30, 38, 39]. Finally, a background document containing generalizations and omitted proofs is our [31]. 2 Modal Spaces and Logical Convergence Let there be given a countable set Φ of atoms and a finite set I of agents. Where p ∈ Φ and i ∈ I, define the language L by φ := > | p | ¬φ | φ ∧ φ | iφ. Modal logics may be formulated in L. By a logic Λ we refer only to extensions of the minimal normal modal logic K over the language L. With Λ given by context, let φ be the set of formulas Λ-provably equivalent to φ. Denote the resulting partition {φ : φ ∈ L} of L by LΛ.3 Call LΛ's elements Λ-propositions. We use relational semantics to evaluate formulas. A Kripke model for L is a tuple M = (JMK , R, J*K) where JMK is a countable, non-empty set of states, R : I −→ P(JMK × JMK) assigns to each i ∈ I an accessibility relation Ri, and J*K : Φ −→ P(JMK) is a valuation, assigning to each atom a set of states. With s ∈ JMK, call Ms = (JMK , R, J*K , s) a pointed Kripke model. The used semantics are standard, including the modal clause: Ms  iφ iff for all t : sRit implies Mt  φ. Throughout, we work with pointed Kripke models. Working with modal logics, we find it natural to identify pointed Kripke models that are considered equivalent by the logic used. The domains of interest are thus the following type of quotient spaces: Definition 1. The LΛ modal space of a set of pointed Kripke models X is the set X = {x : x ∈ X} for x = {y ∈ X : y  φ iff x  φ for all φ ∈ LΛ}. Working with an LΛ modal space portrays that we only are interested in differences between pointed Kripke models insofar as these are modally expressible and are considered differences by Λ. In a modal space, how may we conceptualize that a sequence x1,x2, ... converges to some point x? Focusing on the concept from which we derive the notion of identity in modal spaces, namely Λ-propositions, we find it natural to think of x1,x2, ... as converging to x just in case xn moves towards satisfying all the same Λ-propositions as x as n goes to infinity. We thus offer the following definition: Definition 2. A sequence of points x1,x2, ... in an LΛ modal space X is said to logically converge to the point x in X iff for every φ ∈ LΛ for which x  φ, there is an N ∈ N such that xn  φ for all n ≥ N . To avoid re-proving useful results concerning this notion of convergence, we next turn to seeking a topology for which logical convergence coincides with topological convergence. Recall that for a topology T on a set X, a sequence of points x1, x2, ... is said to converge to x in the topological space (X, T ) iff for every open set U ∈ T containing x, there is an N ∈ N such that xn ∈ U for all n ≥ N . 3 Topologies on Modal Spaces One way of obtaining a topology on a space is to define a metric for said space. Several metrics have been suggested for sets of pointed Kripke models 3 LΛ is isomorphic to the domain of the Lindenbaum algebra of Λ. [1, 17]. These metrics are only defined for finite pointed Kripke models, but incorporating ideas from the metrics of [36] on shift spaces and [26] on sets of first-order logical theories allows us to simultaneously generalize and simplify the n-Bisimulation-based Distance of [17] to the degree of applicability: Let X be a modal space for which modal equivalence and bisimilarity coincide4 and let -n relate x, y ∈ X iff x and y are n-bisimilar. Then proving dB(x,y) = { 0 if x -n y for all n 1 2n if n is the least intenger such that x 6-n y a metric on X is trivial. We refer to dB as the n-bisimulation metric, and to the inducedmetric topology as the n-bisimulation topology, denoted TB . A basis of the topology TB is given by the set of elements Bxn = {y ∈X : y -n x}. Considering the intimate link between modal logic and bisimulation, we consider both n-bisimulation metric and topology highly natural.5 Alas, logical convergence does not: Proposition 1. Logical convergence in arbitrary modal space X does not imply convergence in the topological space (X, TB). Proof. LetX be anLΛ modal space with L based on the atoms Φ = {pk : k ∈ N}. Let x ∈ X satisfy ⊥ and pk for all k ∈ N. Let x1,x2, ... be a sequence in X such that for all k ∈ N, xk satisfies ⊥, pm for all m ≤ k, and ¬pl for all l > k. Then for all φ ∈ LΛ for which x  φ, there is an N such that xn  φ for all n ≥ N , hence the sequence x1,x2, ... converges to x.There does not, however, exist any N ′ such that xn′ ∈ Bx0 for all n′ ≥ N ′. Hence x1,x2, ... does not converge to x in TB . ut Proposition 1 implies that the n-bisimulation topology may not straight-forwardly be used to establish negative results concerning logical convergence. That it may be used for positive cases is a corollary to Propositions 2 and 6 below. On the upside, logical convergence coincides with convergence in the n-bisimulation topology – i.e. Proposition 1 fails – when L has finite atoms. This is a corollary to Proposition 5. An alternative to a metric-based approach to topologies is to construct the set of all open sets directly. Comparing the definition of logical convergence with that of convergence in topological spaces is highly suggestive: Replacing every occurrence of the formula φ with an open set U while replacing satisfaction  with inclusion ∈ transforms the former definition into the latter. Hence the collection of sets Uφ = {x ∈X : x  φ}, φ ∈ LΛ, seems a reasonable candidate for a topology. Alas, this collection is not closed under arbitrary unions, as all formulas are finite. Hence it is not a topology. It does however constitute the basis for a topology, in fact the somewhat influential Stone topology, TS . 4 That all models in X are image-finite is a sufficient condition, cf. the HennessyMilner Theorem. See e.g. [14] or [27]. 5 Space does not allow for a discussion of the remaining metrics of [1,17], but see [31]. The Stone topology is traditionally defined on the collection of complete theories for some propositional, first-order or modal logic, but is straightforwardly applicable to modal spaces. Moreover, it satisfies our desideratum: Proposition 2. For any LΛ modal space X, a sequence x1,x2, ... logically converges to the point x if, and only if, it converges to x in (X, TS). Proof. Assume x1,x2, ... logically converges to x in X and that U containing x is open in TS . Then there is a basis element Uφ ⊆ U with x ∈ Uφ. So x  φ. By assumption, there exists an N such that xn  φ for all n ≥ N . Hence xn ∈ Uφ ⊆ U for all n ≥ N . Assume x1,x2, ... converges to x in (X, TS) and let x  φ. Then x ∈ Uφ, which is open. As the sequence converges, there exists an N such that xn ∈ Uφ for all n ≥ N . Hence xn  φ for all n ≥ N . ut Apart from its attractive characteristic concerning convergence, working on the basis of a logic, the Stone topology imposes a natural structure. As is evident from its basis, every subset of X characterizable by a single Λ-proposition φ ∈ LΛ is clopen. If the logic Λ is compact and X saturated (see fn. 7), also the converse is true: every clopen set is of the form Uφ for some φ. We refer to [31] for proofs and a precise characterization result. In this case, a subset is open, but not closed, iff it is characterizable only by an infinitary disjunction of Λ-propositions, and a subset if closed, but not open, iff it is characterizable only by an infinitary conjunction of Λ-propositions. The Stone topology thus transparently reflects the properties of logic, language and topology. Moreover, it enjoys practical topological properties: Proposition 3. For any LΛ modal space X, (X, TS) is Hausdorff and totally disconnected. If Λ is (logically) compact6 and X is saturated7, then (X, TS) is also (topologically) compact. Proof. These properties are well-known for the Stone topology applied to complete theories. For the topology applied to modal spaces, we defer to [31]. ut One may interject that, as having a metric may facilitate obtaining results, it may cause a loss of tools to move away from the n-bisimulation topology. The Stone topology, however, is metrizable. A family of metrics inducing it, generalizing the Hamming distance to infinite strings by using weighted sums, was introduced in [31]. We here present a sub-family, suited for modal spaces: Definition 3. Let D ⊆ LΛ contain for every ψ ∈ LΛ some {φi}i∈I that Λentails either ψ or ¬ψ, and let φ1,φ2, ... be an enumeration of D. Let X be an LΛ modal space. For all x,y ∈X, for all k ∈ N, let 6 A logic Λ is logically compact if any arbitrary set A of formulas is Λ-consistent iff every finite subset of A is Λ-consistent. 7 An LΛ modal space X is saturated iff for each Λ-consistent set of formulas A, there is an x ∈ X such that x  A. Saturation relates to the notion of strong completeness, cf. e.g. [14, Prop.4.12]. See [31] for its use in a more general context. dk(x,y) = { 0 if x  φ iff y  φ for φ ∈ φk 1 else Let w : D −→ R>0 assign strictly positive weight to each φk in D such that (w(φn)) forms a convergent series. Define the function dw :X 2 −→ R by dw(x,y) = ∞∑ k=0 w(φk)dk(x,y) for all x,y ∈ X. The set of these functions is denoted DX . Let DD,X = ∪D⊆LΛDX . We refer to [31] for the proof establishing the following proposition: Proposition 4. Let X be an LΛ modal space and dw belong to DX . Then dw is a metric on X and the metric topology Tw induced by dw on X is the Stone topology of Λ. For a metric space (X, d), we will also write Xd. With variable parameters D and w, DX allows one to vary the choice of metric with the problem under consideration. E.g., if the n-bisimulation metric seems apt, one could choose that, with one restriction: Proposition 5. If X is an LΛ modal space with L based on a finite atom set, then DX contains a topological equivalent to the n-bisimulation metric. Proof (sketch). As L is based on a finite set of atoms, for each x ∈ X, n ∈ N0, there exists a characteristic formula φx,n such that y  φx,n iff y -n x, cf. [27]. Let Dn = {φx,n : x ∈ X} and D = ∪n∈N0Dn. Then each Dn is finite and D satisfies Definition 3. Finally, let w(φ) = 1|Dn| * 1 2n+1 for φ ∈ Dn. Then dw ∈ DX and is equivalent to the n-bisimulation metric db. ut As a corollary to Proposition 5, it follows that, for finite atom languages, the n-bisimulation topology is the Stone topology. This is not true in general, as witnessed by Proposition 1 and the following: Proposition 6. If X is an LΛ modal space with L based on a countably infinite atom set, then the n-bisimulation metric topology on X is strictly finer than the Stone topology on X. Proof (sketch). We refer to [31] for details, but for TB 6⊆ TS , note that the set Bx0 used in the proof of Prop. 1, is open in TB , but not in TS . ut With this comparison, we end our exposition of topologies on modal spaces. 4 Clean Maps on Modal Spaces We focus on a class of maps induced by action models applied using product update. Action models are a popular and widely applicable class of model transformers, generalizing important constructions such as public announcements. An especially general version of action models is multi-pointed action models with postconditions. Postconditions allow action states in an action model to change the valuation of atoms [12,19], thereby also allowing the representation of information dynamics concerning situations that are not factually static. Permitting multiple points allows the actual action states executed to depend on the pointed Kripke model to be transformed, thus generalizing single-pointed action models.8 Amulti-pointed action model is a tuple ΣΓ = (JΣK,R, pre, post, Γ ) where JΣK is a countable, non-empty set of actions. The map R : I → P(JΣK × JΣK) assigns an accessibility relation Ri on JΣK to each agent i ∈ I. The map pre : JΣK→ L assigns to each action a precondition, and the map post : JΣK→ L assigns to each action a postcondition,9 which must be > or a conjunctive clause10 over Φ. Finally, ∅ 6= Γ ⊆ JΣK is the set of designated actions. To obtain well-behaved total maps on a modal spaces, we must invoke a set of mild, but non-standard, requirements: Let X be a set of pointed Kripke models. Call ΣΓ precondition finite if the set {pre(σ) ∈ LΛ : σ ∈ JΣK} is finite. This is needed for our proof of continuity. Call ΣΓ exhaustive over X if for all x ∈ X, there is a σ ∈ Γ such that x  pre(σ). This conditions ensures that the action model ΣΓ is universally applicable on X. Finally, call ΣΓ deterministic over X if X  pre(σ) ∧ pre(σ′) → ⊥ for each σ 6= σ′ ∈ Γ . Together with exhaustivity, this condition ensures that the product of ΣΓ and any Ms ∈ X is a (single-)pointed Kripke model, i.e., that the actual state after the updates is well-defined and unique. Let ΣΓ be exhaustive and deterministic over X and let Ms ∈ X. Then the product update of Ms with ΣΓ , denoted Ms ⊗ ΣΓ , is the pointed Kripke model (JMΣK , R′, J*K′, s′) with JMΣK = {(s, σ) ∈ JMK× JΣK : (M, s)  pre(σ)} R′ = {((s, σ), (t, τ)) : (s, t) ∈ Ri and (σ, τ) ∈ Ri} , for all i ∈ N JpK′ = {(s, σ) :s ∈ JpK, post(σ) 2 ¬p} ∪ {(s, σ) :post(σ)  p} , for all p ∈ Φ s′ = (s, σ) : σ ∈ Γ and Ms  pre(σ) Call ΣΓ closing over X if for all x ∈ X, x⊗ΣΓ ∈ X. With ΣΓ exhaustive and deterministic, ΣΓ and ⊗ induce a well-defined total map on X. The class of maps of interest in the present is then the following: Definition 4. Let X be an LΛ modal space. A map f :X →X is called clean if there exists a precondition finite, multi-pointed action model ΣΓ closing, deterministic and exhaustive over X such that f(x) = y iff x ⊗ ΣΓ ∈ y for all x ∈X. 8 Multi-pointed action models are also referred to as epistemic programs in [2], and allow encodings akin to knowledge-based programs [22] of interpreted systems, cf. [42]. 9 The precondition of σ specify the conditions under which σ is executable, while its postcondition may dictate the posterior values of a finite, possibly empty, set of atoms. 10 I.e. a conjuction of literals, where a literal is an atom or a negated atom. Clean maps are total by the assumptions of being closing and exhaustive. They are well-defined as f(x) is independent of the choice of representative for x: If x′ ∈ x, then x′ ⊗ ΣΓ and x ⊗ ΣΓ are modally equivalent and hence define the same point in X. The latter follows as multi-pointed action models applied using product update preserve bisimulation [2], which implies modal equivalence. Clean maps moreover play nicely with the Stone topology: Proposition 7. Let f be a clean map on an LΛ modal space X. Then f is continuous with respect to the Stone topology of Λ. Proof (sketch). We defer to [31] for details, but offer a sketch: The map f is shown uniformly continuous using the ε-δ formulation of continuity. The proof relies on a lemma stating that for every dw ∈ DX and every ε > 0, there are formulas χ1, . . . , χl ∈ L such that every x ∈ X satisfies some χi and whenever y  χi and z  χi for some i ≤ l, then dw(y, z) < ε. The main part of the proof establishes the claim that there is a function δ : L → (0,∞) such that for any φ ∈ L, if f(x)  φ and da(x, y) < δ(φ), then f(y)  φ. Setting δ = min{δ(χi) : i ≤ l} then yields a δ with the desired property. ut With Proposition 7, we are positioned to state our main theorem: Theorem 1. Let f be a clean map on a saturated LΛ modal space X with Λ compact and let d ∈ DX . Then (Xd,f) is a topological dynamical system. Proof. Propositions 2, 3, 4 and 7 jointly imply thatXd is a compact metric space on which f is continuous, thus satisfying the requirements of e.g. [21,29,44]. ut With Theorem 1, we have, in what we consider a natural manner, situated dynamic epistemic logic in the mathematical discipline of dynamical systems. A core topic in this discipline is to understand the long-term, qualitative behavior of maps on spaces. Central to this endeavor is the concept of recurrence, i.e., understanding when a system returns to previous states as time goes to infinity. 5 Recurrence in the Limit Behavior of Clean Maps We represent results concerning the limit behavior of clean maps on modal spaces. In establishing the required terminology, we follow [29]: Let f be a continuous map on a metric space Xd and x ∈ Xd. A point y ∈ X is a limit point11 for x under f if there is a strictly increasing sequence n1, n2, ... such that the subsequence fn1(x), fn2(x), ... of (fn(x))n∈N0 converges to y. The limit set of x under f is the set of all limit points for x, denoted ωf (x). Notably, ωf (x) is closed under f : For y ∈ ωf (x) also f(y) ∈ ωf (x). We immediately obtain that any modal system satisfying Theorem 1 has a nonempty limit set: Proposition 8. Let (Xd,f) be as in Theorem 1. For any point x ∈ X, the limit set of x under f is non-empty. 11 Or ω-limit point. The ω is everywhere omitted as time here only moves forward. Proof. SinceX is is compact, every sequence inX has a convergent subsequence, cf. e.g. [37, Thm. 28.2]. Proposition 8 does not inform us of the structure of said limit set. In the study of dynamical systems, such structure is often sought through classifying the possible repetitive behavior of a system, i.e., through the system's recurrence properties. For such studies, a point x is called (positively) recurrent if x ∈ ωf (x), i.e., if it is a limit point of itself. The simplest structural form of recurrence is periodicity : For a point x ∈ X, call the set Of (x) = {fn(x) : n ∈ N0} its orbit. The orbit Of (x) is periodic if fn+k(x) = fn(x) for some n ≥ 0, k > 0; the least such k is the period of Of (x). Periodicity is thus equivalent to Of (x) being finite. Related is the notion of a limit cycle: a periodic orbit Of (x) is a limit cycle if it is the limit set of some y not in the period, i.e., if Of (x) = ωf (y) for some y 6∈ Of (x). It was conjectured by van Benthem that certain clean maps-those based on finite action models and without postconditions-would, whenever applied to a finite x, have a periodic orbit Of (x). I.e., after finite iterations, the map would oscillate between a finite number of states. This was the content of van Benthem's "Finite Evolution Conjecture" [8]. The conjecture was refuted using a counterexample by Sadzik in his 2006 paper, [43].12 The example provided by Sadzik (his Example 33) uses an action model with only Boolean preconditions. Interestingly, the orbit of the corresponding clean map terminates in a limit cycle. This is a corollary to Proposition 9 below. Before we can state the proposition, we need to introduce some terminology. Call a multi-pointed action model ΣΓ finite if JΣK is finite, Boolean if pre(σ) is a Boolean formula for all σ ∈ JΣK, and static if post(σ) = > for all σ ∈ JΣK. We apply the same terms to a clean map f based on ΣΓ . In this terminology, Sadzik showed that for any finite, Boolean, and static clean map f : X →X, if the orbit Of (x) is periodic, then it has period 1.13 This insightful result immediates the following: Proposition 9. Let (Xd,f) be as in Theorem 1 with f finite, Boolean, and static. For all x ∈X, the orbit Of (x) is periodic with period 1. Proof. By Prop. 8, the limit set ωf (x) of x under f is non-empty. Sadzik's result shows that it contains a single point. Hence (fn(x))n∈N0 converges to this point. As the limit set ωf (x) is closed under f , its unique point is a fix-point. ut Proposition 9 may be seen as a partial vindication of van Benthem's conjecture: Forgoing the requirement of reaching the limit set in finite time and the possibility of modal preconditions, the conjecture holds, even if the initial state has an infinite set of worlds JxK. This simple recurrent behavior is, however, not the general case. More complex clean maps may exhibit nontrivial recurrence, i.e., produce non-periodic orbits with recurrent points: 12 We paraphrase van Benthem and Sadzik using the terminology introduced. 13 See [16] for an elegant and generalizing exposition. Proposition 10. There exist finite, static, but non-Boolean, clean maps that exhibit nontrivial recurrence. Proposition 11. There exist finite, Boolean, but non-static, clean maps that exhibit nontrivial recurrence. We show these propositions below, building a clean map which, from a selected initial state, has uncountably many limit points, despite the orbit being only countable. Moreover, said orbit also contains infinitely many recurrent points. In fact, every element of the orbit is recurrent. We rely on Lemma 1 in the proof. A proof of Lemma 1.1 may be found in [32], a proof of Lemma 1.2 in [15]. Lemma 1. Any Turing machine can be emulated using a set X of S5 pointed Kripke models for finite atoms and a finite multi-pointed action model ΣΓ deterministic over X. Moreover, ΣΓ may be chosen 1. static, but non-Boolean, or 2. Boolean, but non-static. Proof (of Propostitions 10 and 11). For both propositions, we use a Turing machine ad infinitum iterating the successor function on the natural numbers. Numbers are represented in mirrored base-2, i.e., with the leftmost digit the lowest. Such a machine may be build with alphabet {., 0, 1,t}, where the symbol . is used to mark the starting cell and t is the blank symbol. We omit the exact description of the machine here. Of importance is the content of the tape: Omitting blank (t) cells, natural numbers are represented as illustrated in Fig. 1. 0 : . 0 2 : . 0 1 4 : . 0 0 1 6 : . 0 1 1 8 : . 0 0 0 1 1 : . 1 3 : . 1 1 5 : . 1 0 1 7 : . 1 1 1 9 : . 1 0 0 1 Fig. 1. Mirrored base-2 Turing tape representation of 0, .., 9 ∈ N0, blank cells omitted. Notice that the mirrored notation causes perpetual change close to the start cell, .. Initiated with its read-write head on the cell with the start symbol . of a tape with content n, the machine will go through a number of configurations before returning the read-write head to the start cell with the tape now having content n+1. Auto-iterating, the machine will thus, over time, produce a tape that will have contained every natural number in order. This Turing machine may be emulated by a finite ΣΓ on a set X cf. Lemma 1. Omitting the details14, the idea is that the Turing tape, or a finite fragment, thereof may be encoded as a pointed Kripke model: Each cell of the tape corresponds to a state, with the cell's content encoded by additional structure,15 which is modally expressible. By structuring the cell states with two equivalence relations and atoms u and e true at cells with odd (even) index respectively, (cf. Fig. 2), also the position of a cell is expressible. The designated state corresponds to the start cell, marked .. 14 The details differ depending on whether ΣΓ must be static, but non-Boolean for Prop. 10, or Boolean, but non-static for Prop. 11. See resp. [32] and [15]. 15 For Prop. 11, tape cell content may be encoded using atomic propositions, changable through postconditions, cf. [15]; for Prop. 10, cell content is written by adding and removing additional states, cf. [32]. e, φ. c0 u, φ0 c1 e, φ1 c2 u, φ0 c3 e, φ1 c4 a b a b Fig. 2. A pointed Kripke model emulating the configuration of the Turing machine with cell content representing the number 10. The designated state is the underlined c0. Each state is labeled with a formula φ., φ0 or φ1 expressing its content. Relations a and b allow expressing distance of cells: That c0 satisfies ♦a(u ∧ ♦b(e ∧ φ1)) exactly expresses that cell c2 contains a 1. Omitted are reflexive loops for relations, and the additional structure marking cell content and read-write head position. Let (cn)n∈N0 be the sequence of configurations of the machine when initiated on a tape with content 0. Each cn may be represented by a pointed Kripke model, obtaining a sequence (xn)n∈N0 . By Lemma 1, there thus exists a ΣΓ such that for all n, xn ⊗ ΣΓ = xn+1. Hence, moving to the full modal space X for the language used, a clean map f : X →X based on ΣΓ will satisfy f(xn) = xn+1 for all n. The Turing machine's run is thus emulated by (fk(x0))k∈N0 . Let (c′n)n∈N0 be the subsequence of (cn)n∈N0 where the machine has finished the successor operation and returned its read write head to its starting position ., ready to embark on the next successor step. The tape of the first 9 of these c′n are depicted in Fig. 1. Let (x′n)n∈N0 be the corresponding subsequence of (fk(x0))k∈N0 . We show that (x′n)n∈N0 has uncountably many limit points: For each subset Z of N, let cZ be a tape with content 1 on cell i iff i ∈ Z and 0 else. On the Kripke model side, let the corresponding xZ ∈ X be a model structurally identical to those of (x′n)n∈N0 , but satisfying φ1 on all "cell states" distance i ∈ Z from the designated "." state, and φ0 on all other.16 The set {xZ : Z ⊆ N} is uncountable, and each xZ is a limit point of x: For each Z ⊆ N and n ∈ N, there are infinitely many k for which xk  φ iff xZ  φ for all φ of modal depth at most n. Hence, for every n, the set {xk : db(xk,xZ) < 2−n} is infinite, with db the equivalent of the n-bisimulation metric, cf. Prop. 5. Hence, for each of the uncountably many Z ⊆ N, xZ is a limit point of the sequence x. Finally, every x′k ∈ (x′n)n∈N0 is recurrent: That x′k ∈ ωf (x′k) follows from x′k being a limit point of (x′n)n∈N0 , which it is as x′k = x Z for some Z ⊆ N.17 As the set of recurrent points is thus infinite, it cannot be periodic. ut As a final result on the orbits of clean maps, we answer an open question: After having exemplified a period 2 system, Sadzik [43] notes that it is unknown whether finite, static, but non-Boolean, clean maps exhibiting longer periods exist. They do: Proposition 12. For any n ∈ N, there exists finite, static, but non-Boolean clean maps with periodic orbits of period n. This is also true for finite Boolean, but non-static, clean maps. 16 The exact form is straightforward from the constructions used in [32] and [15]. 17 A similar argument shows that all xZ with Z ⊆ N co-infinite are recurrent points. Hence ωf (x′k) for any x ′ k ∈ (x′n)n∈N0 contains uncountably many recurrent points. Proof. For the given n, find a Turing machine that, from some configuration, loops with period n. From here, Lemma 1 does the job. ut Finally, we note that brute force determination of a clean map's orbit properties is not in general a feasible option: Proposition 13. The problems of determining whether a Boolean and nonstatic, or a static and non-Boolean, clean map, a) has a periodic orbit or not, and b) contains a limit cycle or not, are both undecidable. Proof. The constructions from the proofs of Lemma 1 allows encoding the halting problem into either question. ut 6 Discussion and Future Venues We consider Theorem 1 our main contribution. With it, an interface between the discrete semantics of dynamic epistemic logic with dynamical systems have been provided; thus the former has been situated in the mathematical field of the latter. This paves the way for the application of results from dynamical systems theory and related fields to the information dynamics of dynamic epistemic logic. The term nontrivial recurrence is adopted from Hasselblatt and Katok, [29]. They remark that "[nontrivial recurrence] is the first indication of complicated asymptotic behavior." Propositions 11 and 10 indicate that the dynamics of action models and product update may not be an easy landscape to map. Hasselblatt and Katok continue: "In certain low-dimensional situations [...] it is possible to give a comprehensive description of the nontrivial recurrence that can appear." [29, p. 24]. That the Stone topology is zero-dimensional fuels the hope that general topology and dynamical systems theory yet has perspectives to offer on dynamic epistemic logic. One possible direction is seeking a finer parametrization of clean maps combined with results specific to zero-dimensional spaces, as found, e.g., in the field of symbolic dynamics [36]. But also other venues are possible: The introduction of [29] is counts an inspiration. The approach presented furthermore applies to model transformations beyond multi-pointed action models and product update. Given the equivalence shown in [33] between single-pointed action model product update and general arrow updates, we see no reason to suspect that "clean maps" based on the latter should not be continuous on modal spaces. A further conjecture is that the action-priority update of [5] on plausibility models18 yields "clean maps" continuous w.r.t. the suited Stone topology, and that this may be shown using a variant of our proof of the continuity of clean maps. A more difficult case is the PDLtransformations of General Dynamic Dynamic Logic [25] given the signature change the operation involves. 18 Hence also the multi-agent belief revision policies lexicographic upgrade and elite change, also known as radical and conservative upgrade, introduced in [9], cf. [5]. There is a possible clinch between the suggested approach and epistemic logic with common knowledge. The state space of a dynamical system is compact. The Stone topology for languages including a common knowledge operator is non-compact. Hence, it cannot constitute the space of a dynamical system-but its one-point compactification may. We are currently working on this clinch, the consequences of compactification, and relations to the problem of attaining common knowledge, cf. [28]. Questions also arise concerning the dynamic logic of dynamic epistemic logic. Propositions 10 and 11 indicate that there is more to the semantic dynamics of dynamic epistemic logic than is representable by finite compositional dynamic modalities-even when including a Kleene star. An open question still stands on how to reason about limit behavior. One interesting venue stems from van Benthem [10]. He notes19 that the reduction axioms of dynamic epistemic logic could possibly be viewed on par with differential equations of quantitative dynamical systems. As modal spaces are zero-dimensional, they are imbeddable in R cf. [37, Thm 50.5], turning clean maps into functions from R to R, possibly representable as discrete-time difference equations. An alternative approach is possible given by consulting Theorem 1. With Theorem 1, a connection arises between dynamic epistemic logic and dynamic topological logic (see e.g. [23,24,34,35]): Each system (Xd,f) may be considered a dynamic topological model with atom set LΛ and the 'next' operator's semantics given by an application of f , equivalent to a 〈f〉 dynamic modality of DEL. The topological 'interior' operator has yet no DEL parallel. A 'henceforth' operator allows for a limited characterization of recurrence [35]. We are wondering about and wandering around the connections between a limit set operator with semantics x  [ωf ]φ iff y  φ for all y ∈ ωf (x), dynamic topological logic and the study of oscillations suggested by van Benthem [11]. With the focal point on pointed Kripke models and action model transformations, we have only considered a special case of logical dynamics. It is our firm belief that much of the methodology here suggested is generalizable: With structures described logically using a countable language, the notion of logical convergence will coincide with topological convergence in the Stone topology on the quotient space modulo logical equivalence, and the metrics introduced will, mutatis mutandis, be applicable to said space [31]. The continuity of maps and compactness of course depends on what the specifics of the chosen model transformations and the compactness of the logic amount to. Acknowledgements The contribution of R.K. Rendsvig was funded by the Swedish Research Council through the Knowledge in a Digital World project and by The Center for Information and Bubble Studies, sponsored by The Carlsberg Foundation. The contribution of D. Klein was partially supported by the Deutsche Forschungsgemeinschaft (DFG) and Grantová agentura České republiky (GAČR) as part of the joint project From Shared Evidence to Group Attitudes [RO 4548/6-1]. 19 In the omitted part of the quotation from the introduction. References 1. G. Aucher. Generalizing AGM to a multi-agent setting. Logic Journal of IGPL, 18(4):530–558, 2010. 2. A. Baltag and L. S. Moss. Logics for Epistemic Programs. Synthese, 139(2):165– 224, 2004. 3. A. Baltag, L. S. Moss, and S. Solecki. The Logic of Public Announcements, Common Knowledge, and Private Suspicions. In TARK 1998. M.Kaufmann, 1998. 4. A. Baltag and B. Renne. Dynamic epistemic logic. In The Stanford Encyclopedia of Philosophy. Fall 2016 edition, 2016. 5. A. Baltag and S. Smets. A Qualitative Theory of Dynamic Interactive Belief Revision. In Proc. LOFT 7. Amsterdam Univ. Press, 2008. 6. A. Baltag and S. Smets. Group Belief Dynamics Under Iterated Revision: Fixed Points and Cycles of Joint Upgrades. In TARK'09. ACM, 2009. 7. J. van Benthem. Games in Dynamic-Epistemic Logic. Bulletin of Economic Research, 53(1):219–249, 2001. 8. J. van Benthem. "One is a Lonely Number": Logic and Communication. In Logic Colloquium '02, Lecture Notes in Logic, 27. Association for Symbolic Logic, 2006. 9. J. van Benthem. Dynamic logic for belief revision. Journal of Applied Non-Classical Logics, 17(2):129–155, 2007. 10. J. van Benthem. Logical Dynamics of Information and Interaction. Cambridge University Press, 2011. 11. J. van Benthem. Oscillations, Logic, and Dynamical Systems. In The Facts Matter. College Publications, 2016. 12. J. van Benthem, J. van Eijck, and B. Kooi. Logics of communication and change. Information and Computation, 204(11):1620–1662, 2006. 13. J. van Benthem, J. Gerbrandy, T. Hoshi, and E. Pacuit. Merging Frameworks for Interaction. Journal of Philosophical Logic, 38(5):491–526, 2009. 14. P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Camb. Univ. Press, 2001. 15. T. Bolander and M. Birkegaard. Epistemic planning for singleand multi-agent systems. Journal of Applied Non-Classical Logics, 21(1):9–34, 2011. 16. T. Bolander, M. Jensen, and F. Schwarzentruber. Complexity results in epistemic planning. In Proc. IJCAI 2015. AAAI Press, 2015. 17. T. Caridroit, S. Konieczny, T. de Lima, and P. Marquis. On Distances Between KD45n Kripke Models and Their Use for Belief Revision. In ECAI 2016. IOS Press, 2016. 18. C. Dégremont. The Temporal Mind: Observations on the logic of belief change in interactive systems. PhD thesis, University of Amsterdam, 2010. 19. H. van Ditmarsch and B. Kooi. Semantic Results for Ontic and Epistemic Change. In Logic and the Foundations of Game and Decision Theory (LOFT 7), Texts in Logic and Games, Vol. 3. Amsterdam University Press, 2008. 20. H. van Ditmarsch, W. van der Hoek, and B. Kooi. Dynamic Epistemic Logic. Springer, 2008. 21. T. Eisner, B. Farkas, M. Haase, and R. Nagel. Operator Theoretic Aspects of Ergodic Theory. Springer International Publishing, 2015. 22. R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning About Knowledge. The MIT Press, 1995. 23. D. Fernández-Duque. A sound and complete axiomatization for Dynamic Topological Logic. Journal of Symbolic Logic, 77(3):1–26, 2012. 24. D. Fernández-Duque. Dynamic topological logic of metric spaces. Journal of Symbolic Logic, 77(1):308–328, 2012. 25. P. Girard, J. Seligman, and F. Liu. General Dynamic Dynamic Logic. In Advances in modal logics, vol 9. College Publications, 2012. 26. V. Goranko. Logical Topologies and Semantic Completeness. In Logic Colloquium'99. Lecture Notes in Logic 17, AK Peters, 2004. 27. V. Goranko and M. Otto. Model Theory of Modal Logic. In Handbook of Modal Logic. Elsevier, 2008. 28. Y. J. Halpern and Y. Moses. Knowledge and Common Knowledge in a Distributed Environment. Journal of the ACM, 37(3):549–587, 1990. 29. B. Hasselblatt and A. Katok. Principal structures. In Handbook of Dynamical Systems, Vol. 1A. Elsevier, 2002. 30. J. Hintikka. Knowledge and Belief: An Introduction to the Logic of the Two Notions. College Publications, 2nd, 2005 edition, 1962. 31. D. Klein and R. K. Rendsvig. Metrics for Formal Structures, with an Application to Kripke Models and their Dynamics. arXiv:1704.00977, 2017. 32. D. Klein and R. K. Rendsvig. Turing Completeness of Finite, Epistemic Programs. arXiv:1706.06845, 2017. 33. B. Kooi and B. Renne. Generalized Arrow Update Logic. In TARK 2011, New York, NY, USA, 2011. ACM. 34. P. Kremer and G. Mints. Dynamical Topological Logic. Bulleting of Symbolic Logic, 3:371–372, 1997. 35. P. Kremer and G. Mints. Dynamic Topological Logic. In Handbook of Spatial Logics. Springer, 2007. 36. D. Lind and B. Marcus. An Introduction to Symbolic Dynamics and Coding. Cambridge University Press, 1995. 37. J. R. Munkres. Topology. Prentice-Hall, 2nd edition, 2000. 38. J. A. Plaza. Logics of public communications. In Proceedings of the 4th International Symposium on Methodologies for Intelligent Systems, 1989. 39. R. K. Rendsvig. Towards a Theory of Semantic Competence. Master's thesis, Dept. of Philosophy and Science Studies and Dept. of Mathematics, Roskilde University, 2011. 40. R. K. Rendsvig. Diffusion, Influence and Best-Response Dynamics in Networks: An Action Model Approach. In Proc. ESSLLI 2014 Stud. arXiv:1708.01477, 2014. 41. R. K. Rendsvig. Pluralistic ignorance in the bystander effect: Informational dynamics of unresponsive witnesses in situations calling for intervention. Synthese, 191(11):2471–2498, 2014. 42. R. K. Rendsvig. Model Transformers for Dynamical Systems of Dynamic Epistemic Logic. In Logic, Rationality, and Interaction, LNCS. Springer, 2015. 43. T. Sadzik. Exploring the Iterated Update Universe. ILLC PP-2006-26, 2006. 44. J. de Vries. Topological Dynamical Systems. de Gruyter, 2014.