Convergence, Continuity and Recurrence in Dynamic Epistemic Logic

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.

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,41,42,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

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, Sect. 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 Sect. 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,3,4,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 $\varPhi$ of atoms and a finite set I of agents. Where $p\in \varPhi$ and $i\in I$, define the language $\mathcal {L}$ by

$$ \varphi :=\top \;|\;p\;|\;\lnot \varphi \;|\;\varphi \wedge \varphi \;|\;\square _{i}\varphi . $$

Modal logics may be formulated in $\mathcal {L}$. By a logic $\varLambda$ we refer only to extensions of the minimal normal modal logic K over the language $\mathcal {L}$. With $\varLambda$ given by context, let $\varvec{\varphi }$ be the set of formulas $\varLambda$-provably equivalent to $\varphi$. Denote the resulting partition $\{\varvec{\varphi }:\varphi \in \mathcal {L}\}$ of $\mathcal {L}$ by $\varvec{\mathcal {L}}_{\varLambda }$.¹ Call $\varvec{\mathcal {L}}_{\varLambda }$’s elements $\varLambda$ -propositions.

We use relational semantics to evaluate formulas. A Kripke model for $\mathcal {L}$ is a tuple $M=([\![M]\!],R,[\![\cdot ]\!])$ where $[\![M]\!]$ is a countable, non-empty set of states, $R:I\longrightarrow \mathcal {P}([\![M]\!]\times [\![M]\!])$ assigns to each $i\in I$ an accessibility relation $R_{i}$, and $[\![\cdot ]\!]:\varPhi \longrightarrow \mathcal {P}([\![M]\!])$ is a valuation, assigning to each atom a set of states. With $s\in [\![M]\!]$, call $Ms=([\![M]\!],R,[\![\cdot ]\!],s)$ a pointed Kripke model. The used semantics are standard, including the modal clause:

$$ Ms\vDash \square _{i}\varphi \text { iff for all }t~{:}\, sR_{i}t\text { implies }Mt\vDash \varphi . $$

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 $\varvec{\mathcal {L}}_{\varLambda }$ modal space of a set of pointed Kripke models X is the set $\varvec{X}=\{\varvec{x}:x\in X\}$ for $\varvec{x}=\{y\in X:y\vDash \varphi \text { iff }x\vDash \varphi \; \textit{for}\; \textit{all}\;\varvec{\varphi }\in \varvec{\mathcal {L}}_{\varLambda }\}$.

Working with an $\varvec{\mathcal {L}}_{\varLambda }$ 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 $\varLambda$.

In a modal space, how may we conceptualize that a sequence $\varvec{x_{1}},\varvec{x_{2}},...$ converges to some point $\varvec{x}$? Focusing on the concept from which we derive the notion of identity in modal spaces, namely $\varLambda$-propositions, we find it natural to think of $\varvec{x_{1}},\varvec{x_{2}},...$ as converging to $\varvec{x}$ just in case $\varvec{x_{n}}$ moves towards satisfying all the same $\varLambda$-propositions as $\varvec{x}$ as n goes to infinity. We thus offer the following definition:

Definition 2

