11institutetext: Fachbereich Mathematik, Philipps-Universität Marburg

# Saturated Kripke Structures as Vietoris Coalgebras

H. Peter Gumm  Mona Taheri

###### Abstract

We show that the category of coalgebras for the compact Vietoris endofunctor
$\mathbb{V}$ on the category $Top$ of topological spaces and continuous
mappings is isomorphic to the category of all modally saturated Kripke
structures. Extending a result of Bezhanishvili, Fontaine and Venema [4], we
also show that Vietoris subcoalgebras as well as bisimulations admit
topological closure and that the category of Vietoris coalgebras has a
terminal object.

##  1 Introduction

The theory of coalgebras has provided Computer Science with a much needed
general framework for dealing with all sorts of state based systems, with
their structure theories and their logics. The varied types of systems, be
they deterministic or nondeterministic automata, transition systems,
probabilistic or weighted systems, neighborhood systems or the like, are fixed
by the choice of an appropriate endofunctor $F$ on the category of sets. From
there on, with hardly any further assumptions, a mathematically pleasing
structure theory and corresponding modal logics can be developed, see e.g.
[20],[9],[10].

A particularly well behaved situation arises when choosing for $F$ the finite-
powerset functor $\mathbb{P}_{\omega}(-)$, perhaps augmented with a constant
component $\mathbb{P}(\Phi)$ representing sets of atomic formulas. Coalgebras
for the functor $\mathbb{P}_{\omega}(-)\times\mathbb{P}(\Phi)$ are precisely
all image finite Kripke structures. Their logic is the standard modal logic
based on the atomic formulae in $\Phi$, and they possess a terminal coalgebra
$T$, even though its description is always of an “indirect” nature (see [2, 3,
11]).

The well known Hennessy-Milner theorem[12], relating bisimulations and logical
equivalence is a consequence of image finiteness and will not continue to hold
for arbitrary Kripke structures, i.e. for coalgebras of type
$\mathbb{P}(-)\times\mathbb{P}(\Phi)$, see [14].

The theory of modal logic knows of a class of Kripke structures, which lies
between image finite structures and arbitrary Kripke structures and which
continues to enjoy the Hennessy-Milner theorem. These structures are called
_modally saturated_ , or simply $m$-saturated[8]. Unfortunately, though, there
seems to be no $Set$-functor $F$, somehow located in between
$\mathbb{P}_{\omega}(-)\times\mathbb{P}(\Phi)$ and
$\mathbb{P}(-)\times\mathbb{P}(\Phi)$, whose coalgebras would be just the
$m$-saturated Kripke structures.

It is well known, that much of the theory of coalgebras can be generalized by
turning to other categories than $Set$, provided they are co-complete and come
with a reasonable factorization structure. Some of the examples studied in the
literature replace the base category $Set$ with the category $Rel$ of sets and
relations [15], with the category $Pos$ of posets [1] or $Cpo$ of complete
partial orders, with the category _Meas_ of measurable spaces [6][17], or the
category $Stone$ of Stone spaces. Relevant to this present work will be the
works of Kupke, Kurz and Venema[16] as well as Bezhanishvili, Fontaine and
Venema [4] regarding coalgebras for the Vietoris functor on the category of
Stone spaces, i.e. compact zero-dimensional Hausdorff spaces with continuous
mappings.

When extending the Vietoris functor from Stone spaces to arbitrary topological
spaces $\mathcal{X}$, two natural choices offer themselves for the object map:
either the collection of all closed subsets of $\mathcal{X}$ or the collection
of all compact subsets of $\mathcal{X}$, both equipped with appropriate
topologies. Each of these choices yields a functor, generalizing the mentioned
Vietoris functor on Stone spaces. Named the _lower Vietoris functor_ , resp.
the _compact Vietoris functor_ , these endofunctors on the category $Top$ of
topological spaces with continuous functions were explored in recent work by
Hofmann, Neves and Nora[13].

For our investigation of saturated Kripke structures, the _compact Vietoris
functor_ , which we denote by $\mathbb{V}(-),$ turns out to be appropriate. To
model saturated Kripke-Structures, we choose the endofunctor
$\mathbb{V}(-)\times\mathbb{P}(\Phi)$ on the category $Top$ of topological
spaces and continuous mappings, where the $\mathbb{P}(\Phi)$-part is a
constant component equipped with an appropriate topology, intuitively
representing a set of atomic propositions, as above. We show that
$\mathbb{V}(-)\times\mathbb{P}(\Phi)$ coalgebras precisely correspond to
$m$-saturated Kripke structures, in fact there is an isomorphism of categories
between the category of saturated Kripke structures and the category of all
topological coalgebras for the compact Vietoris functor
$\mathbb{V}(-)\times\mathbb{P}(\Phi)$.

This correspondence also yields a direct description of the terminal
$\mathbb{V}(-)\times\mathbb{P}(\Phi)$ coalgebra, which seems to be simpler and
more natural than the terminal $\mathbb{P}_{\omega}(-)\times\mathbb{P}(\Phi)$
coalgebra mentioned above: it is simply the Vietoris coalgebra corresponding
to the canonical model of normal modal logic over $\Phi.$

For Stone coalgebras we know from [4], that the topological closure $\bar{R}$
of a bisimulation $R$ is itself a bisimulation, again. We verify that their
arguments carry over to the more general case of arbitrary Vietoris
coalgebras, and we show also that a corresponding result holds true for
subcoalgebras in place of bisimulations. For this we need to prepare some
topological tools which may be interesting in their own right, relating
convergence in the Vietoris space $\mathbb{V}(\mathcal{X})$ to convergence in
the base space $\mathcal{X}$. In particular, topological nets
$(\kappa_{i})_{i\in I}$ converging to $\kappa$ in the Vietoris space
$\mathbb{V}(\mathcal{X})$ are shown to correspond, up to subnet formation, to
nets $(a_{i})_{i\in I}$ with $a_{i}\in\kappa_{i}$, converging in the base
space $\mathcal{X}$ to $a\in\kappa$, and conversely.

##  2 Preliminaries

For the remainder of this article, we shall fix a set $\Phi,$ the elements of
which shall be called _propositional variables_ or _atomic propositions_.

###  2.1 Kripke structures

###### Definition 1

A _Kripke structure (_ also called _Kripke model)_ $\mathcal{X}=(X,R,v)$
consists of a set $X$ of states together with a relation $R\subseteq X\times
X$, and a map $v:X\to\mathbb{P}(\Phi),$ where $\mathbb{P}$ denotes the
powerset functor.

In applications, $X$ will typically be a set of possible states of a system,
$R$ is called the _transition relation_ , describing the allowed transitions
between states from $X,$ and $v$ is called the _valuation_ , since $v(x)$
consists of all atomic propositions true in state $x.$ Instead of $(x,y)\in R$
we write $x\rightarrowtriangle y$ (or $x\rightarrowtriangle_{R}y$, if
necessary). The idea is that $x\rightarrowtriangle y$ expresses that it is
possible for the system to move from state $x$ to state $y$. Instead of a
relation, we can alternatively consider $R$ as a map $R:X\to\mathbb{P}(X)$.
This justifies the notation

$R(x):=\\{y\in X\mid(x,y)\in R\\},$

so $R(x)$ denotes the _successors_ of $x,$ i.e. all states reachable from $x$
in one step.

###### Definition 2

For subsets $U\subseteq X$ define $\langle R\rangle U:=\\{x\in X\mid\exists
y\in U.(x,y)\in R\\}$ and $[R]U:=\\{x\in X\mid\forall y\in X.(x,y)\in
R\implies y\in U\\}.$

Thus $x\in\langle R\rangle U$ if from $x$ it is _possible_ to reach an element
of $U$ in one step, and $x\in[R]U$ says that starting from $x,$ each
transition will _necessarily_ take us to $U$. Obviously, $\langle
R\rangle(X-U)=X-[R]U$, and $[R](X-U)=X-\langle R\rangle U$, so $\langle
R\rangle$ and $[R]$ are mutually expressible if complements are available.

###  2.2 Modal logic

Starting with the elements of $\Phi$__ as _atomic formulae,_ we obtain _modal
formulae_ by combining them with the standard boolean connectors $\wedge,$
$\vee,\neg$ or prefixing with the unary modal operator $\square.$ We also
allow the usual shorthands $\bigvee_{i\in I_{0}}\phi_{i}$ and $\bigwedge_{i\in
I_{0}}\phi_{i}$, whenever $I_{0}$ is a finite indexing set and each $\phi_{i}$
is a formula. Let $\mathcal{L}_{\Phi}$ be the set of all modal formulae so
definable.

_Validity_ $x\Vdash\phi,$ is defined for $x\in X$ and
$\phi\in\mathcal{L}_{\Phi}$ in the usual way (see [5]):

$\displaystyle x\Vdash p$ $\displaystyle:\iff$ $\displaystyle p\in v(x)\text{,
\,\,\,\,\,whenever $p\in\Phi$}$ $\displaystyle x\models\square\phi$
$\displaystyle:\iff$ $\displaystyle\forall y\in X.\,(x\rightarrowtriangle
y\implies y\models\phi).$

For the boolean connectives $\wedge,\vee,\neg$, validity is defined as
expected. We extend it to sets of formulas
$\Sigma\subseteq\mathcal{L}_{\Phi}$, by

$x\Vdash\Sigma\,\,:\iff\,\,\,\forall\phi\in\Sigma.\,x\Vdash\phi.\,\,\,\,\,\,$

For any $x\in X$ we put $\llbracket
x\rrbracket:=\\{\phi\in\mathcal{L}_{\Phi}\mid x\Vdash\phi\\}$ and, similarly,
for any $\phi\in\mathcal{L}_{\Phi}$ we set $\llbracket\phi\rrbracket:=\\{x\in
X\mid x\Vdash\phi\\}.$ Two elements $x,y$ from (possibly different) Kripke
structures are called _logically equivalent_ (in symbols $x\approx y$), if for
each formula $\phi\in\mathcal{L}_{\Phi}$ we have $x\models\phi\iff
y\models\phi.$ Restricted to a single Kripke structure, $\approx$ is the
kernel of the _semantic map_ $x\mapsto\llbracket x\rrbracket$, and hence an
equivalence relation. Similarly, two modal formulae $\phi,\psi$ are
_equivalent_ , and we write $\phi\equiv\psi,$ if for each element $x$ in any
Kripke structure we have $x\Vdash\phi\iff x\Vdash\psi.$

Adding a further modality $\diamondsuit$ to our logical language by defining
$\diamondsuit\phi:=\neg\square\neg\phi$ provides more than only a convenient
abbreviation. The resulting equivalences
$\neg\square\phi\equiv\diamondsuit\neg\phi$ and
$\neg\diamondsuit\phi\equiv\square\neg\phi$ allow one to push negations
inside, just as the deMorgan laws permit to do so for $\vee$ and $\wedge$, so
that each modal formula becomes equivalent to a modal formula in _negation
normal form_ (_nnf_), where negations may only occur only in front of an
atomic formula. We state this here for later reference:

###### Lemma 1

Every modal formula is equivalent to a modal formula in negation normal form
(nnf).

###  2.3 Bisimulations

###### Definition 3

A _bisimulation_ between two Kripke structures
$\mathcal{X}_{1}=(X_{1},R_{1},v_{1})$ and
$\mathcal{X}_{2}=(X_{2},R_{2},v_{2})$ is a relation $B\subseteqq X_{1}\times
X_{2}$ such that for each $(x,y)\in B$:

  1. 1.

$v_{1}(x)=v_{2}(y)$,

  2. 2.

$\forall x^{\prime}\in
X_{1}.\,x\rightarrowtriangle_{R_{1}}x^{\prime}\implies\exists y^{\prime}\in
X_{2}.\,y\rightarrowtriangle_{R_{2}}y^{\prime}\wedge\,x^{\prime}B\,y^{\prime}$,

  3. 3.

$\forall y^{\prime}\in
X_{2}.\,y\rightarrowtriangle_{R_{2}}y^{\prime}\implies\exists x^{\prime}\in
X_{1}.\,x\rightarrowtriangle_{R_{1}}x^{\prime}\wedge\,x^{\prime}B\,y^{\prime}.$

The empty relation $\emptyset\subseteq X_{1}\times X_{2}$ is clearly a
bisimulation, and the union of a family of bisimulations between
$\mathcal{X}_{1}$ and $\mathcal{X}_{2}$ is again a bisimulation, hence there
is a largest bisimulation between $\mathcal{X}_{1}$ and $\mathcal{X}_{2}$,
which we call $\sim_{\mathcal{X}_{1},\mathcal{X}_{2}}$ or simply $\sim$, when
$\mathcal{X}_{1}$ and $\mathcal{X}_{2}$ are clear from the context.

If $B_{1}\subseteq X_{1}\times X_{2}$ is a bisimulation between
$\mathcal{X}_{1}$ and $\mathcal{X}_{2}$, then the converse relation
$B_{1}^{-1}\subseteq X_{2}\times X_{1}$ is a bisimulation between
$\mathcal{X}_{2}$ and $\mathcal{X}_{1}$. Given another bisimulation $B_{2}$
between Kripke structures $\mathcal{X}_{2}$ and $\mathcal{X}_{3}$ then the
relational composition $B_{1}\circ B_{2}$ is a bisimulation between
$\mathcal{X}_{1}$ and $\mathcal{X}_{3}$.