A sequence of points $\varvec{x_{1}},\varvec{x_{2}},...$ in an $\varvec{\mathcal {L}}_{\varLambda }$ modal space $\varvec{X}$ is said to logically converge to the point $\varvec{x}$ in $\varvec{X}$ iff for every $\varvec{\varphi }\in \varvec{\mathcal {L}}_{\varLambda }$ for which $x\vDash \varphi$, there is an $N\in \mathbb {N}$ such that $x_{n}\vDash \varphi$ for all $n\ge 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 $\mathcal {T}$ on a set X, a sequence of points $x_{1},x_{2},...$ is said to converge to x in the topological space $(X,\mathcal {T})$ iff for every open set $U\in \mathcal {T}$ containing x, there is an $N\in \mathbb {N}$ such that $x_{n}\in U$ for all $n\ge 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 [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 $\varvec{X}$ be a modal space for which modal equivalence and bisimilarity coincide² and let relate $x,y\in X$ iff x and y are n -bisimilar. Then proving

a metric on $\varvec{X}$ is trivial. We refer to $d_{B}$ as the n -bisimulation metric, and to the induced metric topology as the n -bisimulation topology, denoted $\mathcal {T}_{B}$. A basis of the topology $\mathcal {T}_{B}$ is given by the set of elements .

Considering the intimate link between modal logic and bisimulation, we consider both n-bisimulation metric and topology highly natural.³ Alas, logical convergence does not:

Proposition 1

Logical convergence in arbitrary modal space $\varvec{X}$ does not imply convergence in the topological space $(\varvec{X},\mathcal {T}_{B})$.

Proof

Let $\varvec{X}$ be an $\varvec{\mathcal {L}}_{\varLambda }$ modal space with $\mathcal {L}$ based on the atoms $\varPhi =\{p_{k}:k\in \mathbb {N}\}$. Let $x\in X$ satisfy $\square \bot$ and $p_{k}$ for all $k\in \mathbb {N}$. Let $\varvec{x_{1}},\varvec{x_{2}},...$ be a sequence in $\varvec{X}$ such that for all $k\in \mathbb {N}$, $x_{k}$ satisfies $\square \bot$, $p_{m}$ for all $m\le k$, and $\lnot p_{l}$ for all $l>k$. Then for all $\varvec{\varphi }\in \varvec{\mathcal {L}}_{\varLambda }$ for which $x\vDash \varphi$, there is an N such that $x_{n}\vDash \varphi$ for all $n\ge N$, hence the sequence $\varvec{x_{1}},\varvec{x_{2}},...$ converges to $\varvec{x}$. There does not, however, exist any $N'$ such that $\varvec{x}_{n'}\in B_{\varvec{x}0}$ for all $n'\ge N'$. Hence $\varvec{x_{1}},\varvec{x_{2}},...$ does not converge to $\varvec{x}$ in $\mathcal {T}_{B}$.   $\square$

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 $\mathcal {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 $\varphi$ with an open set U while replacing satisfaction $\vDash$ with inclusion $\in$ transforms the former definition into the latter. Hence the collection of sets $U_{\varvec{\varphi }}=\{\varvec{x}\in \varvec{X}:x\vDash \varphi \}$, $\varvec{\varphi }\in \varvec{\mathcal {L}}_{\varLambda }$, 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, $\mathcal {T}_{S}$.

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 $\varvec{\mathcal {L}}_{\varLambda }$ modal space $\varvec{X}$, a sequence $\varvec{x_{1}},\varvec{x_{2}},...$ logically converges to the point $\varvec{x}$ if, and only if, it converges to $\varvec{x}$ in $(\varvec{X},\mathcal {T}_{S})$.

Proof

Assume $\varvec{x_{1}},\varvec{x_{2}},...$ logically converges to $\varvec{x}$ in $\varvec{X}$ and that U containing $\varvec{x}$ is open in $\mathcal {T}_{S}$. Then there is a basis element $U_{\varvec{\varphi }}\subseteq U$ with $\varvec{x}\in U_{\varvec{\varphi }}$. So $x\vDash \varphi$. By assumption, there exists an N such that $x_{n}\vDash \varphi$ for all $n\ge N$. Hence $\varvec{x_{n}}\in U_{\varvec{\varphi }}\subseteq U$ for all $n\ge N$.

Assume $\varvec{x_{1}},\varvec{x_{2}},...$ converges to $\varvec{x}$ in $(\varvec{X},\mathcal {T}_{S})$ and let $x\vDash \varphi$. Then $\varvec{x}\in U_{\varvec{\varphi }}$, which is open. As the sequence converges, there exists an N such that $\varvec{x_{n}}\in U_{\varvec{\varphi }}$ for all $n\ge N$. Hence $x_{n}\vDash \varphi$ for all $n\ge N$.    $\square$

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 $\varvec{X}$ characterizable by a single $\varLambda$-proposition $\varvec{\varphi }\in \varvec{\mathcal {L}}_{\varLambda }$ is clopen. If the logic $\varLambda$ is compact and $\varvec{X}$ saturated (see footnote 7), also the converse is true: every clopen set is of the form $U_{\varphi }$ for some $\varphi$. 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 $\varLambda$-propositions, and a subset if closed, but not open, iff it is characterizable only by an infinitary conjunction of $\varLambda$-propositions. The Stone topology thus transparently reflects the properties of logic, language and topology. Moreover, it enjoys practical topological properties:

Proposition 3

For any $\varvec{\mathcal {L}}_{\varLambda }$ modal space $\varvec{X}$, $(\varvec{X},\mathcal {T}_{S})$ is Hausdorff and totally disconnected. If $\varLambda$ is (logically) compact ⁴ and $\varvec{X}$ is saturated ⁵, then $(\varvec{X},\mathcal {T}_{S})$ 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].   $\square$

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\subseteq \varvec{\mathcal {L}}_{\varLambda }$ contain for every $\varvec{\psi }\in \varvec{\mathcal {L}}_{\varLambda }$ some $\{\varvec{\varvec{\varphi }}_{i}\}_{i\in I}$ that $\varLambda$-entails either $\mathbf {\varvec{\psi }}$ or $\mathbf {\varvec{\lnot \psi }}$, and let $\varvec{\varphi }_{1},\varvec{\varphi }_{2},...$ be an enumeration of D.

Let $\varvec{X}$ be an $\varvec{\mathcal {L}}_{\varLambda }$ modal space. For all $\varvec{x},\varvec{y}\in \varvec{X}$, for all $k\in \mathbb {N}$, let

Let $w:D\longrightarrow \mathbb {R}_{>0}$ assign strictly positive weight to each $\varvec{\varphi }_{k}$ in D such that $(w(\varvec{\varphi }_{n}))$ forms a convergent series. Define the function $d_{w}:\varvec{X}^{2}\longrightarrow \mathbb {R}$ by

$$ d_{w}(\varvec{x},\varvec{y})=\sum _{k=0}^{\infty }w(\varvec{\varphi }_{k})d_{k}(\varvec{x},\varvec{y}) $$

for all $\varvec{x},\varvec{y}\in \varvec{X}$. The set of these functions is denoted $D_{\varvec{X}}$. Let $\mathcal {D}_{D,\varvec{X}}=\cup _{D\subseteq \varvec{\mathcal {L}}_{\varLambda }}D_{\varvec{X}}$.

We refer to [31] for the proof establishing the following proposition:

Proposition 4

Let $\varvec{X}$ be an $\varvec{\mathcal {L}}_{\varLambda }$ modal space and $d_{w}$ belong to $\mathcal {D}_{\varvec{X}}$. Then $d_{w}$ is a metric on $\varvec{X}$ and the metric topology $\mathcal {T}_{w}$ induced by $d_{w}$ on $\varvec{X}$ is the Stone topology of $\varLambda$.

For a metric space $(\varvec{X},d)$, we will also write $\varvec{X}_{d}$.

With variable parameters D and w, $\mathcal {D}_{\varvec{X}}$ 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 $\varvec{X}$ is an $\varvec{\mathcal {L}}_{\varLambda }$ modal space with $\mathcal {L}$ based on a finite atom set, then $\mathcal {D}_{\varvec{X}}$ contains a topological equivalent to the n-bisimulation metric.

Proof

(sketch). As $\mathcal {L}$ is based on a finite set of atoms, for each $\varvec{x}\in \varvec{X},n\in \mathbb {N}_{0}$, there exists a characteristic formula $\varphi _{x,n}$ such that $y\vDash \varphi _{x,n}$ iff , cf. [27]. Let $D_{n}=\{\varvec{\varphi _{x,n}}:\varvec{x}\in \varvec{X}\}$ and $D=\cup _{n\in \mathbb {N}_{0}}D_{n}$. Then each $D_{n}$ is finite and D satisfies Definition 3. Finally, let $w(\varvec{\varphi })=\frac{1}{|D_{n}|}\cdot \frac{1}{2^{n+1}}$ for $\varvec{\varphi }\in D_{n}$. Then $d_{w}\in \mathcal {D}_{\varvec{X}}$ and is equivalent to the n-bisimulation metric $d_{b}$.   $\square$

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 $\varvec{X}$ is an $\varvec{\mathcal {L}}_{\varLambda }$ modal space with $\mathcal {L}$ based on a countably infinite atom set, then the n-bisimulation metric topology on $\varvec{X}$ is strictly finer than the Stone topology on $\varvec{X}$.

Proof (sketch)