A bisimulation _on_ a Kripke structure $\mathcal{X}=(X,R,v)$ is a bisimulation
between $\mathcal{X}$ and itself. The identity $\Delta_{X}=\\{(x,x)\mid x\in
X\\}$ is always a bisimulation on $\mathcal{X}$. Consequently, the largest
bisimulation _on_ $\mathcal{X}$ is an equivalence relation, denoted by
$\sim_{\mathcal{X}}$ or simply $\sim$. We say that two points $x\in X_{1}$ and
$y\in X_{2}$ are _bisimilar,_ if there exists a bisimulation $B$ with
$x\,B\,y$, which is the same as saying $x\sim y$. It is well known and easy to
check by induction:

###### Lemma 2

Bisimilar points satisfy the same formulae $\phi\in\mathcal{L}_{\Phi}$.

A converse to this lemma was shown by Hennessy and Milner for the case of
_image finite_ Kripke structures. Here, an element $x$ in a Kripke structure
$\mathcal{X}$ is called _image finite_ if it has only finitely many
successors, i.e. $\\{x^{\prime}\mid x\rightarrowtriangle x^{\prime}\\}$ is
finite. $\mathcal{X}$ is called image finite if each $x$ from $\mathcal{X}$ is
image finite. Thus Hennessy and Milner proved in [12]:

###### Proposition 1

If $x\in\mathcal{X}$ and $y\in\mathcal{Y}$ are image finite elements, then
$x\sim y$ iff $x\approx y.$

###  2.4 Homomorphisms and congruences

###### Definition 4

A homomorphism $\varphi:\mathcal{X}\to\mathcal{Y}$ between Kripke structures
$\mathcal{X}=(X,R_{\mathcal{X}},v_{\mathcal{X}})$ and
$\mathcal{Y}=(Y,R_{\mathcal{Y}},v_{\mathcal{Y}})$ is a map whose graph

$G(\varphi):=\\{(x,\varphi(x))\mid x\in X\\}$

is a bisimulation.111In the literature on Modal Logic (see e.g. [5],[8]),
homomorphisms are usually called “bounded morphisms”.

We call $\mathcal{X}$ a _homomorphic preimage_ of $\mathcal{Y}$, and if
$\varphi$ is surjective (which we indicate by writing
$\varphi:\mathcal{X}\twoheadrightarrow\mathcal{Y}$) then we call $\mathcal{Y}$
a _homomorphic image_ of $\mathcal{X}$. If $X\subseteq Y$and the inclusion map
$\iota:\mathcal{X}\to\mathcal{Y}$ is a homomorphism, then $\mathcal{X}$ is
called a _Kripke substructure_ of $\mathcal{Y}$.

It is easy to check that a subset $X\subseteq Y$ with the restrictions of
$R_{\mathcal{Y}}$ and $v_{\mathcal{Y}}$ to $X$ is a substructure of
$\mathcal{Y}$ if only if $R_{\mathcal{X}}(x)\subseteq X$ for each $x\in X.$ If
$\varphi:\mathcal{X}\to\mathcal{Y}$ is a homomorphism, then its kernel

$\ker\varphi:=\\{(x,x^{\prime})\in X\mid\varphi(x)=\varphi(x^{\prime})\\}$

is called a _congruence relation_. This is clearly an equivalence relation and
a bisimulation as well, since we can express it as a relation product of
$G(\varphi)$, the graph of $\varphi$, with its converse $G(\varphi)^{-1}$ as

$\ker\varphi=G(\varphi)\circ G(\varphi)^{-1}.$

##  3 Saturated structures

The notion of _saturation_ goes back to a similar concept of Fine in [7]. The
terminology $m$_-saturation_(or _modal saturation_) was adopted by [5] and
[8]:

###### Definition 5

An element $x$ is _$m$ -saturated_, if for each set $\Sigma$ of formulas, such
that each finite subset $\Sigma_{0}\subseteq\Sigma$ is satisfied at some
successor $y_{0}$ of $x,$ there is a successor $y$ of $x$ satisfying all
formulas in $\Sigma.$ A Kripke structure is called _$m$ -saturated_, if each
of its elements is saturated.

In the following we shall find it convenient to informally use infinitary
disjunctions $\bigvee_{i\in I}\phi_{i}$ – not as as a logical expressions but
as shorthands. In particular we write

$x\Vdash\square\bigvee_{i\in I}\phi_{i}$

as an abbreviation for

$\forall y.(x\rightarrowtriangle y\implies\exists i\in I.\,y\models\phi_{i}).$

With this shorthand, the above definition can be reformulated:

###### Lemma 3

An element $x$ in a Kripke model $\mathcal{X}=(X,R,v)$ is _$m$_ -saturated, if
for each family $(\phi_{i})_{i\in I}$ such that $x\Vdash\square\bigvee_{i\in
I}\phi_{i}$ there exists a finite subset $I_{0}\subseteq I$ with
$x\Vdash\square\bigvee_{i\in I_{0}}\phi_{i}$.

Image finite elements are clearly saturated, but they are not the only ones.
Below, we consider two examples of Kripke structures. In both cases, we assume
$v(x):=\emptyset$ for each $x$:

###### Example 1

On the set $S:=\\{s\\}\cup\\{s_{i}\mid i\in\mathbb{N}\\}$ consider the
relation $R=\\{(s,s_{i})\mid i\in\mathbb{N}\\}\cup\\{(s_{i+1},s_{i})\mid
i\in\mathbb{N}\\}$. Then for each $s_{i}$ we have
$s_{i}\Vdash\square^{i+1}\bot$, but $s_{i}\not\Vdash\square^{j}\bot$ for
$j\leq i$. Therefore $(S,R,v)$ is not saturated, since
$s\Vdash\square\bigvee_{i\in\mathbb{N}}(\square^{i+1}\bot)$, but for no finite
$I_{0}\subseteq\mathbb{N}$ do we have $s\Vdash\square\bigvee_{i\in
I_{0}}(\square^{i+1}\bot)$.

$\textstyle{s\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{...}$$\textstyle{s_{0}}$$\textstyle{s_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{s_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{...\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

Next, we modify the above structure by adding a “point at infinity”
$s_{\infty}$ together with a self-loop $s_{\infty}\rightarrowtriangle
s_{\infty}$ to obtain the following structure:

###### Example 2

$\textstyle{s\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{...}$$\textstyle{s_{0}}$$\textstyle{s_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{s_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{...\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{s_{\infty}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

The point at infinity changes the situation. We claim:

###### Lemma 4

The Kripke structure in Example 2 is saturated.

###### Proof

We first observe that for $s_{\infty}$ and any formula $\phi$ we have:

$s_{\infty}\Vdash\diamondsuit\phi\iff s_{\infty}\Vdash\phi\iff
s_{\infty}\Vdash\square\phi.$

Next we prove for each formula $\phi$:

###### Claim

_If $s_{\infty}\Vdash\phi$, then there is some $k\in\mathbb{N}$ such that
$s_{i}\Vdash\phi$ for each $i\geq k$._

We prove this claim by induction over the construction of nnf-formulae:

  * •

For $\phi=\bot$ and $\phi=\top,$ the claim is vacuously true. For
$\phi=\phi_{1}\wedge\phi_{2},$ from $s_{\infty}\Vdash\phi_{1}\wedge\phi_{2}$,
the hypothesis yields $k_{1}$ and $k_{2}$ such that $s_{i}\Vdash\phi_{1}$ for
each $i\geq k_{1}$ and $s_{i}\Vdash\phi_{2}$ for each $i\geq k_{2}$. With
$k=max(k_{1},k_{2})$ we obtain $s_{i}\Vdash\phi_{1}\wedge\phi_{2}$ for $i\geq
k$. For $\phi=\phi_{1}\vee\phi_{2}$ we could similarly choose
$k=min(k_{1},k_{2}).$

  * •

For $\phi=\square\phi_{1}$ we have $s_{\infty}\Vdash\phi\iff
s_{\infty}\Vdash\phi_{1}$. By assumption, there is some $k$ such that
$s_{i}\Vdash\phi_{1}$ for each $i\geq k$. It follows that
$s_{i}\Vdash\square\phi_{1}$ for $i\geq k+1.$ Similarly we argue for
$\phi=\diamondsuit\phi_{1}$.

Now, to show that $s$ in the structure of Example 2 is saturated, assume that
$s\Vdash\square\bigvee_{i\in I}\phi_{i}$, then there is some $i_{\infty}\in I$
such that $s_{\infty}\Vdash\phi_{i_{\infty}}$. The claim above provides a $k$
such that for each $j\geq k$ we have $s_{j}\Vdash\phi_{i_{\infty}}$, and for
each $j<k$ there is some $i_{j}\in I$ with $s_{j}\Vdash\phi_{i_{j}}$.
Altogether then with
$I_{0}:=\\{i_{0},i_{1},...,i_{k-1}\\}\cup\\{i_{\infty}\\}$ we have
$s\Vdash\square\bigvee_{i\in I_{0}}\phi_{i}$.

Thus $s$ is saturated, and all other points in the structure are image finite,
hence they are saturated, too.

We can extend Lemma 2 to “infinitary formulas” in the following sense:

###### Lemma 5

[Bisimulations preserve saturation] If $B\subseteq X_{1}\times X_{2}$ is a
bisimulation and $(x,y)\in B$, then $x$ is saturated iff $y$ is saturated.

###### Proof

Assume that $x$ is saturated and $(x,y)\in B$. Suppose
$y\Vdash\square\bigvee_{i\in I}\phi_{i}$, then each $y^{\prime}$ with
$y\rightarrowtriangle y^{\prime}$ satisfies one of the formulas $\phi_{i}$.
Each $x^{\prime}$ with $x\rightarrowtriangle x^{\prime}$ is bisimilar to some
$y^{\prime}$ with $y\rightarrowtriangle y^{\prime}$, so by Lemma 2 each
$x^{\prime}$ satisfies one of the $\phi_{i}$. This means that
$x\Vdash\square\bigvee_{i\in I}\phi_{i}$. By saturation of $x$ there is a
finite subset $I_{0}\subseteq I$ with $x\Vdash\square\bigvee_{i\in
I_{0}}\phi_{i}$. The latter, being an honest modal formula, is preserved by
bisimulation, so $y\Vdash\square\bigvee_{i\in I_{0}}\phi_{i}$.

Lemma 2 implies that for each $x\in\mathcal{X}$ and each formula $\phi$ we
have

$x\Vdash\phi\iff\varphi(x)\Vdash\phi$ (3.1)

and Lemma 5 tells us that $x$ is saturated iff $\varphi(x)$ is saturated,
which we might combine to:

###### Corollary 1

Homomorphisms preserve and reflect saturation.

On the level of Kripke structures, rather than elements, this translates to:

###### Corollary 2

Homomorphic images and homomorphic preimages of saturated Kripke structures
are saturated.

Let $\mathcal{X}$ and $\mathcal{Y}$ be Kripke structures. Recall that for
elements $x\in X$ and $y\in Y$ we write $x\approx y$, if they are logically
equivalent, i.e. they satisfy the same modal formulae. The following
generalization of the Hennessy-Milner theorem [12] is credited in [5] to
unpublished notes of Alfred Visser:

###### Proposition 2

Let $\mathcal{X}$ and $\mathcal{Y}$ be saturated Kripke structures. Then
elements $x\in X$ and $y\in Y$ are bisimilar if and only if they are logically
equivalent. In short:
$\sim_{\mathcal{X},\mathcal{Y}}\,\,\,=\,\,\,\approx_{\mathcal{X},\mathcal{Y}}$.

We shall next show that saturation allows us to describe the minimal
homomorphic image of a Kripke structure:

###### Lemma 6

If $\mathcal{X}$ is saturated, then $\approx$ is a congruence relation on
$\mathcal{X}$.

###### Proof

Clearly, $\approx$ is an equivalence relation and therefore it is the kernel
of the map $\pi_{\approx}$ sending arbitrary elements $x$ to $x/_{\approx},$
which denotes the equivalence class of $\approx$ containing $x$. To show that
$\pi_{\approx}$ is a homomorphism, we need to exhibit a coalgebra structure on
$X/_{\approx}$, the factor set of $X$. Put

$x/_{\approx}\,\Vdash\,p\,:\iff\,\exists\,\,x^{\prime}\approx
x\,.\,x^{\prime}\Vdash p.$

$x/_{\approx}\,\rightarrowtriangle\,y/_{\approx}$

$\,:\iff\,$ there exist $x^{\prime}\approx x$ and $y^{\prime}\approx y$ such
that $x^{\prime}\rightarrowtriangle y^{\prime}.$

We check that $\pi_{\approx}:\mathcal{X\to\mathcal{X}}/_{\approx}$ is indeed a
Kripke homomorphism:

  * •

Clearly, $x\Vdash p$ iff $x/_{\approx}\Vdash p$ by definition of $\Vdash$ on
$X/_{\approx}$, and

  * •

if $x\rightarrowtriangle y$, then
$x/_{\approx}\,\rightarrowtriangle\,y/_{\approx}$ is also immediate by
definition. Conversely, given
$\pi_{\approx}(x)=x/_{\approx}\,\rightarrowtriangle\,y/_{\approx}$ for some
$y,$ we must find a $y^{\prime\prime}$ with $x\rightarrowtriangle
y^{\prime\prime}$ and $\pi_{\approx}(y^{\prime\prime})=y/_{\approx}.$ Since
$x/_{\approx}\,\rightarrowtriangle\,y/_{\approx},$ we know that there are
$x^{\prime}\approx x$ and $y^{\prime}\approx y$ with
$x^{\prime}\rightarrowtriangle y^{\prime}$. By assumption, $\approx$ is a
bisimulation, so it follows that there is some $y^{\prime\prime}$ with
$x\rightarrowtriangle y^{\prime\prime}$ and $y^{\prime\prime}\approx
y^{\prime}$. Consequently, $x\rightarrowtriangle y^{\prime\prime}$ and
$\pi_{\approx}(y^{\prime\prime})=\pi_{\approx}(y^{\prime})=y/_{\approx},$ as
required.

---
$\textstyle{x\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\,\,\approx\,\,}$$\scriptstyle{\pi_{\approx}}$$\textstyle{x/_{\approx}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{x^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\pi_{\approx}}$$\textstyle{y^{\prime\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\approx}$$\textstyle{y/_{\approx}}$$\textstyle{y^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\pi_{\approx}}$

Thus, $\pi_{\approx}$ is a homomorphism with kernel $\approx$, which makes the
latter a congruence relation.

###### Definition 6

A Kripke structure is called _simple_ , if it does not have a proper
homomorphic image.

Clearly, if $x\not\approx y$ then there cannot be a homomorphism $\varphi$
with $\varphi(x)=\varphi(y)$, since $x\approx\varphi(x)$ and
$y\approx\varphi(y)$. Thus, if $\approx$ is a congruence,
$\mathcal{X}/_{\approx}$ must be simple. It follows:

###### Theorem 3.1

A Kripke structure is saturated iff it has a simple and saturated homomorphic
image.

Observe that Example 2 is a Kripke structure, which is saturated and simple,
but not image finite. In particular it does not have a homomorphism to an
image finite Kripke structure.

##  4 $F$-coalgebras

Given a category $\mathscr{C}$ and an endofunctor
$F:\mathscr{C}\to\mathscr{C},$ an $F$_-coalgebra_ $\mathcal{A}=(A,\alpha)$ is
an object $A$ from $\mathscr{C}$ together with a morphism $\alpha:A\to F(A).$
The object $A$ is called the _base object_ and $\alpha$ is called the
_structure morphism_ of the $F$-coalgebra $\mathcal{A}=(A,\alpha).$

Given a second coalgebra $\mathcal{B}=(B,\beta)$, a _homomorphism_
$\varphi:\mathcal{A}\to\mathcal{B}$ is a $\mathscr{C}$-morphism $\varphi:A\to
B$ which renders the following diagram commutative:

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\alpha}$$\scriptstyle{\varphi}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\beta}$$\textstyle{F(A)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F(\varphi)}$$\textstyle{F(B)}$

$F$-coalgebras with homomorphisms, as defined above, form a category, which we
shall call $\mathscr{C}_{F}$, or simply $Coalg_{F}$ when the base category is
understood. When $\varphi$ in the above figure is a monomorphism in the base
category, then we call $\mathcal{A}$ a _subcoalgebra_ of $\mathcal{B}$.

Kripke structures are prime examples of coalgebras. Indeed, the successor
relation $R\subseteq X\times X$ can be understood as a map
$R:X\to\mathbb{P}(X)$ and the valuation $v$ as a map $v:X\to\mathbb{P}(\Phi)$,
where $\mathbb{P}$ is the powerset functor and $\Phi$ is the fixed set of
propositional atoms. Thus a Kripke structure $\mathcal{X}=(X,R,v)$ is simply
an $F$-coalgebra for the combined functor
$\mathbb{P}(-)\times\mathbb{P}(\Phi)$, that is a map

$\alpha:X\to\mathbb{P}(X)\times\mathbb{P}(\Phi),$

whose first component models the successor relation $R$ and whose second
component is the valuation $v.$

It is easy to check (see [19]), that a homomorphism of Kripke structures, as
introduced earlier, is the same as a homomorphism of coalgebras when Kripke
structures are understood as $\mathbb{P}(-)\times\mathbb{P}(\Phi)$-coalgebras.

In this case a subcoalgebra $\mathcal{U}$ of $\mathcal{X}$ is uniquely
determined by its base set $U$. To be precise, $U\subseteq X$ carries a
subcoalgebra of the Kripke structure $\mathcal{X}=(X,\alpha)$ if and only if
$R(U)\subseteq U.$

Choosing the finite-powerset functor $\mathbb{P}_{\omega}(-)$ instead of
$\mathbb{P}(-)$, coalgebras for the functor
$\mathbb{P}_{\omega}(-)\times\mathbb{P}(\Phi)$ are precisely the image finite
Kripke structures.

Saturated Kripke structures, however, lying between image finite and arbitrary
Kripke structures, do not seem to allow such a simple modelling by an
appropriate $Set$-functor between $\mathbb{P}_{\omega(-)}$ and
$\mathbb{P}(-).$ Instead, we shall have to pass to the category _Top_ of
topological spaces and continuous mappings and model them as coalgebras over
_Top_.

##  5 Topological models

###### Definition 7

A _topological model_ is a Kripke model $\mathcal{X}=(X,R,v)$ together with a
topology $\tau$ on $X$, such that

  1. 1.

$\forall x\in X.\,R(x)$ is compact

  2. 2.

$\forall O\in\tau.\,\langle R\rangle O\in\tau$

  3. 3.

$\forall O\in\tau.\,[R]O\in\tau$

  4. 4.

$\forall p\in\Phi.\left\llbracket p\right\rrbracket\in\tau$ and
$(X-\left\llbracket p\right\rrbracket)\in\tau.$

A _homomorphism_ $\varphi:\mathcal{X}\to\mathcal{Y}$ between topological
models is simply a Kripke-homomorphism (see def. 4) which additionally is
continuous with respect to the topologies on $\mathcal{X}$ and $\mathcal{Y}$.

We need two simple technical lemmas:

###### Lemma 7

If $C$ is closed, then so are $\langle R\rangle C$ and $[R]C$.

###### Proof

Let $C=X-O$ where $O$ is open, then $\langle R\rangle C=\langle
R\rangle(X-O)=X-[R]O$ and $[R]C=[R](X-O)=X-\langle R\rangle O.$

###### Lemma 8

In every topological model the sets $\left\llbracket\phi\right\rrbracket$
where $\phi\in\mathcal{L}_{\Phi}$, are _clopen_ _(clo_ sed and o _pen)_.

###### Proof

By induction on the construction of $\phi:$

For $p\in\Phi$ the assertion is part of the definition. If the claim is true
for $\phi,\phi_{1}$ and $\phi_{2}$, then it is obviously true for all boolean
compositions, in particular for $\neg\phi$ and for $\phi_{1}\wedge\phi_{2}$.

Lemma 7 and Definition 7 ensure that the claim remains true for $\square\phi$
and $\diamondsuit\phi,$ since
$\left\llbracket\square\phi\right\rrbracket=[R]\left\llbracket\phi\right\rrbracket$
and for $\left\llbracket\diamondsuit\phi\right\rrbracket=\langle
R\rangle\left\llbracket\phi\right\rrbracket.$

Topological models with continuous Kripke-Homomorphisms obviously form a
category which we shall call $\mathscr{K}_{Top}$.

##  6 The compact Vietoris-functor

Leopold Vietoris, in his 1922 paper [21], defined his _domains of second
order_(“Bereiche zweiter Ordnung”) as the collection of closed subsets of a
compact Hausdorff space. Later several generalizations and modifications of
this topology were introduced and studied under the heading of _hypertopolog_
y.

In connection with Kripke structures, Bezhanishvili, Fontaine and Venema [4]
consider the Vietoris functor and Vietoris coalgebras over Stone spaces, i.e.
compact and totally disconnected Hausdorff spaces.

In compact Hausdorff spaces, all closed subsets are compact. Hence, when
extending the Vietoris functor to act on arbitrary topological spaces
$\mathcal{X}=(X,\tau)$, one has the choice to take as base set for
$\mathbb{V}(\mathcal{X})$ all closed subsets or all compact subsets of $X.$ In
[13] the authors show that both choices lead to endofunctors on the category
$Top$ of topological spaces, the _“lower” Vietoris functor_ , and the _compact
Vietoris functor_. Here we shall only need to work with the latter, which for
us then is “the” Vietoris functor:

Given a topological space $\mathcal{X}=(X,\tau)$, the _Vietoris space_
$\mathbb{V}(\mathcal{X})$ takes as base set the collection of all compact
subsets $K\subseteq X$. The _Vietoris topology_ on $\mathbb{V}(\mathcal{X})$
is generated by a subbase consisting of all sets

$\displaystyle\langle O\rangle$
$\displaystyle:=\\{K\in\mathbb{V}(\mathcal{X})\mid K\cap
O\neq\emptyset\\},\text{and}$ $\displaystyle{}[O]$
$\displaystyle:=\\{K\in\mathbb{V}(\mathcal{X})\mid K\subseteq O\\}$

where $O\in\tau$.

If $\mathcal{X}=(X,\tau)$ and $\mathcal{Y}=(Y,\rho)$ are topological spaces,
then the _Vietoris functor_ sends a continuous function
$f:\mathcal{X}\to\mathcal{Y}$ to a map
$(\mathbb{V}f):\mathbb{V}(\mathcal{X})\to\mathbb{V}(\mathcal{Y})$ by setting
$(\mathbb{V}f)(K):=f(K).$ Recall that the image $f(K)$ of a compact set $K$ by
a continuous map $f$ is always compact. It is easy to calculate that
$(\mathbb{V}f)^{-1}(\left\langle O\right\rangle)=\left\langle
f^{-1}(O)\right\rangle$ and $(\mathbb{V}f)^{-1}(\left[O\right])=[f^{-1}(O)],$
hence $(\mathbb{V}f)$ is continuous with respect to the Vietoris topologies.
In fact, $(\mathbb{V}f)^{-1}$ takes the defining subbase of
$\mathbb{V}(\mathcal{Y})$ to the defining subbase of
$\mathbb{V}(\mathcal{X})$. This shows that $\mathbb{V}$ is indeed an
endofunctor on $Top$.

Let now $\mathbb{P}(\Phi)$ be the powerset of $\Phi$, equipped with the
topology having as a base the set of all

$\uparrow p:=\\{u\subseteq\Phi\mid p\in u\\}$

where $p\in\Phi,$ together with their complements $\mathbb{P}(\Phi)\,-\uparrow
p$. This topology, trivially, is Hausdorff, but in general not compact.

###### Definition 8

The product $\mathbb{V}(-)\times\mathbb{P}(\Phi)$ of the Vietoris functor
$\mathbb{V}$ with the constant functor of value $\mathbb{P}(\Phi),$ carrying
the above topology, will be called the $\Phi$-_Vietoris functor, or simply
the_ Vietoris functor _, when $\Phi$ is clear. _

The Vietoris functor is an endofunctor on the category $Top$ of topological
spaces with continuous maps. We can now define:

_Vietoris coalgebras_ are coalgebras over $Top$ for the $\Phi$-Vietoris
functor $\mathbb{V}(-)\times\mathbb{P}(\Phi)$, and the following result shows
that they agree with our topological models:

###### Theorem 6.1

Vietoris coalgebras with coalgebra homomorphisms are the same as topological
models with continuous Kripke-homomorphisms.

###### Proof

Given a topological model $(X,R,v)$ with underlying space
$\mathcal{X}=(X,\tau),$ we can consider it as a Vietoris coalgebra by defining
the structure map
$\alpha:\mathcal{X}\to\mathbb{V}(\mathcal{X})\times\mathbb{P}(\Phi)$ as
$\alpha(x):=(R(x),v(x)).$ To show that $\alpha$ is continuous, we must verify
that both components are continuous.

Continuity of (the map) $R:\mathcal{X}\to\mathbb{V}(\mathcal{X})$ needs to be
tested only on the subbase for the Vietoris topology on
$\mathbb{V}(\mathcal{X})$. Indeed, assume $O\in\tau,$ then

$\displaystyle R^{-1}(\left[O\right])$ $\displaystyle=\\{x\in X\mid
R(x)\in\left[O\right]\\}$ $\displaystyle=\\{x\in X\mid R(x)\subseteq
O\\}=[R]O$

is open in $\tau$ and so is

$\displaystyle R^{-1}(\left\langle O\right\rangle)$ $\displaystyle=\\{x\in
X\mid R(x)\in\left\langle O\right\rangle\\}$ $\displaystyle=\\{x\in X\mid
R(x)\cap O\neq\emptyset\\}=\langle R\rangle O.$

To see that $v$ also is continuous, let $\uparrow
p\,\subseteq\,\mathbb{P}(\Phi)$ be given, then

$v^{-1}(\uparrow p)=\\{x\in X\mid p\in v(x)\\}=\llbracket p\rrbracket\in\tau$

as well as

$v^{-1}(\mathbb{P}(X)-\uparrow p)=\\{x\in X\mid p\notin v(x)\\}=(X-\llbracket
p\rrbracket)\in\tau.$

Conversely, let $(X,\alpha)$ be a Vietoris coalgebra, with
$\mathcal{X}=(X,\tau)$ as base space and
$\alpha:\mathcal{X}\to\mathbb{V}(\mathcal{X})\times\mathbb{P}(\Phi)$ as
structure morphism, then $\alpha=(R,v)$ with
$R:=\pi_{1}\circ\alpha:\mathcal{X}\to\mathbb{V}(\mathcal{X})$ and
$v:=\pi_{2}\circ\alpha:\mathcal{X}\to\mathbb{P}(\Phi)$, both of which are
continuous. Since $R(x)\in\mathbb{V}(\mathcal{X})$, it is necessarily compact.
If $O$ is open in $(X,\tau)$ then $\left[O\right]$ is open in
$\mathbb{V}(\mathcal{X}),$ hence $R^{-1}([O])$ must be open in $(X,\tau)$,
hence so is

$[R]O=\\{x\in X\mid R(x)\subseteq O\\}=\\{x\in X\mid
R(x)\in[O]\\}=R^{-1}([O]).$

Similarly, for $O$ open in $(X,\tau)$ we have $\left\langle O\right\rangle$
open in $\mathbb{V}(\mathcal{X}),$ hence $R^{-1}(\left\langle O\right\rangle)$
is open in $\mathcal{X},$ which means that

$\langle R\rangle O=\\{x\in X\mid R(x)\cap O\neq\emptyset\\}=\\{x\in X\mid
R(x)\in\left\langle O\right\rangle\\}=R^{-1}(\left\langle O\right\rangle)$

is open as well.

Finally, for $p\in\Phi$ we have $\uparrow p=\\{u\subseteq\Phi\mid p\in u\\}$
clopen in the topology on $\mathbb{P}(\Phi)$, so also $\left\llbracket
p\right\rrbracket=\\{x\in X\mid p\in v(x)\\}=v^{-1}(\\{u\subseteq\Phi\mid p\in
u\\})=v^{-1}(\uparrow p)$ as well as its complement $X-\left\llbracket
p\right\rrbracket$ are open in $\tau$.

Coalgebra homomorphisms between Vietoris coalgebras, as coalgebras over $Top$,
must be continuous and preserve both $R$ and $v$ which means they are the same
as continuous Kripke homomorphisms between the corresponding topological
models.

##  7 Characterization theorem

The following theorem shows that saturated Kripke structures arise precisely
as the algebraic reducts of Vietoris coalgebras when forgetting the topology.
Bezhanishvili, Fontaine and Venema [4], studying Vietoris coalgebras over
Stone spaces, show that in this case the underlying Kripke structures are
saturated. In contrast to their work, we consider the Vietoris functor over
arbitrary topological spaces, which allows us to obtain an equivalence:

###### Theorem 7.1

For a Kripke structure $\mathcal{X}$ the following are equivalent:

  1. 1.

$\mathcal{X}$ is saturated,

  2. 2.

$\mathcal{X}$ is the algebraic reduct of a topological model,

  3. 3.

$\mathcal{X}$ is the algebraic reduct of a Vietoris coalgebra.

###### Proof

“$(1)\to(2)"$: Assuming that $\mathcal{X}=(X,R,v)$ is saturated, let $\tau$ be
the topology on $X$ generated by the sets
$\left\llbracket\phi\right\rrbracket$ for $\phi\in\mathcal{L}_{\Phi}$. It
follows that each $\left\llbracket\phi\right\rrbracket$ is clopen (_clo_ sed
and _open_), so each open set can be written as $O=\bigcup_{i\in
I}\left\llbracket\phi_{i}\right\rrbracket$ and each closed set as
$C=\bigcap_{i\in I}\left\llbracket\phi_{i}\right\rrbracket$.

To show that $\mathcal{X}$ with this topology $\tau$ is a topological model,
we show first, that $R(x)$ is topologically compact. For that, assume
$R(x)\subseteq\bigcup_{i\in I}O_{i}$, then $R(x)\subseteq\bigcup_{i\in
I}\bigcup_{j\in J_{i}}\left\llbracket\phi_{j}\right\rrbracket$, i.e.

$x\Vdash\square\bigvee_{i\in I}\bigvee_{j\in J_{i}}\phi_{j}.$

By saturation of $\mathcal{X}$, there are finitely many $j_{i_{1}}\in
J_{i_{1}},...,j_{i_{n}}\in J_{i_{n}}$ with

$x\Vdash\square(\phi_{j_{i_{1}}}\vee...\vee\phi_{j_{i_{n}}}),$

so $R(x)\subseteq O_{i_{1}}\cup...\cup O_{i_{n}}.$

Next, to see that $\langle R\rangle O$ is open, we calculate

$\displaystyle\langle R\rangle O$ $\displaystyle=$ $\displaystyle\langle
R\rangle(\bigcup_{i\in I}\left\llbracket\phi_{i}\right\rrbracket)$
$\displaystyle=$ $\displaystyle\bigcup_{i\in I}\langle
R\rangle\left\llbracket\phi_{i}\right\rrbracket$ $\displaystyle=$
$\displaystyle\bigcup_{i\in I}\\{x\in X\mid
x\models\diamondsuit\phi_{i}\\}\phantom{{\text{\,for some very finite
}I_{0}\subseteq I}}$ $\displaystyle=$ $\displaystyle\bigcup_{i\in
I}\left\llbracket\diamondsuit\phi_{i}\right\rrbracket,$

which is open, and similarly

$\displaystyle[R]O$ $\displaystyle=$ $\displaystyle[R](\bigcup_{i\in
I}\left\llbracket\phi_{i}\right\rrbracket)$ $\displaystyle=$
$\displaystyle\\{x\in X\mid R(x)\subseteq\bigcup_{i\in
I}\left\llbracket\phi_{i}\right\rrbracket\\}$ $\displaystyle=$
$\displaystyle\\{x\in X\mid R(x)\subseteq\bigcup_{i\in
J_{x}}\left\llbracket\phi_{i}\right\rrbracket\text{\,for some finite
}J_{x}\subseteq I\\}$ $\displaystyle=$ $\displaystyle\\{x\in X\mid
x\models\square\bigvee_{i\in J_{x}}\phi_{i}\,\text{for some
finite}J_{x}\subseteq I\,\\}$ $\displaystyle=$
$\displaystyle\bigcup_{J\subseteq
I,\,J\text{\,finite}}\left\llbracket\square\bigvee_{i\in
J}\phi_{i}\right\rrbracket,$

which is open as well.

“$(2)\leftrightarrow(3)"$ is Theorem 6.1.

“$(2)\to(1)"$ : Given a Kripke model $\mathcal{X}$ which is the algebraic
reduct of a topological model, assume $x\Vdash\square\bigvee_{i\in
I}\phi_{i}$, then $R(x)\subseteq\bigcup_{i\in
I}\left\llbracket\phi_{i}\right\rrbracket$. By Lemma 8, the right hand side is
a union of open sets, thus by compactness of $R(x)$ there is a finite subset
$I_{0}\subseteq I$ with $R(x)\subseteq\bigcup_{i\in I_{0}}\phi_{i}$, which
means $x\Vdash\square\bigvee_{i\in I_{0}}\phi_{i}$.

Given a saturated Kripke-structure $\mathcal{X}=(X,R,v)$, let $F(\mathcal{X})$
denote the Vietoris coalgebra, as constructed above, and conversely, given a
Vietoris coalgebra $\mathcal{A}$, let $G(\mathcal{A})$ be the corresponding
saturated Kripke structure. On objects, $F$ and $G$ are clearly inverses to
each other.

On morphisms, this is true as well, since a homomorphism
$\varphi:\mathcal{X}\to\text{$\mathcal{Y}$}$ between saturated Kripke
structures preserves (and reflects) modal formulae (see Lemma 2) and the
topologies on $F(\mathcal{X})$ and $F(\mathcal{Y})$ are generated by validity
sets of formulae. Conversely, a morphism between Vietoris coalgebras
$\mathcal{A}$ and $\mathcal{B}$ is automatically a Kripke-homomorphism by
forgetting continuity.

###### Corollary 3

Saturated Kripke structures, topological models, and Vietoris coalgebras are
isomorphic as categories.

##  8 Closure of Vietoris structures

In those topological spaces where each point has a countable base for its
neighbourhoods, such as, for instance, in metric spaces, continuity can be
conveniently dealt with in terms of convergent sequences
$(x_{n})_{n\in\mathbb{N}}.$ For general spaces $\mathcal{X}=(X,\tau)$, this
intuitive approach is not sufficient, but its spirit and its power can be
salvaged if one allows the linearly ordered set $\mathbb{N}$, indexing a
sequence, to be replaced by arbitrary directed sets $I$ indexing the elements
$(x_{i})_{i\in I}$ of a net. Often, a proof based on convergence of sequences
can be easily generalized by replacing sequences with nets. Therefore net
convergence can be considered more intuitive than the equally powerful notion
of filter convergence. The following definitions and results on nets in
general topological spaces will be needed. They can be found as a series of
exercises in Munkres [18].

###  8.1 Nets and subnets

A partially ordered set $(I,\leq)$ is called _directed_ , if for each pair
$i_{1},i_{2}\in I$ there is some $i\in I$ such that $i_{1}\leq i$ and
$i_{2}\leq i,$ i.e. $i$ is an upper bound for $\\{i_{1},i_{2}\\}.$ It follows
that each finite subset $I_{0}\subseteq I$ has a common upper bound.

###### Definition 9

A subset $J\subseteq I$ is called _cofinal_ in $I$, if for each $i\in I$ there
is some $j\in J$ with $i\leq j.$ A map $f:J\to I$ between ordered sets
$(J,\leq)$ and $(I,\leq)$ is called _cofinal_ if its image $f[J]$ is cofinal
in $I.$

Clearly, if $J_{1}$ is cofinal in $J_{2}$ and $J_{2}$ cofinal in $I$ then
$J_{1}$ is cofinal in $I$. Also, compositions of cofinal maps are cofinal.

Let $\mathcal{X}=(X,\tau)$ be a topological space and $x\in X$. By
$\mathfrak{U}(x)$ we denote the collection of all open neighborhoods of $x.$
Observe that $\mathfrak{U}(x)$, when ordered by reverse inclusion, is a
directed set.

###### Definition 10

A _net_ in $X$ is a map $\sigma:I\to X$ from a directed set $I$ to the set
$X.$

If $\sigma(i)=x_{i}$, then one often denotes the net $\sigma$ as
$(x_{i})_{i\in I}$ and if $I$ is clear from the context one simply writes
$(x_{i}).$

The net $(x_{i})_{i\in I}$ _converges_ to $x\in X$ and we shall write
$\textstyle{(x_{i})_{i\in
I}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{x,}$ or
when $I$ is understood, simply
$\textstyle{(x_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{x),}$
provided that

$\forall U\in\mathfrak{U}(x).\,\exists i_{U}\in I.\,\forall i\geq
i_{U}.\,x_{i}\in U.$ (8.1)

In this case, $x$ is called a _limit point_ of $(x_{i})_{i\in I}.$
Colloquially, condition 8.1 can be expressed as “$(x_{i})$_is eventually in
every neighborhood of_ $x".$

Limit points need not exist, nor need they be unique, unless $X$ is Hausdorff.
In any case though, one has (see [18]):

###### Proposition 3

Let $\mathcal{X}$ and $\mathcal{Y}$ be arbitrary topological spaces.

  1. 1.

A map $\varphi:\mathcal{X}\to\mathcal{Y}$ is continuous at $x$ if and only if
it “preserves convergence”, i.e. for all nets $(x_{i})_{i\in I}$ in $X:$

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
8.76672pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{(x_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
32.76672pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
32.76672pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{x)}$}}}}}}}\ignorespaces}}}}\ignorespaces\implies\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
15.92645pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{(\varphi(x_{i})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
39.92645pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
39.92645pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\varphi(x))}$}}}}}}}\ignorespaces}}}}\ignorespaces.$

  2. 2.