We refer to [31] for details, but for $\mathcal {T}_{B}\not \subseteq \mathcal {T}_{S}$, note that the set $B_{\varvec{x}0}$ used in the proof of Proposition 1, is open in $\mathcal {T}_{B}$, but not in $\mathcal {T}_{S}$.    $\square$

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.⁶

A multi-pointed action model is a tuple $\varSigma {\scriptstyle \varGamma }=([\![\varSigma ]\!],\mathsf {R},pre,post,\varGamma )$ where $[\![\varSigma ]\!]$ is a countable, non-empty set of actions. The map $\mathsf {R}:I\rightarrow \mathcal {P}([\![\varSigma ]\!]\times [\![\varSigma ]\!])$ assigns an accessibility relation $\mathsf {R}_{i}$ on $[\![\varSigma ]\!]$ to each agent $i\in I$. The map ${pre:[\![\varSigma ]\!]\rightarrow \mathcal {L}}$ assigns to each action a precondition, and the map ${post:[\![\varSigma ]\!]\rightarrow \mathcal {L}}$ assigns to each action a postcondition,⁷ which must be $\top$ or a conjunctive clause⁸ over $\varPhi$. Finally, $\emptyset \not =\varGamma \subseteq [\![\varSigma ]\!]$ 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 $\varSigma {\scriptstyle \varGamma }$ precondition finite if the set $\{\varvec{pre(\sigma )}\in \varvec{\mathcal {L}}_{\varLambda }:\sigma \in [\![\varSigma ]\!]\}$ is finite. This is needed for our proof of continuity. Call $\varSigma {\scriptstyle \varGamma }$ exhaustive over X if for all $x\in X$, there is a $\sigma \in \varGamma$ such that $x\vDash pre(\sigma )$. This conditions ensures that the action model $\varSigma {\scriptstyle \varGamma }$ is universally applicable on X. Finally, call $\varSigma {\scriptstyle \varGamma }$ deterministic over X if $X\vDash pre(\sigma )\wedge pre(\sigma ')\rightarrow \bot$ for each $\sigma \ne \sigma '\in \varGamma$. Together with exhaustivity, this condition ensures that the product of $\varSigma {\scriptstyle \varGamma }$ and any $Ms\in X$ is a (single-)pointed Kripke model, i.e., that the actual state after the updates is well-defined and unique.

Let $\varSigma {\scriptstyle \varGamma }$ be exhaustive and deterministic over X and let $Ms\in X$. Then the product update of Ms with $\varSigma {\scriptstyle \varGamma }$, denoted $Ms\otimes \varSigma {\scriptstyle \varGamma }$, is the pointed Kripke model $([\![M\varSigma ]\!],R',[\![\cdot ]\!]',s')$ with

$$\begin{aligned}{}[\![M\varSigma ]\!]= & {} \left\{ (s,\sigma )\in [\![M]\!]\times [\![\varSigma ]\!]:(M,s)\vDash pre(\sigma )\right\} \\ R'= & {} \left\{ ((s,\sigma ),(t,\tau )):(s,t)\in R_{i}\text { and }(\sigma ,\tau )\in \mathsf {R}_{i}\right\} ,\text { for all }i\in N\\ [\![p]\!]'= & {} \left\{ (s,\sigma )\!:\!s\in [\![p]\!]\!,post(\sigma )\nvDash \lnot p\right\} \cup \left\{ (s,\sigma )\!:\!post(\sigma )\vDash p\right\} ,\text { for all }p\in \varPhi \\ s'= & {} (s,\sigma ):\sigma \in \varGamma \text { and }Ms\vDash pre(\sigma ) \end{aligned}$$

Call $\varSigma {\scriptstyle \varGamma }$ closing over X if for all $x\in X,$ $x\otimes \varSigma {\scriptstyle \varGamma }\in X$. With $\varSigma {\scriptstyle \varGamma }$ exhaustive and deterministic, $\varSigma {\scriptstyle \varGamma }$ and $\otimes$ induce a well-defined total map on X.

The class of maps of interest in the present is then the following:

Definition 4

Let $\varvec{X}$ be an $\varvec{\mathcal {L}}_{\varLambda }$ modal space. A map $\varvec{f}:\varvec{X}\rightarrow \varvec{X}$ is called clean if there exists a precondition finite, multi-pointed action model $\varSigma {\scriptstyle \varGamma }$ closing, deterministic and exhaustive over X such that $\varvec{f}(\varvec{x})=\varvec{y}$ iff $x\,\otimes \varSigma {\scriptstyle \,\varGamma }\in \varvec{y}$ for all $\varvec{x}\in \varvec{X}$.

Clean maps are total by the assumptions of being closing and exhaustive. They are well-defined as $\varvec{f}(\varvec{x})$ is independent of the choice of representative for $\varvec{x}$: If $x'\in \varvec{x}$, then $x'\otimes \varSigma {\scriptstyle \varGamma }$ and $x\otimes \varSigma {\scriptstyle \varGamma }$ are modally equivalent and hence define the same point in $\varvec{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 $\varvec{f}$ be a clean map on an $\varvec{\mathcal {L}}_{\varLambda }$ modal space $\varvec{X}$. Then $\varvec{f}$ is continuous with respect to the Stone topology of $\varLambda$.

Proof (sketch)

We defer to [31] for details, but offer a sketch: The map $\varvec{f}$ is shown uniformly continuous using the $\varepsilon$-$\delta$ formulation of continuity. The proof relies on a lemma stating that for every $d_{w}\in \mathcal {D}_{\varvec{X}}$ and every $\epsilon >0$, there are formulas $\chi _{1},\ldots ,\chi _{l}\in \mathcal {L}$ such that every $x\in X$ satisfies some $\chi _{i}$ and whenever $y\vDash \chi _{i}$ and $z\vDash \chi _{i}$ for some $i\le l$, then $d_{w}(y,z)<\epsilon$. The main part of the proof establishes the claim that there is a function $\varvec{\delta }:\mathcal {L}\rightarrow (0,\infty )$ such that for any $\varphi \in \mathcal {L}$, if $f(x)\vDash \varphi$ and $d_{\mathbf {a}}(x,y)<\varvec{\delta }(\varphi )$, then $f(y)\vDash \varphi$. Setting $\delta =\min \{\varvec{\delta }(\chi _{i}):i\le l\}$ then yields a $\delta$ with the desired property.    $\square$

With Proposition 7, we are positioned to state our main theorem:

Theorem 1

Let $\varvec{f}$ be a clean map on a saturated $\varvec{\mathcal {L}}_{\varLambda }$ modal space $\varvec{X}$ with $\varLambda$ compact and let $d\in \mathcal {D}_{\varvec{X}}$. Then $(\varvec{X}_{d},\varvec{f})$ is a topological dynamical system.

Proof

Propositions 2, 3, 4 and 7 jointly imply that $\varvec{X}_{d}$ is a compact metric space on which $\varvec{f}$ is continuous, thus satisfying the requirements of e.g. [21, 29, 44].    $\square$

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 $X_{d}$ and $x\in X_{d}$. A point $y\in X$ is a limit point ⁹ for x under f if there is a strictly increasing sequence $n_{1},n_{2},...$ such that the subsequence $f^{n_{1}}(x),f^{n_{2}}(x),...$ of $(f^{n}(x))_{n\in \mathbb {N}_{0}}$ converges to y. The limit set of x under f is the set of all limit points for x, denoted $\omega _{f}(x)$. Notably, $\omega _{f}(x)$ is closed under f: For $y\in \omega _{f}(x)$ also $f(y)\in \omega _{f}(x)$. We immediately obtain that any modal system satisfying Theorem 1 has a nonempty limit set:

Proposition 8

Let $(\varvec{X}_{d},\varvec{f})$ be as in Theorem 1. For any point $\varvec{x}\in \varvec{X}$, the limit set of $\varvec{x}$ under $\varvec{f}$ is non-empty.

Proof

Since $\varvec{X}$ is is compact, every sequence in $\varvec{X}$ has a convergent subsequence, cf. e.g. [37, Theorem 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\in \omega _{f}(x)}$, i.e., if it is a limit point of itself.

The simplest structural form of recurrence is periodicity: For a point $x\in X$, call the set $\mathcal {O}_{f}(x)=\{f^{n}(x):n\in \mathbb {N}_{0}\}$ its orbit. The orbit $\mathcal {O}_{f}(x)$ is periodic if $f^{n+k}(x)=f^{n}(x)$ for some $n\ge 0,k>0$; the least such k is the period of $\mathcal {O}_{f}(x)$. Periodicity is thus equivalent to $\mathcal {O}_{f}(x)$ being finite. Related is the notion of a limit cycle: a periodic orbit $\mathcal {O}_{f}(x)$ is a limit cycle if it is the limit set of some y not in the period, i.e., if $\mathcal {O}_{f}(x)=\omega _{f}(y)$ for some $y\not \in \mathcal {O}_{f}(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 $\mathcal {O}_{f}(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].¹⁰ 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 $\varSigma {\scriptstyle \varGamma }$ finite if $[\![\varSigma ]\!]$ is finite, Boolean if $pre(\sigma )$ is a Boolean formula for all $\sigma \in [\![\varSigma ]\!]$, and static if $post(\sigma )=\top$ for all $\sigma \in [\![\varSigma ]\!]$. We apply the same terms to a clean map $\varvec{f}$ based on $\varSigma {\scriptstyle \varGamma }$. In this terminology, Sadzik showed that for any finite, Boolean, and static clean map $\varvec{f}:\varvec{X}\rightarrow \varvec{X}$, if the orbit $\mathcal {O}_{\varvec{f}}(\varvec{x})$ is periodic, then it has period 1.¹¹ This insightful result immediates the following:

Proposition 9

Let $(\varvec{X}_{d},\varvec{f})$ be as in Theorem 1 with $\varvec{f}$ finite, Boolean, and static. For all $\varvec{x}\in \varvec{X}$, the orbit $\mathcal {O}_{\varvec{f}}(\varvec{x})$ is periodic with period 1.

Proof

By Proposition 8, the limit set $\omega _{\varvec{f}}(\varvec{x})$ of $\varvec{x}$ under $\varvec{f}$ is non-empty. Sadzik’s result shows that it contains a single point. Hence $(\varvec{f}^{n}(\varvec{x}))_{n\in \mathbb {N}_{0}}$ converges to this point. As the limit set $\omega _{\varvec{f}}(\varvec{x})$ is closed under $\varvec{f}$, its unique point is a fix-point.    $\square$

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 $[\![x]\!]$. 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:

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 $\varSigma {\scriptstyle \varGamma }$ deterministic over X. Moreover, $\varSigma {\scriptstyle \varGamma }$ may be chosen 1. static, but non-Boolean, or 2. Boolean, but non-static.

Proof

(of Propositions 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 $\{\triangleright ,\mathtt {0},\mathtt {1},\mathtt {\sqcup }\}$, where the symbol $\triangleright$ is used to mark the starting cell and $\mathtt {\sqcup }$ is the blank symbol. We omit the exact description of the machine here. Of importance is the content of the tape: Omitting blank ($\mathtt {\sqcup }$) cells, natural numbers are represented as illustrated in Fig. 1.

Fig. 1.

Mirrored base-2 Turing tape representation of $0,..,9\in \mathbb {N}_{0}$, blank cells omitted. Notice that the mirrored notation causes perpetual change close to the start cell, $\triangleright$.

Initiated with its read-write head on the cell with the start symbol $\triangleright$ 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 $\varSigma {\scriptstyle \varGamma }$ on a set X cf. Lemma 1. Omitting the details¹², 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,¹³ 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 $\triangleright$.

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 $c_{0}$. Each state is labeled with a formula $\varphi _{\triangleright },\ \varphi _{0}$ or $\varphi _{1}$ expressing its content. Relations a and b allow expressing distance of cells: That $c_{0}$ satisfies $\lozenge _{a}(u\wedge \lozenge _{b}(e\wedge \varphi _{1}))$ exactly expresses that cell $c_{2}$ contains a 1. Omitted are reflexive loops for relations, and the additional structure marking cell content and read-write head position.

Let $(c_{n})_{n\in \mathbb {N}_{0}}$ be the sequence of configurations of the machine when initiated on a tape with content 0. Each $c_{n}$ may be represented by a pointed Kripke model, obtaining a sequence $(x_{n})_{n\in \mathbb {N}_{0}}$. By Lemma 1, there thus exists a $\varSigma {\scriptstyle \varGamma }$ such that for all n, $x_{n}\otimes \varSigma {\scriptstyle \varGamma }=x_{n+1}$. Hence, moving to the full modal space $\varvec{X}$ for the language used, a clean map $\varvec{f}:\varvec{X}\rightarrow \varvec{X}$ based on $\varSigma {\scriptstyle \varGamma }$ will satisfy $\varvec{f}(\varvec{x}_{n})=\varvec{x}_{n+1}$ for all n. The Turing machine’s run is thus emulated by $(\varvec{f}^{k}(\varvec{x}_{0}))_{k\in \mathbb {N}_{0}}$.

Let $(c'_{n})_{n\in \mathbb {N}_{0}}$ be the subsequence of $(c_{n})_{n\in \mathbb {N}_{0}}$ where the machine has finished the successor operation and returned its read write head to its starting position $\triangleright$, ready to embark on the next successor step. The tape of the first 9 of these $c_{n}'$ are depicted in Fig. 1. Let $(\varvec{x}'_{n})_{n\in \mathbb {N}_{0}}$ be the corresponding subsequence of $(\varvec{f}^{k}(\varvec{x}_{0}))_{k\in \mathbb {N}_{0}}$. We show that $(\varvec{x}'_{n})_{n\in \mathbb {N}_{0}}$ has uncountably many limit points:

For each subset Z of $\mathbb {N}$, let $c^{Z}$ be a tape with content 1 on cell i iff $i\in Z$ and 0 else. On the Kripke model side, let the corresponding $x^{Z}\in X$ be a model structurally identical to those of $(x'_{n})_{n\in \mathbb {N}_{0}}$, but satisfying $\varphi _{1}$ on all “cell states” distance $i\in Z$ from the designated “$\triangleright$” state, and $\varphi _{0}$ on all other.¹⁴ The set $\{x^{Z}:Z\subseteq \mathbb {N}\}$ is uncountable, and each $\varvec{x^{Z}}$ is a limit point of $\overline{\varvec{x}}$: For each $Z\subseteq \mathbb {N}$ and $n\in \mathbb {N}$, there are infinitely many k for which $x_{k}\vDash \varphi$ iff $x^{Z}\vDash \varphi$ for all $\varphi$ of modal depth at most n. Hence, for every n, the set $\{\varvec{x}_{k}:d_{b}(\varvec{x}_{k},\varvec{x^{Z}})<2^{-n}\}$ is infinite, with $d_{b}$ the equivalent of the n-bisimulation metric, cf. Proposition 5. Hence, for each of the uncountably many $Z\subseteq \mathbb {N}$, $\varvec{x^{Z}}$ is a limit point of the sequence $\varvec{\overline{x}}$.

Finally, every $\varvec{x}'_{k}\in (\varvec{x}'_{n})_{n\in \mathbb {N}_{0}}$ is recurrent: That $\varvec{x}'_{k}\in \omega _{\varvec{f}}(\varvec{x}'_{k})$ follows from $\varvec{x}'_{k}$ being a limit point of $(\varvec{x}'_{n})_{n\in \mathbb {N}_{0}}$, which it is as $\varvec{x}'_{k}=\varvec{x}^{Z}$ for some $Z\subseteq \mathbb {N}$.¹⁵ As the set of recurrent points is thus infinite, it cannot be periodic.    $\square$

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\in \mathbb {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.

Proof

For the given n, find a Turing machine that, from some configuration, loops with period n. From here, Lemma 1 does the job.    $\square$

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 non-static, 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.    $\square$

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 10 and 11 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 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 models¹⁶ 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 PDL-transformations of General Dynamic Dynamic Logic [25] given the signature change the operation involves.

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 notes¹⁷ 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 $\mathbb {R}$ cf. [37, Theorem 50.5], turning clean maps into functions from $\mathbb {R}$ to $\mathbb {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 $(\varvec{X}_{d},\varvec{f})$ may be considered a dynamic topological model with atom set $\varvec{\mathcal {L}}_{\varLambda }$ and the ‘next’ operator’s semantics given by an application of $\varvec{f}$, equivalent to a $\langle \varvec{f}\rangle$ 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\vDash [\omega _{\varvec{f}}]\varphi$ iff $y\vDash \varphi$ for all $\varvec{y}\in \omega _{\varvec{f}}(\varvec{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.