Given a subset $A\subseteq X$, then $x\in X$ belongs to the topological
closure $\overline{A}$ of $A$ if and only if some net $(a_{i})$ in $A$
converges to $x.$ Thus, $A$ is closed iff it contains all limit points of nets
in $A.$

$x\in X$ is called an _accumulation point of the net $(x_{i})_{i\in I}$ _if __

$\forall U\in\mathfrak{U}(x).\,\forall i\in I.\,\exists j\geq i.\,x_{j}\in U.$
(8.2)

Condition (8.2) can be phrased as: “$x_{i}$ _is frequently in every
neighborhood of_ $x".$ A characterization of compactness using nets is ([18]):

###### Lemma 9

_A subset $A\subseteq X$ is compact if and only if every net in $A$ has an
accumulation point in $A$._

###### Definition 11

A net $\lambda:J\to X$ is a _subnet_ of $\sigma:I\to X$ if there is a
monotonic and cofinal map $f:J\to I$ with $\lambda=\sigma\circ f$:

---
$\textstyle{I\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma}$$\textstyle{X}$$\textstyle{J\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\scriptstyle{\lambda}$

Thus, if $\sigma=(x_{i})_{i\in I}$ then $\lambda=(x_{f(j)})_{j\in J}.$ One
easily checks that the subnet relation is reflexive and transitive, but
mainly:

###### Lemma 10

If ($x_{i})_{i\in I}$ converges to $x$ then so does each subnet
$(x_{f(j)})_{j\in J}$.

###### Lemma 11

$x\in X$_is an accumulation point of the net_ $\sigma:I\to X$ _if and only if
there is a subnet_ $\lambda$ _of_ $\sigma$ _converging to $x.$_

###### Corollary 4

_A subset $A\subseteq X$ is compact iff every net in $A$ has a subnet
converging to some $a\in A.$_

###  8.2 Convergence in Vietoris spaces

In this section, we prepare our main result on net convergence in Vietoris
spaces. Let $\mathcal{X}=(X,\tau)$ be a topological space. Recall that the
_Vietoris space_ $\mathbb{V}(\mathcal{X})$ over $\mathcal{X}$ consists of all
compact subsets $K\subseteq X$, with a topology generated by a subbase
consisting of all sets

$\displaystyle\langle O\rangle$ $\displaystyle:=$
$\displaystyle\\{K\in\mathbb{V}(\mathcal{X})\mid K\cap O\neq\emptyset\\}$
$\displaystyle{}[O]$ $\displaystyle:=$
$\displaystyle\\{K\in\mathbb{V}(\mathcal{X})\mid K\subseteq O]$

where $O$ ranges over all open subsets of $\mathcal{X}.$ The following results
establish the relevant connections between convergence in
$\mathbb{V}(\mathcal{X})$ and convergence in $\mathcal{X}=(X,\tau)$.

###### Lemma 12

Let $\kappa:I\to\mathbb{V}(\mathcal{X})$ be a net in the Vietoris space. If
$(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.84543pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\kappa_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
30.84543pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
30.84543pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{K}$}}}}}}}\ignorespaces}}}}\ignorespaces)$
and $K\neq\emptyset$, then $\kappa$ has a subnet, each member of which is
nonempty.

###### Proof

Since $K\neq\emptyset$, we have $K\in\langle X\rangle$, so $\langle X\rangle$
is a neighborhood of $K$ in $\mathbb{V}(\mathcal{X})$. As $\kappa$ converges
to $K$, there must be some $i_{0}\in I$ such that $\forall i\geq
i_{0}.\,\kappa_{i}\in\langle X\rangle,$ i.e $\forall i\geq
i_{0}.\,\kappa_{i}\neq\emptyset.$ Put $J=(\\{i\in I\mid i\geq i_{0}\\},\leq)$
and let $f:J\hookrightarrow I$ be the natural inclusion, then $f$ is clearly
monotonic and cofinal. Therefore $\tau:=\kappa\circ f$ is a subnet of $\kappa$
and $\tau_{j}=\kappa_{f(j)}=\kappa_{j}\neq\emptyset,$ owing to $j\in J.$

###### Lemma 13

Given a net $\kappa:I\to\mathbb{V}(\mathcal{X})$ converging to
$K\in\mathbb{V}(\mathcal{X})$ and $b_{i}\in\kappa_{i}$ for each $i\in I$. Then
the net $(b_{i})_{i\in I}$ has a subnet converging to some $b\in K$.

###### Proof

It is enough to show that $(b_{i})_{i\in I}$ has an accumulation point $b\in
K.$ For then we obtain a subnet $(b_{f(j)})_{j\in J}$ converging to $b$. By
Lemma 10, the subnet $(\kappa_{f(j)})_{j\in J}$ of $\kappa$ still converges to
$K.$

For every $x\in K$ which is not an accumulation point of $(b_{i})_{i\in I}$,
we obtain by negating (8.2) an open neighborhood $U_{x}$ of $x$ and an
$i_{x}\in I$ such that for all $i\geq i_{x}$ we have $b_{i}\not\in U_{x}.$
Assuming that no $x\in K$ is an accumulation point, then the family
$(U_{x})_{x\in K}$ forms an open cover of $K.$ By compactness, there is a
finite subcover $U=U_{x_{1}}\cup...\cup U_{x_{n}}$. Choose $i_{U}\geq
i_{x_{1}},...,i_{x_{n}}$, then for every $i\geq i_{U}$ we have $b_{i}\not\in
U\supseteq K.$

But $[U]$ is also an open neighborhood of $K$ in $\mathbb{V}(\mathcal{X})$ and
$\textstyle{(\kappa_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{K),}$
so there exists $i_{[U]}$ with $\kappa_{i}\in[U]$, that is
$b_{i}\in\kappa_{i}\subseteq U$ for $i\geq i_{[U]}$. For
$i\geq\\{i_{U},i_{[U]}\\}$ we enter the contradiction $b_{i}\in U$ and
$b_{i}\not\in U$.

###### Lemma 14

Given a net $\kappa:I\to\mathbb{V}(\mathcal{X})$ converging to
$K\in\mathbb{V}(\mathcal{X})$ and $a\in K$. Then there is a subnet
$(\kappa_{j})_{j\in J}$ and elements $a_{j}\in\kappa_{j}$ converging to $a.$

###### Proof

By Lemma 12 and Lemma 10, we may assume that $\kappa_{i}\neq\emptyset$ for all
$i\in\mathcal{I}.$

For every $U\in\mathfrak{U}(a)$ we have $a\in U\cap K$, so $K\cap
U\neq\emptyset,$ which means that $K\in\langle U\rangle,$ so $\langle
U\rangle$ is an open neighborhood of $K$ in $\mathbb{V}(\mathcal{X}).$

Since $\kappa$ converges to $K$ we have

$\forall U\in\mathfrak{U}(a).\exists i_{U}\in I.\forall i\geq
i_{U}.\kappa_{i}\in\langle U\rangle.$ (8.3)

Consider a partial order on

$J:=\\{(i,U)\in I\mathcal{\times\mathfrak{U}}(a)\mid\kappa_{i}\in\langle
U\rangle\\}$

by defining:

$(i_{1},U_{1})\leq(i_{2},U_{2})\,:\iff i_{1}\leq i_{2}\,\wedge\,U_{1}\supseteq
U_{2}.$

To verify that $\mathcal{J}=(J,\leq)$ is directed, let arbitrary
$j_{1}=(i_{1},U_{1})$ and $j_{2}=(i_{2},U_{2})$ be given. Pick $U=U_{1}\cap
U_{2}$ then by (8.3) there is an $i_{U}\in I$ with $\kappa_{i}\in\langle
U\rangle$ for all $i\geq i_{U}.$ It suffices to choose $i\geq
i_{1},i_{2},i_{U},$ then $(i,U)\in J$ and
$(i,U)\geq(i_{1},U_{1}),(i_{2},U_{2})$.

The map $\pi_{1}:J\to I$ given as $\pi_{1}(i,U):=i$ is clearly monotonic. For
each $i\in I$ we have $(i,X)\in J$ since $\kappa_{i}\neq\emptyset.$ Hence
$\pi_{1}$ is cofinal. Therefore
$\kappa\circ\pi_{1}:J\to\mathbb{V}(\mathcal{X})$ is a subnet of $\kappa$ and
therefore also converges to $K$.

For each $(i,U)\in J$ we can pick some $a_{(i,U)}\in\kappa_{i}\cap U$. This
defines a net $(a_{j})_{j\in J}$ in $X$.

To show that $(a_{j})_{j\in J}$ converges to $a,$ let $U$ be any open
neighborhood of $a.$ By 8.3 there exist some $i_{U}$ such that in particular
$j_{U}:=(i_{U},U)\in J.$ We therefore have $a_{j_{U}}:=a_{(i_{U},U)}\in U$ and
for each $j=(i,U^{\prime})\geq(i_{U},U)=j_{U},$ i.e. for $i\geq i_{U}$ and
$U^{\prime}\subseteq U$ we have $a_{j}=a_{(i,U^{\prime})}\in\kappa_{i}\cap
U^{\prime}\subseteq U.$

We can combine the previous two lemmas to a theorem relating convergence in
Vietoris spaces to convergence in their base spaces:

###### Theorem 8.1

Let $(\kappa_{i})_{i\in I}$ converge to $K$ in the Vietoris space
$\mathbb{V}(\mathcal{X}).$ Then

  1. 1.

for each $a\in K$ there is a subnet $(\kappa_{j})_{j\in J}$ and elements
$a_{j}\in\kappa_{j}$ such that
$\textstyle{(a_{j}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{a),}$
and

  2. 2.

each net $(b_{i})_{i\in I}$ with $b_{i}\in\kappa_{i}$ has a subnet
$(b_{j})_{j\in J}$ converging to some $b\in K.$

###  8.3 Closure of subcoalgebras and bisimulations

In this section we shall show that in topological Kripke structures, i.e. for
Vietoris coalgebras, the topological closure of a substructure is again a
substructure and the closure of a bisimulation is a bisimulation. The second
of these results has previously been shown for Vietoris coalgebras over Stone
spaces in [4], but now we work in the more general context of Vietoris
coalgebras over arbitrary topological spaces, so we were forced to prepare our
tools in the previous sections.

###### Theorem 8.2

Let $\mathcal{A}=(A,\alpha)$ be a Vietoris coalgebra. If $U\subseteq A$ is a
Kripke substructure of $\mathcal{A}$, then so is its topological closure
$\overline{U}$.

###### Proof

We may consider $\mathcal{A}$ as a topological model $(A,R,v_{A})$ where
$R(a)=(\pi_{1}\circ\alpha)(a)$ for each $a\in A$ is the compact set of all
successors of $a.$ Assume that $U$ is a subcoalgebra, i.e. a subset
$U\subseteq X$ such that $R(u)\subseteq U$ for each $u\in U.$ We need to show
that the same property holds for $\overline{U}.$

Thus let $u\in\overline{U}$ be arbitrary and let $v$ be a successor of $u$ in
the coalgebra $\mathcal{X}$, i.e. $v\in R(u)$. We need to show that
$v\in\overline{U}.$

Due to Proposition 3, there is a net $(u_{i})_{i\in I}$ converging to $u$ with
each $u_{i}\in U.$ By continuity of $\alpha,$ the net $R(u_{i})_{i\in I}$
converges to $R(u)$ in the Vietoris topology.

As $v\in R(u)$, we may assume by Lemma 12, that each $R(u_{i})$ is nonempty.
222With the phrase “we may assume” we often hide the technicality that we
might have to pass to a subnet, such as here to $(\alpha(u_{f(j)}))_{j\in J}$
and retroactively replace $(u_{i})_{i\in I}$ by the subnet $(u_{f(j)})_{j\in
J}$, which is always justified by Lemma 10. Next, we may assume by Theorem 8.1
that we can pick a $v_{i}$ from each $R(u_{i})$ so that the net $(v_{i})_{i\in
I}$ converges to $v$ in $\mathcal{X}.$

Since $U$ was a subcoalgebra, $R(u_{i})\subseteq U,$ so each $v_{i}$ must
belong to $U$. Therefore, we have found a net in $U$ which converges to $v,$
hence $v\in\overline{U}.$

###### Theorem 8.3

If $S$ is a Kripke bisimulation between Vietoris coalgebras
$\mathcal{A}=(A,\alpha)$ and $\mathcal{B}=(B,\beta)$, then so is its
topological closure $\overline{S}.$

###### Proof

Again, we consider $\mathcal{A}$ and $\mathcal{B}$ as topological models with
$\alpha=(R_{A},v_{A})$ and $\beta=(R_{B},v_{B})$. Given
$(a,b)\in\overline{S},$ we need to show that

  1. 1.

$v_{A}(a)=v_{B}(b)$ and

  2. 2.

whenever $a\rightarrowtriangle u$ then there is some $v$ with
$b\rightarrowtriangle v$ and $(u,v)\in\overline{S}.$

The third case of definition 3 will follow by a symmetric proof.

First note that by Theorem 3 there is a net $(a_{i},b_{i})_{i\in I}$
converging to $(a,b)$ with each $(a_{i},b_{i})\in S.$ The individual nets
$(a_{i})$, resp. $(b_{i})$, converge to $a,$ resp. to $b$, since the
projection maps are continuous.

Also by continuity, $v_{A}(a_{i})$ and $v_{B}(b_{i})$ converge to $v_{A}(a)$
and $v_{B}(b)\in\mathbb{P}(\Phi)$. Since $(a_{i},b_{i})\in S,$ we know
$v_{A}(a_{i})=v_{B}(b_{i})$ for each $i\in I.$ Since the topology on
$\mathbb{P}(\Phi)$, the second component of the Vietoris functor, is
Hausdorff, we get $v_{A}(a)=v_{B}(b)$ as required.

Next, assume $a\rightarrowtriangle u$, i.e. $u\in R_{A}(a),$ then we need to
find some $v$ with $b\rightarrowtriangle v$ and $(u,v)\in\overline{S}.$

By continuity of $R_{A}$ and $R_{B}$, the nets $(R_{A}(a_{i}))_{i\in I}$ resp.
$(R_{B}(b_{i})_{i\in I}),$ converge to $R_{A}(a),$ resp. to $R_{B}(b)$ in the
Vietoris spaces $\mathbb{V}(\mathcal{A})$, resp. $\mathbb{V}(\mathcal{B})$.

$\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R_{A}}$$\scriptstyle{\overline{S}}$
$\textstyle{a_{j}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{lim_{\mathcal{A}}}$$\scriptstyle{R_{A}}$$\scriptstyle{S}$$\textstyle{b_{j}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{lim_{\mathcal{B}}}$$\scriptstyle{R_{B}}$
$\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R_{B}}$$\textstyle{R_{A}(a)}$
$\textstyle{R_{A}(a_{j})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{lim_{\mathbb{V}(\mathcal{A})}}$$\textstyle{R_{B}(b_{j})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{lim_{\mathbb{V}(\mathcal{B})}}$
$\textstyle{R_{B}(b)}$$\textstyle{u\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\in}$$\scriptstyle{\overline{S}}$$\textstyle{\exists\,u_{j}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{lim_{\mathcal{A}}}$$\scriptstyle{\in}$$\scriptstyle{S}$$\textstyle{v_{j}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\in}$$\scriptstyle{lim_{\mathcal{B}}}$$\textstyle{\exists\,v\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\in}$

In the sense mentioned previously, we may assume that the $R_{A}(a_{i})$ are
nonempty and further, using Theorem 8.1, and possibly passing to a subnet
indexed by some $J$, we find $u_{j}\in R_{A}(a_{j})$ with
$\textstyle{(u_{j}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{u).}$

Since $S$ is a bisimulation and $a_{j}\,S\,b_{j}$ for each $j$ and $u_{j}\in
R_{A}(a_{j})$ it follows that there are $v_{j}\in R_{B}(b_{j})$ with
$(u_{j},v_{j})\in S$ for each $j\in J.$ Since
$\textstyle{(b_{j}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{b)}$
it follows
$\textstyle{(R_{B}(b_{j})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{R_{B}(b))}$
by continuity of $R_{B}$. Therefore, Lemma 13 forces $(v_{j})_{j\in J}$ to
converge to some $v\in R_{B}(b).$

Consequently,
$\textstyle{((u_{j},v_{j})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{(u,v))}$
where $(u_{j},v_{j})\in S$ for each $j\in J,$ hence by Lemma 3
$(u,v)\in\overline{S}$ as desired.

##  9 The terminal Vietoris coalgebra

To obtain the terminal Vietoris coalgebra, we utilize the equivalence with
saturated Kripke structures and look for a terminal saturated Kripke structure
instead. This will be found in the “canonical model”.

Recall from [5], that the _canonical model_ for a normal modal logic consists
of all _maximally consistent_ subsets of $\mathcal{L}_{\Phi}$. Here
$u\subseteq\mathcal{L}_{\Phi}$ is called maximally consistent, if

  * •

no contradiction can be derived from the formulae in $u,$ and

  * •

for each formula $\phi\in\mathcal{L}_{\Phi}$, either $\phi\in u$ or
$\neg\phi\in u.$

Typical sets of formulas which are maximally consistent arise as

$\llbracket x\rrbracket:=\\{\phi\mid x\Vdash\phi\\},$

where $x$ is any element of any Kripke structure. Moreover, any consistent set
of formulas can be extended to a maximally consistent set.

It is also essential to know that a set $u$ is consistent, if and only if
every finite subset $u_{0}\subseteq u$ is consistent, see [5].

The _canonical model_ is now defined as
$\mathcal{M}:=(M,\rightarrowtriangle_{\mathcal{M}},v_{\mathcal{M}})$ where $M$
is the collection of all maximally consistent subsets of $\mathcal{L}_{\Phi}$,
and $\rightarrowtriangle_{\mathcal{M}}$ and $v_{\mathcal{M}}$ are defined as

$u\rightarrowtriangle_{\mathcal{M}}v\,:\Leftrightarrow\,\forall\phi.(\square\phi\in
u\implies\phi\in v),$ (9.1)

and

$v_{\mathcal{M}}(u)\,:=\,u\cap\Phi.$ (9.2)

The latter definition extends to the important “truth lemma”:

###### Lemma 15

For each formula $\phi\in\mathcal{L}_{\Phi}$ and each $u\in M$ we have:

$u\Vdash\phi\iff\phi\in u.$

As an immediate corollary, we note:

###### Corollary 5

$\forall u,v\in M.\,u\approx v\implies u=v$.

First, we shall verify, that $\mathcal{M}$ is saturated: Given $u\in M$ and
$\Sigma$ a set of formulas such that for every finite subset
$\Sigma_{0}\subseteq\Sigma$ there is some $v_{0}$ such that
$u\rightarrowtriangle v_{0}$ and $v_{0}\Vdash\bigwedge\Sigma_{0}$. It follows
that every finite subset of the set

$S\,:=\,\\{\phi\mid\square\phi\in u\\}\,\cup\,\Sigma$

is satisfied in some $v_{0}$, and hence consistent. Hence the whole set $S$
itself is consistent. Let $v$ be any maximal consistent set containing $S$,
then $v\in M$ and clearly $u\rightarrowtriangle v$ as well as $v\Vdash\sigma$
for each $\sigma\in\Sigma.$ Therefore:

###### Lemma 16

$\mathcal{M}$ is saturated.

Let us see that moreover:

###### Theorem 9.1

$\mathcal{M}$ is the terminal object in the category of all saturated Kripke
structures.

###### Proof

First note that Corollary 5 yields uniqueness: If for any Kripke structure
$\mathcal{X}=(X,R,v)$ we had different homomorphisms
$\varphi_{1},\varphi_{2}:\mathcal{X}\to\mathcal{M}$, then for some $x\in X$ we
would have $\varphi_{1}(x)\neq\varphi_{2}(x)$. However,
$x\approx\varphi_{1}(x)$ as well as $x\approx\varphi_{2}(x)$ according to 3.1,
whence $\varphi_{1}(x)\approx\varphi_{2}(x)$, which contradicts Corollary 5.

For any Kripke structure $\mathcal{X}=(X,R,v)$ we show that the map
$\left\llbracket-\right\rrbracket:X\to M$ which sends an element $x\in X$ to
$\left\llbracket x\right\rrbracket:=\\{\phi\mid x\Vdash\phi\\}$ is a
homomorphism, see definition 4:

First, for each $p\in\Phi$ we have: $x\Vdash p$ in $\mathcal{X}$ implies
$p\in\llbracket x\rrbracket$, so $\llbracket x\rrbracket\Vdash p$ in
$\mathcal{M}$, by the _Truth Lemma_.

Next, suppose $x,y\in\mathcal{X}$ and $x\rightarrowtriangle_{\mathcal{X}}y$.
Then for each $\phi\in\mathcal{L}_{\Phi}$ with $x\Vdash\square\phi$ it follows
$y\Vdash\phi$, which by the truth lemma says $\square\phi\in\llbracket
x\rrbracket\implies\phi\in\llbracket y\rrbracket$, hence $\llbracket
x\rrbracket\rightarrowtriangle_{\mathcal{M}}\llbracket y\rrbracket$ by 9.1.

Finally, let us assume $\llbracket
x\rrbracket\rightarrowtriangle_{\mathcal{M}}v$ for some maximally consistent
set $v.$ We need to find some $y\in\mathcal{X}$ with
$x\rightarrowtriangle_{\mathcal{X}}y$ and $\llbracket y\rrbracket=v.$

$\textstyle{x\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\llbracket
x\rrbracket\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{y_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Vdash}$$\textstyle{\phi_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\notin}$$\textstyle{v}$

For this we invoke a Hennessy–Milner style argument again: Let $(y_{i})_{i\in
I}$ be the collection of all successors of $x.$ If $\llbracket
y_{i}\rrbracket=v$ for some $i$, then we are done. Otherwise, assume that
$\llbracket y_{i}\rrbracket\neq v$ for each $i\in I,$ then there are formulae
$\phi_{i}$ with $\phi_{i}\in\llbracket y_{i}\rrbracket$ but $\phi_{i}\notin
v$, or, in other words, $y_{i}\Vdash\phi_{i}$, but $v\not\Vdash\phi_{i}$.

Hence $x\models\square\bigvee_{i\in I}\phi_{i}$. By assumption $\mathcal{X}$
is saturated, so $x\in X$ is saturated, which means that we can find a finite
subset $I_{0}\subseteq I$ with $x\Vdash\square\bigvee_{i\in I_{0}}\phi_{i}$.
This is now an honest formula, so from $\llbracket
x\rrbracket\rightarrowtriangle v$, and definition 9.1 we conclude
$v\models\bigvee_{i\in I_{0}}\phi_{i}$. This means that $v\Vdash\phi_{i}$ for
some $i\in I_{0}$, contradicting our assumption.

Theorem 7.1 tells us explicitly, how to obtain the terminal Vietoris
coalgebra, so we have:

###### Theorem 9.2

The category of all Vietoris coalgebras has a terminal object. Its base
structure is the canonical model, consisting of all maximally consistent sets
of $\mathcal{L}_{\Phi}$-formulas, and its topology is generated by the open
sets $\\{u\in\mathcal{M}\mid\phi\in u\\}$ for all $\phi\in\mathcal{L}_{\Phi}.$

##  10 Conclusion

Starting from an arbitrary set $\Phi$ of atomic proposition, we have
characterized modally saturated Kripke structures as _Top_ -coalgebras for
$\mathbb{V}(-)\times\mathbb{P}(\Phi)$, which is the compact Vietoris functor
on the category Top of topological spaces and continuous mappings, augmented
with a constant part, representing sets of atomic propositions.

In fact, the categories of saturated Kripke structures and the category of all
Vietoris coalgebras over the category $Top$ are isomorphic. We have described
the relation of convergence in the Vietoris space $\mathbb{V}(\mathcal{X})$ to
convergence in the base space $\mathcal{X},$ from which it was easy to derive
that the Kripke-closure of bisimulations and of subcoalgebras are again
bisimulations, resp. subcoalgebras. Finally, we have shown that the final
Vietoris coalgebra exists, and is derived from the canonical Kripke model.

## References

  * [1] Adriana Balan and Alexander Kurz.  Finitary functors: From set to preord and poset.  In Andrea Corradini, Bartek Klin, and Corina Cîrstea, editors, Algebra and Coalgebra in Computer Science, pages 85–99, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg.
  * [2] M. Barr.  Terminal coalgebras in well-founded set theory.  Theoretical Computer Science, (114(2)):299–315, 1993.
  * [3] M. Barr.  Additions and corrections to ‘Terminal coalgebras in well-founded set theory’.  Theoretical Computer Science, (124(1)):189–192, 1994.
  * [4] N. Bezhanishvili, G. Fontaine, and Y. Venema.  Vietoris bisimulations.  Journal of Logic and Computation, 20(5), 2010.
  * [5] Patrick Blackburn, Maarten de Rijke, and Yde Venema.  Modal Logic.  Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001.
  * [6] Ernst-Erich Doberkat.  Stochastic Coalgebraic Logic.  Monographs in Theoretical Computer Science. Springer Berlin Heidelberg, 2009.
  * [7] K. Fine.  Some connections between elementary and modal logic.  In Patrick Blackburn, Johan Van Benthem, and Frank Wolter, editors, Proceedings of the Third Scandinavian Logic Symposium, volume 3, pages 15–31. North-Holland, 1973.
  * [8] Valentin Goranko and Martin Otto.  Model theory of modal logic.  In Patrick Blackburn, Johan Van Benthem, and Frank Wolter, editors, Handbook of Modal Logic, volume 3, pages 249–329. Elsevier B.V., 2007.
  * [9] H. Peter Gumm.  Elements of the general theory of coalgebras.  In LUATCS 99. Rand Afrikaans University, Johannesburg, South Africa, 1999.
  * [10] H. Peter Gumm.  Anhang über universelle coalgebra.  In Thomas Ihringer, editor, Allgemeine Algebra, volume 10 of Berliner Studienreihe zur Mathematik. Heldermann Verlag, 2003.
  * [11] H. Peter Gumm and Tobias Schröder.  Coalgebras of bounded type.  Mathematical Structures in Computer Science, 12(5):565–578, 2002.
  * [12] Matthew Hennessy and Robin Milner.  On observing nondeterminism and concurrency.  In J. de Bakker and J. van Leeuwen, editors, Automata, Languages and Programming. ICALP 1980, volume 85 of Lecture Notes in Computer Science, pages 159–173. Springer Verlag, Berlin, 1980.
  * [13] Dirk Hofmann, Renato Neves, and Pedro Nora.  Limits in categories of vietoris coalgebras.  Math. Struct. in Comp. Science, pages 552–587, 2019.
  * [14] Marco Hollenberg.  Hennessy-milner classes and process algebra.  In A. Ponse, de Rijke M., and Venema Y., editors, Modal Logic and Process Algebra, volume 53 of CSLI Lecture Notes, pages 107–129. CSLI Publications, 1995.
  * [15] Bart Jacobs.  Introduction to Coalgebra: Towards Mathematics of States and Observation.  Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016.
  * [16] Clemens Kupke, Alexander Kurz, and Yde Venema.  Stone coalgebras.  Theoretical Computer Science, 327:109–134, 2004.
  * [17] Lawrence S. Moss and Ignacio D. Viglizzo.  Final coalgebras for functors on measurable spaces.  Information and Computation, 204(4):610 – 636, 2006.  Seventh Workshop on Coalgebraic Methods in Computer Science 2004.
  * [18] James Munkres.  Topology.  Prentice Hall, 2000.
  * [19] J.J.M.M. Rutten.  Universal coalgebra: a theory of systems.  Technical report, CWI, Amsterdam, 1996.
  * [20] J.J.M.M. Rutten.  Universal coalgebra: a theory of systems.  Theoretical Computer Science, (249):3–80, 2000.
  * [21] Leopold Vietoris.  Bereiche zweiter Ordnung.  Monatsh. Math. Phys., 32(1), 1922.


* Athey et al. [2021] Susan Athey, Sarah Baird, Vitor Hadad, Julian Jamison, Craig McIntosh, Berk Özler, Luca Parisotto, and Dohbit Sama.  Increasing the take-up of long acting reversible contraceptives among adolescents and young women in Cameroon.  2021\.
  * Audibert et al. [2009] Jean-Yves Audibert, Sébastien Bubeck, et al.  Minimax policies for adversarial and stochastic bandits.  In _COLT_ , volume 7, pages 1–122, 2009.
  * Auer and Ortner [2010] Peter Auer and Ronald Ortner.  UCB revisited: Improved regret bounds for the stochastic multi-armed bandit problem.  _Periodica Mathematica Hungarica_ , 61(1-2):55–65, 2010.
  * Auer et al. [2002] Peter Auer, Nicolo Cesa-Bianchi, Yoav Freund, and Robert E Schapire.  The nonstochastic multiarmed bandit problem.  _SIAM Journal on Computing_ , 32(1):48–77, 2002\.
  * Billingsley [1999] Patrick Billingsley.  _Convergence of probability measures_.  John Wiley & Sons, 1999.
  * Bubeck and Cesa-Bianchi [2012] Sébastien Bubeck and Nicolò Cesa-Bianchi.  Regret analysis of stochastic and nonstochastic multi-armed bandit problems.  _Foundations and Trends® in Machine Learning_ , 5(1):1–122, 2012.
  * Bubeck and Liu [2014] Sébastien Bubeck and Che-Yu Liu.  Prior-free and prior-dependent regret bounds for thompson sampling.  In _2014 48th Annual Conference on Information Sciences and Systems (CISS)_ , pages 1–9. IEEE, 2014.
  * Caria et al. [2020] Stefano Caria, Maximilian Kasy, Simon Quinn, Soha Shami, and Alex Teytelboym.  An adaptive targeted field experiment: Job search assistance for refugees in jordan.  2020\.
  * Chapelle and Li [2011] Olivier Chapelle and Lihong Li.  An empirical evaluation of Thompson sampling.  In _Advances in Neural Information Processing Systems_ , pages 2249–2257, 2011.
  * Durrett [1996] Richard Durrett.  _Stochastic calculus: a practical introduction_ , volume 6.  CRC press, 1996.
  * Erev and Roth [1998] Ido Erev and Alvin E Roth.  Predicting how people play games: Reinforcement learning in experimental games with unique, mixed strategy equilibria.  _American Economic Review_ , pages 848–881, 1998.
  * Fan and Glynn [2021] Lin Fan and Peter W Glynn.  Diffusion approximations for thompson sampling.  _arXiv preprint arXiv:2105.09232_ , 2021.
  * Ferreira et al. [2018] Kris Johnson Ferreira, David Simchi-Levi, and He Wang.  Online network revenue management using thompson sampling.  _Operations research_ , 66(6):1586–1602, 2018\.
  * Gamarnik and Zeevi [2006] David Gamarnik and Assaf Zeevi.  Validity of heavy traffic steady-state approximations in generalized Jackson networks.  _The Annals of Applied Probability_ , 16(1):56–90, 2006.
  * Glynn [1990] Peter W Glynn.  Diffusion approximations.  _Handbooks in Operations research and management Science_ , 2:145–198, 1990.
  * Hadad et al. [2021] Vitor Hadad, David A Hirshberg, Ruohan Zhan, Stefan Wager, and Susan Athey.  Confidence intervals for policy evaluation in adaptive experiments.  _Proceedings of the National Academy of Sciences_ , 118(15), 2021.
  * Harrison [1988] J Michael Harrison.  Brownian models of queueing networks with heterogeneous customer populations.  In _Stochastic differential systems, stochastic control theory and applications_ , pages 147–186. Springer, 1988.
  * Harrison and Reiman [1981] J Michael Harrison and Martin I Reiman.  Reflected Brownian motion on an orthant.  _The Annals of Probability_ , pages 302–308, 1981.
  * Harrison and Sunar [2015] J Michael Harrison and Nur Sunar.  Investment timing with incomplete information and multiple means of learning.  _Operations Research_ , 63(2):442–457, 2015.
  * Hill et al. [2017] Daniel N Hill, Houssam Nassif, Yi Liu, Anand Iyer, and SVN Vishwanathan.  An efficient bandit algorithm for realtime multivariate optimization.  In _Proceedings of the 23rd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining_ , pages 1813–1821, 2017.
  * Hirano and Porter [2009] Keisuke Hirano and Jack R Porter.  Asymptotics for statistical treatment rules.  _Econometrica_ , 77(5):1683–1701, 2009.
  * Hirano and Porter [2021] Keisuke Hirano and Jack R Porter.  Asymptotic representations for sequential experiments.  Cowles Foundation Conference on Econometrics, 2021.
  * Howard et al. [2018] Steven R Howard, Aaditya Ramdas, Jon McAuliffe, and Jasjeet Sekhon.  Uniform, nonparametric, non-asymptotic confidence sequences.  _arXiv preprint arXiv:1810.08240_ , 2018.
  * Iglehart and Whitt [1970] Donald L Iglehart and Ward Whitt.  Multiple channel queues in heavy traffic. I.  _Advances in Applied Probability_ , 2(1):150–177, 1970.
  * Karatzas and Shreve [2005] Ioannis Karatzas and Steven E Shreve.  _Brownian Motion and Stochastic Calculus_.  Springer, 2005.
  * Kasy and Sautmann [2021] Maximilian Kasy and Anja Sautmann.  Adaptive treatment assignment in experiments for policy choice.  _Econometrica_ , 89(1):113–132, 2021.
  * Kasy and Teytelboym [2020] Maximilian Kasy and Alexander Teytelboym.  Adaptive targeted infectious disease testing.  _Oxford Review of Economic Policy_ , 36(Supplement_1):S77–S93, 2020.
  * Kelly and Laws [1993] FP Kelly and CN Laws.  Dynamic routing in open queueing networks: Brownian models, cut constraints and resource pooling.  _Queueing systems_ , 13(1):47–86, 1993.
  * Kitagawa and Tetenov [2018] Toru Kitagawa and Aleksey Tetenov.  Who should be treated? empirical welfare maximization methods for treatment choice.  _Econometrica_ , 86(2):591–616, 2018.
  * Lai and Robbins [1985] Tze Leung Lai and Herbert Robbins.  Asymptotically efficient adaptive allocation rules.  _Advances in Applied Mathematics_ , 6(1):4–22, 1985.
  * Lattimore and Szepesvári [2019] Tor Lattimore and Csaba Szepesvári.  An information-theoretic approach to minimax regret in partial monitoring.  _arXiv preprint arXiv:1902.00470_ , 2019.
  * Lattimore and Szepesvári [2020] Tor Lattimore and Csaba Szepesvári.  _Bandit algorithms_.  Cambridge University Press, 2020.
  * Le Cam [1972] Lucien M Le Cam.  Limits of experiments.  In Elizabeth L Scott Lucien M Le Cam, Jerzy Neyman, editor, _Proceedings of the Sixth Berkeley Symposium on Mathematical Statistics and Probability_ , volume 6, pages 245–261. University of California Press Berkeley–Los Angeles, 1972.
  * Luce [1959] R Duncan Luce.  _Individual choice behavior: A theoretical analysis_.  John Wiely & Son, 1959.
  * Luedtke and Chambaz [2017] Alexander R Luedtke and Antoine Chambaz.  Faster rates for policy learning.  _arXiv preprint arXiv:1704.06431_ , 2017.
  * Mannor and Tsitsiklis [2004] Shie Mannor and John N Tsitsiklis.  The sample complexity of exploration in the multi-armed bandit problem.  _Journal of Machine Learning Research_ , 5(Jun):623–648, 2004.
  * Nie et al. [2018] Xinkun Nie, Xiaoying Tian, Jonathan Taylor, and James Zou.  Why adaptively collected data have negative bias and how to correct for it.  In _International Conference on Artificial Intelligence and Statistics_ , pages 1261–1269. PMLR, 2018.
  * Reiman [1984] Martin I Reiman.  Open queueing networks in heavy traffic.  _Mathematics of operations research_ , 9(3):441–458, 1984.
  * Robbins [1952] Herbert Robbins.  Some aspects of the sequential design of experiments.  _Bulletin of the American Mathematical Society_ , 58(5):527–535, 1952.
  * Russo [2020] Daniel Russo.  Simple Bayesian algorithms for best-arm identification.  _Operations Research_ , 68(6), 2020.
  * Russo and Van Roy [2016] Daniel Russo and Benjamin Van Roy.  An information-theoretic analysis of Thompson sampling.  _The Journal of Machine Learning Research_ , 17(1):2442–2471, 2016.
  * Russo et al. [2018] Daniel Russo, Benjamin Van Roy, Abbas Kazerouni, Ian Osband, and Zheng Wen.  A tutorial on Thompson sampling.  _Foundations and Trends in Machine Learning_ , 11(1):1–96, 2018.
  * Shin et al. [2019] Jaehyeok Shin, Aaditya Ramdas, and Alessandro Rinaldo.  On the bias, risk and consistency of sample means in multi-armed bandits.  _arXiv preprint arXiv:1902.00746_ , 2019.
  * Siegmund [1985] David Siegmund.  _Sequential Analysis: Tests and Confidence Intervals_.  Springer Science & Business Media, 1985.
  * Stroock and Varadhan [2007] Daniel W Stroock and SR Srinivasa Varadhan.  _Multidimensional diffusion processes_.  Springer, 2007.
  * Thompson [1933] William R Thompson.  On the likelihood that one unknown probability exceeds another in view of the evidence of two samples.  _Biometrika_ , 25(3/4):285–294, 1933.
  * Wald [1947] Abraham Wald.  _Sequential analysis_.  John Wiley & Sons, New York, 1947.
  * Wang and Zenios [2020] Zhengli Wang and Stefanos Zenios.  Adaptive design of clinical trials: A sequential learning approach.  _Available at SSRN_ , 2020.
  * Xu and Yun [2020] Kuang Xu and Se-Young Yun.  Reinforcement with fading memories.  _Mathematics of Operations Research_ , 45(4):1258–1288, 2020.
  * Zhang et al. [2020] Kelly Zhang, Lucas Janson, and Susan Murphy.  Inference for batched bandits.  In H Larochelle, M Ranzato, R Hadsell, M F Balcan, and H Lin, editors, _Advances in Neural Information Processing Systems_ , volume 33, pages 9818–9829. Curran Associates, Inc., 2020.

##  Appendix A Technical Lemmas

We will use the following technical lemmas repeatedly.

######  Lemma 18 (Gaussian Tail Bounds).

For all $x<-\sqrt{2\pi/(9-2\pi)}$:

$\displaystyle\Phi(x)\leq$
$\displaystyle\frac{1}{|x|}\exp(-x^{2}/2),\quad\Phi(x)\geq\frac{1}{3|x|}\exp(-x^{2}/2).$
(A.1)

This immediately implies that for all $x>\sqrt{2\pi/(9-2\pi)}$:

$\Phi(x)\leq 1-\frac{1}{3x}\exp(-x^{2}/2),\quad\Phi(x)\geq
1-\frac{1}{x}\exp(-x^{2}/2).$ (A.2)

_Proof._ For the lower bound, we have that for all $x<0$:

$\displaystyle\Phi(x)=\frac{1}{\sqrt{2\pi}}\int_{-x}^{\infty}\exp(-s^{2}/2)ds\stackrel{{\scriptstyle(a)}}{{\leq}}\frac{1}{\sqrt{2\pi}}\int_{-x}^{\infty}\frac{-x}{s}\exp(-s^{2}/2)ds<\frac{1}{|x|}\exp(x^{2}/2),$

where $(a)$ follows from the fact that $-x/s\leq 1$ for all $s\geq-x$. For the
upper bound, define
$f(x)=\frac{x}{\sqrt{2\pi}(x^{2}+1)}\exp(-x^{2}/2)-\Phi(-x)$. We have that
$f(0)=-\Phi(0)<0$, $\lim_{x\to\infty}=0$, and

$f^{\prime}(x)=\frac{1}{\sqrt{2\pi}(1+x^{2})^{2}}\exp(-x^{2}/2)>0,\quad\forall
x>0.$ (A.3)

This implies that $f(x)<0$ for all $x>0$, which further implies that

$\Phi(-x)\geq\frac{|x|}{\sqrt{2\pi}(x^{2}+1)}\exp(-x^{2}/2),\quad\forall x<0.$
(A.4)

The claim follows by noting that
$\frac{|x|}{\sqrt{2\pi}(x^{2}+1)}\geq\frac{1}{3|x|}$ whenever
$|x|\geq\sqrt{2\pi/(9-2\pi)}$. ∎

The next result is a well-known, fundamental property of the Brownian motion.
Proofs can be found in standard texts (e.g., [Karatzas and Shreve, 2005,
Theorem 9.23]).

######  Lemma 19 (Law of Iterated Logarithm).

Let $W_{t}$ be a standard Brownian motion. Then, almost surely,

$\displaystyle\limsup_{t\to\infty}\frac{W_{t}}{\sqrt{2t\log\log
t}}=\limsup_{t\downarrow 0}\frac{W_{t}}{\sqrt{2t\log\log(1/t)}}=1.$ (A.5)
$\displaystyle\liminf_{t\to\infty}\frac{W_{t}}{\sqrt{2t\log\log
t}}=\liminf_{t\downarrow 0}\frac{W_{t}}{\sqrt{2t\log\log(1/t)}}=-1.$ (A.6)

##  Appendix B Additional Proofs

###  B.1 Proof of Lemma 12

_Proof._ The proof is based on Durrett [1996], and we include it here for
completeness. For $\Delta^{n}_{\epsilon}$, note that for all $\epsilon>0$,

$\Delta^{n}_{\epsilon}(z)\leq\frac{1}{\epsilon^{p}}m^{n}_{p}(z).$ (B.1)

The convergence of (6.11) thus implies that of (6.9). For $b^{n}_{k}$, note
that

$|\tilde{b}^{n}_{k}(z)-b^{n}_{k}(z)|=\int_{x:|x-z|>1}|x-z|K^{n}(z,dx)\leq
m^{n}_{p}(z),$ (B.2)

where the last step follows from the assumption $p\geq 2$. We have thus proven
that (6.11) and (6.13) together imply (6.8). Finally, for $a^{n}_{k,l}$, we
have

$\displaystyle|\tilde{a}^{n}_{k,l}(z)-a^{n}_{k,l}(z)|\leq$
$\displaystyle\int_{x:|x-z|>1}|(x_{k}-z_{k})(x_{l}-z_{l})|K^{n}(z,dx)$
$\displaystyle\leq$ $\displaystyle\int_{x:|x-z|>1}|x-z|^{2}K^{n}(z,dx)\leq
m^{n}_{p}(z),$ (B.3)

whenever $p\geq 2$, where the first step follows from the Cauchy-Schwartz
inequality, and the second step from the observation that
$(x_{k}-z_{k})^{2}\leq|x-z|^{2}$ for all $k$. This shows (6.11) and (6.12)
together imply (6.7), completing our proof. ∎

###  B.2 Proof of Lemma 13

By the law of iterated logarithm (Lemma 19 in Appendix A), we have that there
exists constant $C>0$ such that for all large $u$

$\tilde{W}_{u}/\sqrt{u}\leq-C\sqrt{\log\log u},\quad a.s.$ (B.4)

Using the lower bound on the normal cdf:

$\Phi(x)\geq\frac{1}{\sqrt{2\pi}}\frac{-x}{1+x^{2}}\exp(-x^{2}/2),\quad
x<0,\\\ $

We have that for all large $u$, almost surely:

$\displaystyle\xi(\mu,u)=1/{\Phi\left(\frac{\mu}{\sigma\sqrt{u}}+\frac{\tilde{W}_{u}}{\sigma\sqrt{u}}\right)}\leq
1/{\Phi\left(\frac{\tilde{W}_{u}}{\sigma\sqrt{u}}\right)}\leq b_{1}(\log
u)^{b_{2}},$ (B.5)

where $b_{1}$ and $b_{2}$ are positive constants that do not depend on $u$,
which further implies that for any $\alpha\in(0,1)$

$\int_{K}^{\infty}u^{-2}\xi(\mu,u)\leq 1/K^{1-\alpha},$ (B.6)

for all large $K$. ∎

###  B.3 Proof of Lemma 14

_Proof._ The first claim follows directly from the definitions of $g_{1}$ and
$\mathcal{E}_{2}$. In particular, for all $t\geq\nu$, $t\leq 1$, and under
$\mathcal{E}_{2}$,

$g_{1}(t)\geq\frac{\sqrt{Q_{2,t}}}{\sqrt{t}}\geq\sqrt{Q_{2,t}}\geq\delta^{-\alpha/2}.$
(B.7)

The second claim follows from the law of iterated logarithm (Lemma 19) applied
to $W_{2,\cdot}$ and the fact that $Q_{1,t}\leq t$. ∎

###  B.4 Proof of Lemma 15

_Proof._ The proof of the result will use the law of iterated logarithm of
Brownian motion, along with the bounds we have developed for the functions
$g_{1}$ and $g_{2}$ in Lemma 14. We have that there exist constants
$b_{1},\ldots,b_{4}$ and $c_{1},\ldots,c_{6}$, such that for all sufficiently
large $M$:

$\displaystyle\int_{M}^{1/Q_{1,v}}u^{-2}\xi(\delta,u)du$ $\displaystyle=$
$\displaystyle\int_{M}^{1/Q_{1,v}}u^{-2}/\Phi\left(g_{1}(\tau(u^{-1}))\left(\frac{\delta}{\sqrt{u}}+\frac{\tilde{W}_{u}}{\sqrt{u}}\right)+g_{2}(\tau(u^{-1}))\right)du$
$\displaystyle\stackrel{{\scriptstyle(a)}}{{\leq}}$
$\displaystyle\int_{M}^{\infty}u^{-2}/\Phi\left(-\left\lvert\frac{\tilde{W}_{u}}{\sqrt{u}}\right\rvert-
c_{1}\sqrt{\log\log\delta}\right)du$
$\displaystyle\stackrel{{\scriptstyle(b)}}{{\leq}}$
$\displaystyle\int_{M}^{\infty}u^{-2}/\Phi\left(-c_{3}(\sqrt{\log\log
u}+\sqrt{\log\log\delta})\right)du$
$\displaystyle\stackrel{{\scriptstyle(c)}}{{\leq}}$ $\displaystyle
c_{4}\int_{M}^{\infty}u^{-2}\left(\sqrt{\log\log
u}+\sqrt{\log\log\delta}\right)\exp\left(c_{3}^{2}\left(\sqrt{\log\log
u}+\sqrt{\log\log\delta}\right)^{2}\right)du$
$\displaystyle\stackrel{{\scriptstyle(d)}}{{\leq}}$ $\displaystyle
c_{4}\int_{M}^{\infty}u^{-2}\left(\sqrt{\log\log
u}+\sqrt{\log\log\delta}\right){(\log u)^{b_{1}}(\log\delta)^{b_{2}}}du$
$\displaystyle{\leq}$ $\displaystyle
c_{5}(\log\delta)^{b_{3}}\int_{M}^{\infty}u^{-2}(\log u)^{b_{4}}du$
$\displaystyle{\leq}$ $\displaystyle c_{6}(\log\delta)^{b_{3}}M^{1-\beta}.$
(B.8)

where the various steps are based on the following facts:

  1. (a):

$g_{1}(t)\leq 1$, $|g_{2}(t)|\leq c_{1}\sqrt{\log\log\delta}$ for all $t\geq
v$ and that $\tau(u^{-1})\geq v$ when $u\leq 1/Q_{1,u}$.

  2. (b):

Law of iterated logarithm applied to $\tilde{W}$.

  3. (c):

Lower bound on the normal cdf (Lemma 18 in Appendix A):
$\Phi(x)\geq\frac{1}{\sqrt{2\pi}}\frac{-x}{1+x^{2}}\exp(-x^{2}/2)$, for $x<0$.

  4. (d):

Cauchy-Schwartz.

This proves our claim. ∎

###  B.5 Proof of Lemma 16

_Proof._ From (6.90), we have that

$\displaystyle\frac{d}{dt}Q_{2,t}=$
$\displaystyle\Phi\left(g_{1}(t)\left(\frac{-\delta
Q_{2,t}-W_{2,Q_{2,t}}}{\sqrt{Q_{2,t}}}\right)+g_{2}(t)\right)$
$\displaystyle\leq$
$\displaystyle\Phi\left(-g_{1}(t)\sqrt{Q_{2,t}}\delta+\left\lvert\frac{W_{2,Q_{2,t}}}{\sqrt{Q_{2,t}}}\right\rvert+g_{2}(t)\right)$
$\displaystyle\leq$
$\displaystyle\Phi\left(-g_{1}(t)\sqrt{Q_{2,t}}\delta+C\sqrt{\log\log\delta}\right),$
(B.9)

where the first inequality follows from the fact that $g_{1}(t)\leq 1$. The
second follows from applying the law of iterated logarithm to
$\left\lvert\frac{W_{2,Q_{2,t}}}{\sqrt{Q_{2,t}}}\right\rvert$, the fact that
$Q_{2,t}\geq\delta^{-\alpha}$ by the definition of $\tau^{*}_{\delta}$, and
the upper bound on $|g_{2}(t)|$ from Lemma 14. ∎

###  B.6 Proof of Lemma 17

_Proof._ Define the function

$h(t)=\frac{Q_{2,t}}{t}.$ (B.10)

We have

$g_{1}(t)=\sqrt{\frac{Q_{1,t}}{t}}=\sqrt{1-h(t)}.$ (B.11)

Our goal is to show that $h(t)$ stays below $2/3$ for all
$t\in[\tau^{*}_{\delta},1)$. First, we verify that

$h(\tau^{*}_{\delta})\leq 1/2.$ (B.12)

This is true under the condition of $\mathcal{E}_{1}$, by noting that
$Q_{1,\tau^{*}_{\delta}}\geq Q_{2,\tau^{*}_{\delta}}$ and $Q_{1,t}+Q_{2,t}=t$,
and hence

$h(\tau^{*}_{\delta})=\frac{Q_{2,\tau^{*}_{\delta}}}{Q_{1,\tau^{*}_{\delta}}+Q_{2,\tau^{*}_{\delta}}}\leq
1/2.$ (B.13)

Suppose, for the sake of contradiction that $h(t_{0})=1/2$ for some
$t_{0}\geq\tau^{*}_{\delta}$. In light of (B.12), it suffices to show that
$h^{\prime}(t_{0})<0$, which would imply that $h$ will not increase beyond
$1/2$ to ever reach $2/3$. We have that

$h^{\prime}(t)=\frac{\frac{d}{dt}Q_{2,t}}{t}-\frac{Q_{2,t}}{t}\frac{1}{t}=\frac{\frac{d}{dt}Q_{2,t}-h(t)}{t}.$
(B.14)

Evaluating this derivative at $t=t_{0}$ yields

$h^{\prime}(t_{0})=\frac{\frac{d}{dt}Q_{2,t}-h(t_{0})}{t_{0}}=\frac{\frac{d}{dt}Q_{2,t_{0}}-1/2}{t_{0}}.$
(B.15)

It thus suffices to show that $\frac{d}{dt}Q_{2,t_{0}}<1/2$. To this end, note
that by the definition of $t_{0}$,

$h(t)\leq 1/2,\quad\forall t\in[\tau^{*}_{\delta},t_{0}].$ (B.16)

By Lemma 16, we have that for all large $\delta$ and
$t\in[\tau^{*}_{\delta},t_{0})$,

$\displaystyle\frac{d}{dt}Q_{2,t}\leq$
$\displaystyle\Phi\left(-g_{1}(t)\sqrt{Q_{2,t}}\delta+C\sqrt{\log\log\delta}\right)$
$\displaystyle=$
$\displaystyle\Phi\left(-\sqrt{1-h(t)}\sqrt{Q_{2,t}}\delta+C\sqrt{\log\log\delta}\right)$
$\displaystyle\stackrel{{\scriptstyle(a)}}{{\leq}}$
$\displaystyle\Phi\left(-\sqrt{\frac{Q_{2,t}}{2}}\delta+C\sqrt{\log\log\delta}\right)$
$\displaystyle\stackrel{{\scriptstyle(b)}}{{\leq}}$
$\displaystyle\Phi\left(-\delta^{1-\alpha/2}/\sqrt{2}+C\sqrt{\log\log\delta}\right)$
$\displaystyle<$ $\displaystyle 1/2,$ (B.17)

where step $(a)$ follows from (B.16) and $(b)$ from the fact that
$Q_{2,t}\geq\delta^{-\alpha}$ for all $t\geq\tau^{*}_{\delta}$. The final
inequality follows from the fact that $\alpha<2$ and hence
$\delta^{1-\alpha/2}\gg\sqrt{\log\log\delta}$ for all large $\delta$. This
proves the claim. ∎