Safe & Robust Reachability Analysis of Hybrid Systems
Eugenio Moggi1a , Amin Farjudianb , Adam Duracz2c , Walid Taha3b

arXiv:1709.05658v1 [cs.LO] 17 Sep 2017

a DIBRIS,

Genova Univ., v. Dodecaneso 35, 16146 Genova, Italy, Email: moggi@unige.it
University, Halmstad, Sweden, Email: name.surname@hh.se
c Rice University, Houston, TX, USA, Email: adam.duracz@rice.edu

b Halmstad

Abstract
Hybrid systems—more precisely, their mathematical models—can exhibit behaviors, like Zeno behaviors, that are absent in purely discrete or purely continuous systems. First, we observe that, in this context, the usual definition of reachability—namely, the reflexive and transitive closure of a transition relation—can
be unsafe, ie, it may compute a proper subset of the set of states reachable in
finite time from a set of initial states. Therefore, we propose safe reachability,
which always computes a superset of the set of reachable states.
Second, in safety analysis of hybrid and continuous systems, it is important
to ensure that a reachability analysis is also robust wrt small perturbations to
the set of initial states and to the system itself, since discrepancies between
a system and its mathematical models are unavoidable. We show that, under
certain conditions, the best Scott continuous approximation of an analysis A is
also its best robust approximation. Finally, we exemplify the gap between the
set of reachable states and the supersets computed by safe reachability and its
best robust approximation.
Keywords: Domain theory; Models of hybrid systems; Reachability.

Introduction
In a transition system—ie, a binary relation → on a set of states—reachability
is a clearly defined notion, namely, the reflexive and transitive closure →∗ of
→. Reachability analysis plays an important role in computer-assisted verification and analysis [ACH+ 95], since safety (a key system requirement) is usually
formalized in terms of reachability, namely:
state s is safe ⇐⇒ it is not possible to reach a bad state from s.
1 Research

partially supported by the Swedish Knowledge Foundation.
done while the author was a PhD student at Halmstad University.
3 Research partially supported by US NSF award #1736754 “A CPS Approach to Robot
Design” and the Swedish Knowledge Foundation project “AstaMoCA: Model-based Communications Architecture for the AstaZero Automotive Safety Facility”.
2 Work

Preprint submitted to Journal of TCS

August 7, 2017

For a hybrid system one can define a transition relation → on a continuous and
uncountable state space, but →∗ captures only the states reachable in finitely
many transitions, and they can be a proper subset of those reachable in finite
time! Hybrid systems with Zeno behaviors—where infinitely many events occur
in finite time—are among the systems in which the two notions of reachability
differ. Zeno behaviors arise naturally when modeling rigid body dynamics with
impacts, as illustrated by the system consisting of a bouncing ball (Example 2.8),
whose Zeno behavior is due to the modeling of impacts as discrete events.
Contributions
The first contribution of this paper is the notion of safe reachability
(Def 3.6), which gives an over-approximation—ie, a superset—of the states
reachable in finite time, including the case where the hybrid system has Zeno behaviors. Mathematical models are always simplifications, through abstractions
and approximations, of real systems. Simplifications are essential to making
analyses manageable. In safety analysis, over-approximations are acceptable,
since they can only lead to false negatives, ie, the analysis may wrongly conclude that (a state s of) the system in unsafe, because the over-approximation
includes some unreachable bad states.
The second contribution is to show, under certain assumptions, that the best
Scott continuous approximation of safe reachability coincides with its best robust
approximation. In safety analysis robust over-approximations are important,
because inaccuracies in the modeling of a cyber-physical system (as well as in
its building and testing) are unavoidable, as convincingly argued in [Frä99].
Related Work
Reachability maps are arrows in the category of complete lattices and monotonic maps, which is the standard setting for defining and comparing abstract
interpretations [CC92]. We build directly on the following papers.
• [GST09] is an excellent tutorial on hybrid systems, from which we borrow
the definition of hybrid system (Def 2.1), but avoid the use of hybrid arcs,
since they cannot reach nor go beyond Zeno points.
• [CR04, Cui07] introduce topological transition systems (TTS), which we
use for defining safe reachability (Def 3.6). In TTSs on discrete spaces,
standard reachability (Def 3.1) and safe reachability (Def 3.6) coincide.
• [Eda95] is one among several papers, where Edalat recasts mainstream
mathematics in Domain Theory, and shows what is gained by doing so.
In this context Domain Theory becomes particularly relevant when the
Scott and Upper Vietoris topologies on certain hyperspaces coincide.
• [Frä99, GKC13] show that proving δ-safety, ie, safety of a hybrid system
subject to some noise bounded by δ, can make the verification task easier,
besides excluding systems that are safe only under unrealistic assumptions.

2

Summary
The rest of the paper is organized as follows:
• Sec 2 recalls the definition of a hybrid system from [GST09], defines the
corresponding transition relation (Def 2.3), and gives some examples.
• Sec 3 introduces two reachability maps Rf and Rs (Def 3.1 and 3.6, respectively), establishes their properties and how they relate to each other.
• Sec 4 uses the poset-enriched category of complete lattices and monotonic
maps (see Def 4.4) as a framework to discuss approximations and relate
reachability maps defined on different complete lattices. We also give a
systematic way to turn a monotonic map f between complete lattices into
a Scott continuous map f ✷ (see Prop 4.14).
• Sec 5 introduces the notion of robustness (see Def 5.1) and says when
robustness and Scott continuity coincide (see Thm 5.7).
• Sec 6 analyses (with the aid of pictures) the differences between the underapproximation Rf and several over-approximations (from Rs to Rs✷ ) of sets
of reachable states, for the hybrid systems introduced in Sec 2.
Appendix A contains some proofs that were too long to inline into the text.
1. Mathematical preliminaries
We assume familiarity with the notions of Banach, metric, and topological
spaces, and the definitions of open, closed, and compact subsets of a topological
space (see, eg, [Con90, Kel75]). The three notions of space are related as follows:
• Every Banach space is a Cauchy complete metric space whose distance is
△
d(x, y) = |y − x|, where |x| is the norm of x;
• Every metric space is a topological space whose open subsets are given by
△
unions of open balls B(x, δ) = {y|d(x, y) < δ}.
Throughout the paper, for the sake of simplicity, one may replace Banach spaces
with Euclidean spaces Rn . For membership we may write x:X instead of x ∈ X,
and we use the following notations:
• R is the Euclidean space of the real numbers;
• N and ω denote the natural numbers with the usual linear order;
• P(S) is the set of subsets of a set S (we use the same notation also when
S is a set with additional structure, eg, a Banach or topological space);
• O(S) is the set of open subsets of a topological space S, and C(S) is the set
of closed subsets (we use the same notation also when S is a set with additional structure that induces a topology, eg, a Banach or metric space);
3

• Set is the category of sets and (total) maps;
• Setp is the category of sets and partial maps;
• Top is the category of topological spaces and continuous maps.
Finally, we recall some definitions and their basic properties:
△

• x is a limit of a sequence (xn |n:ω) in the topological space S ⇐⇒
∀O:O(S).x:O =⇒ ∃m.∀n > m.xn :O.

The limits of a sequence form a closed subset of S. In a metric space a
sequence has at most one limit.

• x is an accumulation point of a sequence (xn |n:ω) in the topological
△
space S ⇐⇒ ∀O:O(S).x:O =⇒ ∀m.∃n > m.xn :O.
The accumulation points of a sequence form a closed subset of S, every
limit is also an accumulation point, and every accumulation point is a limit
of a sub-sequence (xf (n) |n:ω) for some strictly increasing f :Set(ω, ω), ie,
∀n.f (n) < f (n + 1). In a metric space, if a sequence has a limit, then the
limit is the only accumulation point.

• The derivative f˙:Setp (R, S) of a partial map f :Setp (R, S) from R to a
△
Banach space S is given by f˙(x) = v ⇐⇒ ∃δ > 0 st B(x, δ) is included
in the domain of f , and for any sequence (xn |n:ω) in B(x, δ) − {x}, if x
(x)
is the limit of (xn |n:ω) in R, then v is the limit of ( f (xxnn)−f
|n:ω) in S.
−x

If f˙(x) is defined, then f must be continuous at x. A stronger requirement
is that f˙ is defined and continuous in B(x, δ), in this case f is called
continuously differentiable in B(x, δ).

2. Hybrid Systems and Topological Transition Systems
In this section, we define what is a hybrid system (cf. [GST09]), namely,
a mathematical model suitable for describing cyber-physical systems; what is
a topological timed transition system (cf. [CR04]), namely, an abstraction of
hybrid systems useful for defining various reachability maps; and, finally, we
introduce some example hybrid systems that will be used throughout the paper.
Definition 2.1. A Hybrid System (HS for short) H on a Banach space S is a
pair (F, G) of binary relations on S, ie, F, G:P(S×S), respectively called flow and
jump relation. We say that H is open/closed/compact, when the relations
F and G—as subsets of the topological space S × S—are open/closed/compact.
Remark 2.2. In [GST09], the authors restrict S to a Euclidean space Rn , and
show that HS subsume Hybrid Automata [ACH+ 95] and Switching Systems.

4

The flow and jump relations are constraints for the trajectories describing how
the HS evolves over time (see the definition of hybrid arc in [GST09, page 39]).
Trajectories are not needed to define reachability (Sec 3), since a simpler notion
of timed transition suffices (see also [ACH+ 95, Sec 2] and [Pla08, Def 5]).
Definition 2.3. A Topological Timed Transition System (TTTS) is a pair
✲ ) consisting of a topological space S and a timed transition relation
(S,
△
✲ :P(S × T × S), where T =
{d:R|d ≥ 0} is the continuous time line. Its
d
△
corresponding transition relation on S is given by s ✲ s′ ⇐⇒ ∃d.s ✲ s′ .
d
△
A HS H = (F, G) on S induces a TTTS (S, ✲ ) such that s ✲ s′ ⇐⇒
H

H

′

1. d = 0 and s G s , or,
2. d > 0 and there exists a continuous map f :Top([0, d], S) such that:
• the derivative f˙ of f is defined and continuous in (0, d);
• s = f (0), s′ = f (d) and ∀t:(0, d).f (t) F f˙(t).

In this case we say that f realizes the transition.
Remark 2.4. The Banach space structure is just what is needed to define
derivatives. Hybrid arcs (cf. [GST09]) could be defined in term of a transition
relation where the labels d > 0 are replaced by their realizer maps f .
In [GST09] the requirements on f are more relaxed than ours, namely: f
must be absolutely continuous (which, in our case, is implied by the continuity
of f˙), and the flow relation must hold almost everywhere in (0, d). However, the
safe evolution and safe reachability maps (see Def 3.6) are insensitive to these
changes. Thus, we have adopted the requirements on f that are mathematically
simpler to express.
In [Dur16] the requirements on f are stricter than ours, namely: f˙ must
extend continuously to [0, d], and the flow
√ relation must hold also at the endpoints. For instance, the map f (t) = t is continuous in [0, d], its derivative
f˙(t) = 2∗1√t is continuous in (0, d), but it cannot be extended continuously to 0.
d
The main rationale for the stricter requirements is that a transition s ✲ s′
with d > 0 can only start from a state in the domain of the flow relation F .

Notation 2.5. Given a first-order language with an interpretation in a Banach
space S, a HS on S can be described by two formulas, a flow formula F (x, ẋ) and
a jump formula G(x, x+ ), with two free variables each: x denotes the current
state, ẋ denotes the derivative of a trajectory flowing through x, and x+ denotes
a state reachable from x with one jump.
Similarly, given a two sorted language, with one sort interpreted in R and
the other in a topological space S, a timed transition relation can be described
by a formula T (x, d, x′ ) with three free variables: x denotes the starting state,
d:R the duration of the transition, and x′ the final state.
We introduce some hybrid systems, and give explicit descriptions of their timed
transition relations (see also the Figures in Sec 6).
5

Example 2.6 (Expand). HE is a HS on R describing the expansion of a quantity m until it reaches a threshold M > 0. The flow and jump relations are:
F = {(m, ṁ)|0 ≤ m = ṁ ≤ M },

G = ∅.

It has two kinds of trajectories depending on the start state m0 (see Fig 1).
1. When m0 = 0, the quantity remains 0 forever, ie, f (t) = 0 when t ≥ 0.
2. When m0 :(0, M ), there is an exponential growth f (t) = m0 ∗ et until f (t)
becomes M , then the trajectory cannot progress further.
The timed transition relation
• m

✲ consists of the transitions

HE

✲ m′ with 0 < d and 0 ≤ m ≤ m′ = m ∗ ed ≤ M .

d

Removing (M, M ) from F does not change the timed transitions, while adding
d
(M, 0) to F entails the addition of the transitions M ✲ M with d > 0.
Example 2.7 (Decay). The hybrid system HD on R describes the decay of a
quantity when m > 0, and a ‘refill’ to M > 0 when m = 0. The flow and jump
relations are:
F = {(m, ṁ)|m > 0 ∧ ṁ = −m},

G = {(0, M )}.

It has two kinds of trajectories, depending on the start state m0 (see Fig 2):
1. When m0 = 0, there is a refill followed by a decay f (t) = M ∗ e−t .
2. When m0 > 0, there is a decay f (t) = m0 ∗ e−t . Thus, f (t) > 0 when
t ≥ 0, and f (t) → 0 as t → +∞.
✲ consists of the transitions
The timed transition relation
HD

• 0
• m

✲ M , and

0

✲ m′ with 0 < d and m > m′ = m ∗ e−d > 0.

d

Adding (0, 0) to F entails the addition of the transitions 0

✲ 0 with d > 0.

d

Example 2.8 (Bouncing ball). The hybrid system HB on R2 describes a
bouncing ball with height h ≥ 0 and velocity v, which is kicked when it stops,
ie, when h = v = 0. We assume the force of gravity to be −1 (for the sake
of simplicity), a coefficient of restitution b (we do not restrict its value, but
b:[−1, 0] would be the obvious restriction), and a velocity V > 0 given to the
ball when it is kicked. Formally:
• F = {((h, v), (ḣ, v̇))|h > 0 ∧ ḣ = v ∧ v̇ = −1}.
• G = {((0, v), (0, v + ))|v < 0 ∧ v + = b ∗ v} ⊎ {((0, 0), (0, V ))}.
It has seven kinds of trajectories starting from (h = 0, v > 0), depending on the
value of b (see Fig 3).
6

1. When b < −1, the ball never stops (its energy increases at each bounce).
2. When b = −1, the ball never stops (its energy remains constant).
3. When b:(−1, 0), the ball stops in finite time, but after infinitely many
bounces (this is a Zeno behavior), then it is kicked, ie, (h = 0, v = V ).
4. When b = 0, the ball stops as it hits the ground, then it is kicked.
5. When b:(0, 1), as the ball hits the ground, it stops after infinitely many
instantaneous slowdowns 0 > bn ∗ v → 0 (this is a chattering Zeno
behavior), then it is kicked.
6. When b = 1, as the ball hits the ground, the trajectory cannot progress
further in time.
7. When b > 1, as the ball hits the ground, its velocity drifts to −∞ after
an infinite sequence of instantaneous accelerations 0 > bn ∗ v → −∞, and
the trajectory cannot progress further in time.
✲ consists of the following transitions:
The timed transition relation
HB

• (0, v)
• (0, 0)

✲ (0, v ′ ) with v < 0 and v ′ = b ∗ v, this is a bounce;

0

✲ (0, V ), this is when the ball is kicked;

0

• (h, v) ✲ (h′ , v ′ ), with 0 < d and 0 ≤ h, h′ = h+v∗d− d2 ∧v ′ = v−d, this
2
is when the ball moves while the energy E(h, v) = h + v2 stays constant.
d

2

2∗v
In particular, (0, v) ✲ (0, −v) is the transition between two bounces. Adding
{((0, v), (ḣ, v̇))|ḣ = v ∧ v̇ = −1} to F does not change the timed transitions,
0
while adding ((0, 0), (0, 0)) to G entails the addition of (0, 0) ✲ (0, 0).

The following construction adds a clock to a HS to record the passing of time.
Definition 2.9. Given a HS H = (F, G) on S, the derived HS t(H) = (F ′ , G′ )
on R × S adds a clock to H, namely:
△

• F ′ = {((t, s), (1, ṡ))|s F ṡ}, because dt/dt = 1;
△

• G′ = {((t, s), (t, s+ ))|s G s+ }, because jumps are instantaneous.
Proposition 2.10. (t, s)

✲ (t′ , s′ ) ⇐⇒ t′ = t + d ∧ s

✲ s′ .

d

d

t(H)

H

Proof. Only the case d > 0 is non-trivial.
• If f ′ :Top([0, d], R × S) realizes the transition (t, s)

d

✲ (t′ , s′ ), then

t(H)

f ′ (x) = (t + x, f (x)) for a unique f :Top([0, d], S), and moreover this f
d
realizes the transition s ✲ s′ .
H

• Conversely, if f :Top([0, d], S) realizes s
realizes (t, s)

✲ (t′ , s′ ).

d

✲ s′ , then f ′ (x) = (t + x, f (x))

d

H

✷

t(H)

7

3. Evolution and Reachability
Transition systems (TS for short) provide the main formalism for modeling
discrete systems. The formalism does not mention time explicitly, but it assumes
that time is discrete, and each transition takes one time unit (or alternatively,
it abstracts from time and describes only the order of discrete state changes).
Given a TS (S, →), ie, a binary relation → on a set S (aka a directed graph),
we identify the discrete time line with the set N of natural numbers and define
the following notions related to the TS.
• A trajectory is a map f :Set([0, n], S) such that ∀i < n.f (i) → f (i + 1) for
some n:N, or equivalently, a path f :S+ in the graph. The length of f is n
and f (0) is its starting state.
△

• The evolution map Ef :P(S) → P(N × S) is Ef (I) = {(n, s′ )|∃s:I.s →n s′ },
or equivalently the union of (the graphs of) all trajectories starting from
the set I of initial states. Therefore, Ef (I) says at what time a state is
reached, but forgets the trajectories used to reach it. However, when →
is deterministic, there is at most one trajectory of length n from s to s′ ,
which can be recovered from Ef ({s}).
△

• The reachability map Rf :P(S) → P(S) is Rf (I) = {s′ |∃s:I.s →∗ s′ }, or
equivalently {s′ |∃n.(n, s′ ):Ef (I)}. Therefore, Rf (I) says whether a state is
reachable from I, but forgets at which time instances it is reached.
For TTTS (and HS) one would like to reuse as much as possible the theory
available for TS. The main point of this section is that naive reuse can result
under-approximating what is reachable in finite time. To address this problem,
we present a solution that computes an over-approximation (see Sec 3.1). This
solution exploits the topological structure of the state space S and the continuous
time line T.
We choose to cast analyses (eg reachability) as monotonic maps (like Rf )
rather than as relations (like →∗ ). This becomes essential in Def 3.6 and for
defining approximability (Sec 4) and robustness (Sec 5) of an analysis.
Definition 3.1. The evolution map Ef :P(S) → P(T×S) and the reachability
✲ ) are:
map Rf :P(S) → P(S) for a TTTS (S,
△

• Ef (I) = the smallest S:P(T × S) such that {0} × I ⊆ S and S is closed
d
wrt timed transitions, ie, (t, s) ∈ S ∧ s ✲ s′ =⇒ (t + d, s′ ) ∈ S.
△

• Rf (I) = the smallest S:P(S) such that I ⊆ S and
S is closed wrt transitions, ie, s ∈ S ∧ s ✲ s′ =⇒ s′ ∈ S.
We denote with Ef H and Rf H the evolution and reachability maps for the TTTS
induced by the HS H.

8

Remark 3.2. The ”f” in Ef and Rf stands for ”finite”, because these maps
consider only states that are reachable in finitely many transitions. There is an
important difference between discrete systems and continuous/hybrid systems.
In a discrete (time) system the transition relation suffices to define trajectories,
the evolution, and the reachability maps. In a continuous (time) system: to
define trajectories, the structure of a HS is needed; to define the evolution map,
the timed transition relation suffices; and to define the reachability map, the
transition relation suffices.
Theorem 3.3. The following properties hold:
1. Ef is monotonic, ie, I0 ⊆ I1 =⇒ Ef (I0 ) ⊆ Ef (I1 ), and preserves unions,
ie, ∀K ⊆ P(S).Ef (∪K) = ∪{Ef (I)|I:K}.
2. Rf is monotonic, preserves unions, is a closure, ie, I ⊆ Rf (I) = Rf 2 (I),
and π(Ef (I)) = Rf (I).
3. If H is a HS on S, then ∀I:P(S).Ef H (I) = Rf t(H) ({0} × I) and
∀J:P(R × S).π(Rf t(H) (J)) = Rf H (π(J)).
Here, π:R × S

△
✲ S is π(t, s) =
s, and π(J) is the image of J ⊆ R × S.

Proof. See Appendix A.
A pair (t, s′ ) is in Ef H (I) exactly when s′ is reached at time t in finitely many
transitions starting from some s:I. In Zeno systems there are states that are
reached at a finite time t, but not in a finite number of transitions. Therefore,
Ef H and Rf H may under-approximate what we would like to compute.
Definition 3.4. A Zeno behavior of H is a sequence ((dn , sn )|n:ω) in T × S
such that:
dn
1. ∀n.sn ✲ sn+1 ,
XH
△
2. d =
dn is defined and finite, and,
n:ω

3. the sequence has infinitely many jumps, ie, {n|dn = 0} is infinite.

d
The last requirement excludes fragmentations of a flow transition s ✲ s′ , ie,
d
sequences ((f (tn ), tn+1 − tn )|n:ω), where f :Top([0, d], S) realizes s ✲ s′ , and
(tn |n:ω) is a strictly increasing sequence with t0 = 0 and supn:ω tn = d.
The accumulation points of (sn |n:ω) in the topological space S are called
the Zeno points, and d is called the Zeno time, since it is the time needed to
reach a Zeno point from s0 .

HB of Example 2.8 is the classical case of a HS with Zeno behavior. When b
is in the interval (−1, 0), the stop state s = (0, 0) is reached in finite time from
s0 = (0, v) with v < 0, but after infinitely many bounces (see Fig 3 in Sec 6).
When b is in the interval (0, 1), HB has a chattering Zeno behaviour, ie, the stop
state is reached after infinitely many instantaneous slowdowns. On the other
hand, Prop 3.5 shows that the stop state is not in Rf HB ({s0 }) when b 6= 0.
9

2

△

Proposition 3.5. Let S = {(h, v)|h ≥ 0 ∧ E(h, v) > 0}, where E(h, v) = h + v2
is the energy in state (h, v). Then, Rf HB (S) = S, provided that b 6= 0.
Proof. We prove that S is closed wrt the transition relation
analysis. There are three cases:

✲ by case

HB

• bounce, ie, (0, v) ✲ (0, b ∗ v) with v < 0: (0, v) ∈ S, because E(0, v) =
v2
2 > 0, and (0, b ∗ v) ∈ S, because E(0, b ∗ v) > 0 when b 6= 0;
• ball kicked, ie, (0, 0)

✲ (0, V ): there is nothing to prove, as (0, 0) 6∈ S;

• move, ie, (h, v) ✲ (h′ , v ′ ) with h, h′ ≥ 0 ∧ v > v ′ ∧ E(h, v) = E(h′ , v ′ ):
(h, v) ∈ S =⇒ (h′ , v ′ ) ∈ S holds, because the energy stays constant. ✷
We propose a key change to Def 3.1 that exploits the topology on S and T by
considering reachable also a state that is arbitrarily close to reachable states.
Definition 3.6 (Safe maps). Let C(S) be the set of closed subsets of a topological space S. The safe evolution map Es:C(S) → C(T × S) and the safe
✲ ) are:
reachability map Rs:C(S) → C(S) for a TTTS (S,
△

• Es(I) = the smallest S:C(T × S) such that {0} × I ⊆ S and closed wrt
timed transitions.
△

• Rs(I) = the smallest S:C(S) such that I ⊆ S, and closed wrt transitions.
We denote with EsH and RsH the safe evolution and safe reachability maps for
the TTTS induced by the HS H, respectively.
Remark 3.7. If s0 :I and ((dn , sn )|n:ω) is a Zeno behavior of H, then the set
S = RsH (I) includes every Zeno point s (similarly EsH (I) includes (d, s), where
d is the Zeno time and s is a Zeno point). In fact, the sequence (sn |n:ω) is
included in S, and all its accumulation points must be in S, because S is closed.
The set S also includes asymptotically reachable points—ie, accumulation points
dn
✲ sn+1 and P dn = +∞—that
of a sequence (sn |n:ω) such that ∀n.sn
n:ω
H
may not be reachable in finite time.
The safe maps include other points that should be considered reachable in
finite time, but are not reachable in a finite number of transitions. For instance,
consider a HS H = (F, ∅) on Rn that can only flow—thus, it cannot have Zeno
behaviors—and a continuous map f :Top([0, d), Rn ) such that:
• the derivative f˙ of f is defined and continuous in (0, d),

• ∀t:(0, d).f (t) F f˙(t), but,

• there is no way to extend f to a continuous map on [0, d].
If f (0):I, then EsH (I) includes {(t, f (t))|t < d} and also the pairs (d, s) with s
1
) satisfies
accumulation point of f (t) as t → d. For instance, f (x) = x ∗ sin( x−1
the above properties for d = 1.
10

There is an analogue of Thm 3.3 for the safe maps, but with weaker properties,
mainly because the set of closed subsets is closed only wrt finite unions.
Theorem 3.8. The following properties hold:
1. Es is monotonic and preserves finite unions.
2. Rs is monotonic, preserves finite unions, is a closure, and
π(Es(I)) ⊆ Rs(I).
3. ∀I:P(S).Ef (I) ⊆ Es(I), and ∀I:P(S).Rf (I) ⊆ Rs(I).
4. If H is a HS on S, then ∀I:C(S).EsH (I) = Rst(H) ({0} × I), and
∀J:C(R × S).π(Rst(H) (J)) ⊆ RsH (π(J)).
Here, S:C(S) is the closure of S:P(S), ie, the smallest S ′ :C(S) such that S ⊆ S ′ .
Proof. See Appendix A.
3.1. Summary of inclusion relations
We provide a summary of the inclusion relations among the sets computed
by the four maps defined in this section. Given a hybrid system H on S and
a subset I:P(S) of initial states, there are two subsets E:P(T × S) and R:P(S)
informally defined as:
• E: the set of (t, s) such that s is reached at time t, ie, there is a trajectory
of H starting from a state in I and reaching s at time t.
• R: the set of states reachable (from I) in finite time, ie, R = π(E).
The monotonic maps in Def 3.1 and 3.6 allow to define four subsets:
• Ef H (I): the set of (t, s) such that s is reached at time t in finitely many
transitions.
• Rf H (I): the set of states reachable in finitely many transitions, ie, π(Ef H (I)).
• EsH (I):C(T × S) a closed over-approximation of E.
• RsH (I):C(S) a closed over-approximation of R.
When I:C(S), the inclusion relations among these six subsets are:
Ef H (I)

⊂

❄
Ef H (I)

✲ E
∩

∩

⊂

Rf H (I)

⊂

❄
❄
✲ EsH (I) Rf H (I)

✲ R

⊂

✲ π(EsH (I))
∩

∩

⊂

❄
✲ RsH (I)

By suitable choices of closed HS H on R and singletons I we show that no
other inclusion holds. In particular, Ef H and Rf H may compute proper underapproximations, while EsH and RsH may compute proper over-approximations.
11

1. Ef H (I) ⊂ Ef H (I) ⊂ E = EsH (I) and Rf H (I) ⊂ Rf H (I) ⊂ R = RsH (I).
△
Take H = (∅, G) with G = {(x, x/2)|0 ≤ x} ⊎ {(0, 2)} and I = {1}, then
• Rf H (I) = {2−n |n:N} and Ef H (I) = {0} × Rf H (I)

• Rf H (I) = {2−n |n:N} ⊎ {0} and Ef H (I) = {0} × Rf H (I)

• RsH (I) = {2−n |n:N} ⊎ {0, 2} and EsH (I) = {0} × RsH (I)

2. Ef H (I) = E ⊂ Ef H (I) ⊂ EsH (I) and Rf H (I) = R ⊂ Rf H (I) ⊂ π(EsH (I)).
△
Take H = (∅, G) with G = {(2, x)|x ≥ 2} ⊎ {(x, 1/x)|x ≥ 2} ⊎ {(0, 1)} and
I = {2}, then
• Rf H (I) = [2, +∞) ⊎ (0, 1/2] and Ef H (I) = {0} × Rf H (I)

• Rf H (I) = [2, +∞) ⊎ [0, 1/2] and Ef H (I) = {0} × Rf H (I)

• RsH (I) = [2, +∞) ⊎ [0, 1/2] ⊎ {1} and EsH (I) = {0} × RsH (I)

3. Rf H (I) = R = π(EsH (I)) ⊂ Rf H (I) ⊂ RsH (I).
△
Take H = (F, {(0, 2)}) with F = {(x, −x)|0 ≤ x} and I = {1}, then
• Ef H (I) = E = EsH (I) = {(t, e−t )|0 ≤ t}
• Rf H (I) = (0, 1]

• Rf H (I) = [0, 1]

• RsH (I) = [0, 2]
4. A Framework for Approximability
All maps introduced in Sec 3 (see Def 3.1 and 3.6) are monotonic maps
between complete lattices. Thus, they live in the poset-enriched category Po of
complete lattices (more generally of posets) and monotonic maps. In fact, one
can stay within Po, by defining a complete lattice of hybrid systems on S (this
can be done also for timed transition relations), by exploiting its cartesian closed
structure, and by using the order relation to express when something is an overor under-approximation of something else. Po is also the natural setting for
defining and comparing abstract interpretations [CC92], with adjunctions giving
a systematic way to relate more concrete to more abstract interpretations.
Therefore, Po will be used as a framework in which to place and compare the
reachability (and evolution) maps introduced so far, as well as their variants.
Definition 4.1. A poset-enriched category A (see [Kel82]) consists of:
• a class of objects, notation X:A;
• a poset A(X, Y ) of arrows from X to Y , notation X

✲ Y and f1 ≤ f2 ;

f

idX
✲ X and composition X g◦f✲ Z of composable arrows
• identities X
f
g
✲ Z satisfying the usual equations and monotonicity, ie,
X ✲ Y
f1 ≤ f2 :X → Y ∧ g1 ≤ g2 :Y → Z =⇒ (g1 ◦ f1 ) ≤ (g2 ◦ f2 ):X → Z.

12

✲

f

An adjunction f ⊣ g is a pair X ✛

g

Y of maps st f ◦ g ≤ idY ∧ idX ≤ g ◦ f .

If A has a terminal object 1 and h:A(X, X), then:
△

• µ:A(1, X) is an initial algebra (aka least prefix-point) for h ⇐⇒
h ◦ µ ≤ µ and ∀x:A(1, X).h ◦ x ≤ x =⇒ µ ≤ x.
△

• ν:A(1, X) is a final co-algebra (aka greatest postfix-point) for h ⇐⇒
ν ≤ h ◦ ν and ∀x:A(1, X).x ≤ h ◦ x =⇒ x ≤ ν.
Remark 4.2. The terminology in Def 4.1 comes from Category Theory, in
particular from 2-categories, since posets are a degenerate form of categories.
Ordinary categories amount to a poset-enriched categories where the order on
A(X, Y ) is equality. If A is poset-enriched, then Aop denotes A with the direction
of arrows reversed, ie, Aop (X, Y ) = A(Y, X), and Aco denotes A with the order
on A(X, Y ) reversed, ie, Aco (X, Y ) = A(X, Y )op . Any notion in A has a dual
notion in Aop and a co-notion in Aco , in particular:
• f ⊣ g in A ⇐⇒ g ⊣ f in Aco .
• x initial algebra for h in A ⇐⇒ x final co-algebra for h in Aco .
The following facts are instances of more general results valid in 2-categories.
Proposition 4.3. In any poset-enriched category A:
1. If f ⊣ g, then g is uniquely determined by f , and when g exists it is
denoted by f R , and called the right adjoint to f .
2. If f :X → Y is an isomorphism, then f ⊣ f −1 .
Definition 4.4. The poset-enriched category Po is defined as follows:
• Objects X:Po are complete lattices, ie,
such that every
F posets (|X|, ≤X ) F
subset S of |X| has a sup, denoted as S. In paricular, ∅ is the least
element ⊥X of X.
• Arrows f :Po(X, Y ) are monotonic maps f :|X| → |Y |, ie,
∀x0 , x1 :|X|.x0 ≤X x1 =⇒ f (x0 ) ≤Y f (x1 ) (sups are irrelevant).
• The poset-enrichment f ≤ g:Po(X, Y ) is given by the point-wise order.
Remark 4.5. Po is cartesian closed in the enriched sense, ie, it has a terminal
object and the following poset isomorphisms natural in Z:
• Po(Z, X × Y ) ∼
= Po(Z, X) × Po(Z, Y ), where X × Y is the cartesian
product of the complete lattices X and Y .
• Po(Z, Y X ) ∼
= Po(Z × X, Y ), where Y X is the complete lattice Po(X, Y ).

13

Moreover, f ⊣ g in Po exactly when f and g form a Galois connection, ie:
∀x:|X|.∀y:|Y |.x ≤X g(y) ⇐⇒ f (x) ≤Y y.
Restricting the objects of Po to complete lattices allows to characterize the
arrows f :Po(X, Y ) that have right adjoints, and implies that every h:Po(X, X)
has an initial algebra and a final co-algebra (the proofs of Thm 3.3 and 3.8 make
systematic use of the universal property of initial algebras).
Proposition 4.6. Given a map f :Po(X, Y ) the following are equivalent:
F
F
• f preserves all sups, ie, f ( S) = (f S) when S ⊆ |X|.
F
• f has a right adjoint f R , namely, f R (y) = {x|f (x) ≤Y y}.
For a HS on S, the complete lattices X of interest should have as underlying
set a subset of P(S), but there are two choices for ≤X : inclusion ⊆; and reverse
inclusion ⊇. When ≤X is an information order, the correct choice is reverse
inclusion, since a smaller over-approximation is more informative.
Definition 4.7. Given a topological space S, define:
△

• P(S) = (P(S), ≤), complete lattice of subsets of S ordered by reverse inF
T
△
clusion, ie, U ≤ V ⇐⇒ U ⊇ V . Thus, S = S.
△

• C(S) = (C(S), ≤), complete lattice of closed subsets of S ordered by ≤.
△

• H(S) = P(S2 ) × P(S2 ), complete lattice of all HS on S.
△

• Hc (S) = C(S2 ) × C(S2 ), complete lattice of all closed HS on S.
Given a complete lattice X and x:|X|, the complete lattice X ↑ x is the set
{x′ |x ≤X x′ } ordered by ≤X . When X is one of the complete lattices from
Def 4.7, instead of X ↑ x, we write x in place of S, eg, P(S) stands for P(S) ↑ S
when S:P(S), and H(H) stands for H(S) ↑ H when H:H(S).
Proposition 4.8. In Po one has the following isomorphisms:
Y
X
Y
X
i:I.P(Si ) ∼
i:I.Si ),
i:I.C(Si ) ∼
i:I.Si ),
= P(
= C(
∼ P(S′ ) and
with isomorphism maps (Ai |i:I) 7→ {(i, a)|i:I ∧ a:Ai }. Thus, H(S) =
′
′
2
2
Hc (S) ∼
= 2 × S × S.
= C(S ), where S is the topological space S + S ∼
Given C:C(S), equivalently, a closed subspace of S, (1) below is a commuting
diagram in Po of sup-preserving maps, and (2) is the commuting diagram of
right adjoints to the maps in (1), where g(U ) = U ∩ C, and f R (U ) = U .
C(C)
✻

⊂

g
C(S)

f ✲ P(C)
✻

(1)
⊂

C(C) ✛f R
∩

gR

g

∩

(2)

❄
C(S) ✛ f R

f ✲ P(S)
14

P(C)
gR
❄
P(S)

P
Proof. By definition of sum S =
i:I.Si of topological spaces, a subset A of
S is closed exactly when each Ai = {a|(i, a):A} is a closed subset of Si .
The set C(S) of closed subsets of a topological space S is closed wrt intersections computed in P(S), thus the inclusion f preserves sups. Since C is closed,
g(U ) = U ∩ C is closed when U is closed.
✷
Definition 4.9. Given a Banach space S, we define the following maps in Po:
1. t:Po(H(S), H(R × S)) is the construction on HS in Def 2.9.
2. T:Po(H(S) × P(S), P(S)) is given by T(H, S) = {s′ |s ✲ s′ }.
H

3. Rf :Po(H(S) × P(S), P(S)) is the reachability map in Def 3.1.
4. Rs:Po(H(S) × C(S), C(S)) is the safe reachability map in Def 3.6.
5. S:Po(H(S), P(S)) is given by S(F, G) = {s|∃s′ .s F s′ ∨ s G s′ ∨ s′ G s}.
We call T(H):Po(P(S), P(S)) transition map of H and S(H):P(S) its support.
The transition map of H corresponds to the transition relation and suffices for
defining the maps Rf (H) and Rs(H). The support of H does not include the
values in the image of F , because they represent velocities, instead of states.
Proposition 4.10. Given a Banach space S, the following hold:
1. t(H) = t(H), for every H:H(S).
2. If H:Hc (S) and T(H, C) ⊆ C:C(S), then T:Po(H(H) × P(C), P(C)),
Rf :Po(H(H) × P(C), P(C)), and Rs:Po(H(H) × C(C), C(C)).
3. S(H) = Rf (H, S(H)), for every H:H(S).

4. S(H) = S(H) ≤ S(H) ≤ S(H):P(S), for every H:H(S).
5. If H is compact (therefore, closed), then S(H) is compact (therefore, closed).
Proof. See Appendix A.
f ✲
X in Po such that g ◦ f = idY , one can
⊥
✛ g
identify Y with its image in X. Then, the right adjoint g maps every x:X to
its best approximation in Y , ie, ∀y:Y.y ≤ x ⇐⇒ y ≤ g(x). Clearly a smaller Y
means that the g(x) are less accurate. In static analysis it is customary to take
as Y a finite lattice, in order to get decidablility. In the case of safe reachability
we take Y = C(S) in place of X = P(S). Also in this case there is a reduction
in cardinality: when S is a Banach space with the cardinality of the continuum,
C(S) has the cardinality of the continuuum, while P(S) has a bigger cardinality.

Given an adjunction Y

Definition 4.11. Given X = (|X|, ≤X ):Po and a subset F ⊆ |X|, define:
• |X|(F ) the smallest subset of |X| containing F and closed wrt sups in X;
• X(F ) the poset |X|(F ) ordered by ≤X ;
△ F
• ✷F (x) = {y:F |y ≤X x}:X(F ) the best approximation of x:X.
15

It is quite easy to establish the following basic properties.
Proposition 4.12. X(F ) is a complete lattice. Moreover:
F ⊆ |X|(F ) = |X|(|X|(F )).
F is finite =⇒ |X|(F ) is finite.
F1 ⊆ F2 =⇒ |X|(F1 ) ⊆ |X|(F2 ) and |X|(F1 ) = |X(F2 )|(F1 ).
The inclusion f :X(F ) ⊂ ✲ X is sup-preserving and f R (x) = ✷F (x).
f ✲
5. Y
X and F image of f =⇒ F = |X|(F ) and ✷F (x) = f (g(x)).
⊥
✛ g

1.
2.
3.
4.

Example 4.13. When Z is the complete lattice Po(X, Y ), there are several
subsets F of |Z| satisfying F = |Z|(F ) which consist of monotonic maps that
preserve certain types of sups. For instance:
1. strict maps, which preserve the sup of the empty set, ie, f (⊥) = ⊥.
F
F
2. additive maps, which preserve all sups, ie, f ( S) = f (S) for S ⊆ |X|.
3. Scott D-continuous maps, which preserve sups of directed subsets,
ie, non-empty D ⊆ |X| satisfying ∀x, y:D.∃z:D.x, y ≤X z.
4. Scott ω-continuous maps, which preserve sups of ω-chains, ie, sequences (xn |n:ω) such that ∀n.xn ≤ xn+1 .
The following implications always hold:
strict ⇐=== additive ===⇒ D-continuous ===⇒ ω-continuous.
Requirements can be combined, eg, by defining the strict D-continuous maps.
Proposition 4.14. The best D-continuous approximation f ✷ of f satisfies
✷
✷ ✷
✷
✷
✷
the properties: idX = id✷
X and (g ◦ f ) = g ◦ f ≤ (g ◦ f ) .
Proof. Like any best approximation ✷F (−) on Po(X, Y ), −✷ is monotonic
and satisfies (f ✷ )✷ = f ✷ ≤ f . The D-continuous maps form a sub-category of
Po, ie, they include identities and are closed wrt composition, thus id✷
X = idX
and (g ✷ ◦ f ✷ )✷ = g ✷ ◦ f ✷. Finally g ✷ ◦ f ✷ ≤ (g ◦ f )✷ follows from monotonicity
of composition and −✷ .
✷
4.1. Best Approximations on Continuous Lattices
Thm 4.20 gives a simple way to compute f ✷ of f :Po(X, Y ) when X is
a continuous lattice. Moreover, all continuous lattices for which we want to
compute f ✷ have a countable base, which implies that D- and ω-continuous
maps over these lattices coincide.
Remark 4.15. [Eda95] advocates the use of Domain Theory for the study of
dynamical systems. In this context, the complete lattice C(S) becomes relevant
when S is a compact metric space. In fact, under this assumption, C(S) is a

16

continuous lattice with a countable base (see [Eda95, Prop 3.4]).4 Thus, one can
address computability issues, and the Scott topology coincides with the Upper
topology (see [Eda95, Prop 3.2 and 3.3]).
We recall some basic notions and facts on continuous lattices. For more
details, the reader is referred to [GHK+ 03, AJ94].
Definition 4.16. Given two complete lattices X and Y , define:
△

• the way-below
relation: x ≪X x′ ⇐⇒ for any directed D ⊆ |X|, if
F
′
x ≤X D, then ∃d:D.x ≤X d.
△

′
′
′
• the subset ↓
↓x = {x|x ≪X x } of elements way-below x .
△

The step map [x, y]:Po(X, Y ) is [x, y](x′ ) = if (x ≪X x′ ) then y else ⊥Y .
Proposition 4.17. For any complete lattices X and Y , the following hold:
1.
2.
3.
4.

x′0 ≤X x0 ≪X x1 ≤X x′1 =⇒ x′0 ≪X x′1 .
x0 ≪X x1 =⇒ x0 ≤X x1 .
x0 , x1 ≪X x =⇒ x0 ⊔ x1 ≪X x and ⊥ ≪X x.
↓
↓x is directed.

F
△
Definition 4.18. A complete lattice X is continuous ⇐⇒ ∀x:X.x = ↓↓x. A
F
△
subset B ⊆ |X| is a base for X ⇐⇒ ∀x:X. B∩↓
↓x is directed and x = (B∩↓↓x).
Proposition 4.19. Given a continuous lattice X and a complete lattice Y :
F
1. D ⊆ |X| is directed and x ≪X D =⇒ ∃d:D.x ≪X d.
2. The step map [x, y]:Po(X, Y ) is D-continuous.
3. if X has a countable base, then f :Po(X, Y ) is ω-continuous =⇒ f is Dcontinuous.
Proof.
1. [GHK+ 03, Thm I-1.9].
2. [AJ94, Prop 4.0.1] and {x′ |x ≪X x′ } Scott open when X is continuous,
by the previous point.
3. [AJ94, Prop 2.2.14].
✷
The following theorem says that f ✷ :Po(X, Y ) is the sup of step maps when X
is a continuous lattice, and more specifically, f ✷ (x) is the sup of {f (b)|b ≪X x}.
F
Theorem 4.20. If f :Po(X, Y ) and B is a base for X, then f ✷ = b:B [b, f (b)].
4 There are some minor differences between our work and that of [Eda95], namely,
in [Eda95], U X is a hyperspace on the set of non-empty compact subsets of X, while our
C(S) is a complete lattice on the closed subsets of S. However, for compact Hausdorff spaces,
the only difference is given by the empty subset.

17

△ F
Proof. As X is a continuous lattice, the maps [b, f (b)] and f ′ = b:B [b, f (b)]
are D-continuous. We prove that for any given D-continuous map g ≤ f , we
F
△
have g ≤ f ′ ≤ f . For x:X, the subset B(x) = B∩↓↓x is directed and x = B(x).
Therefore:

• ∀b:B(x).g(b) ≤Y f (b) ≤Y f (x), since g ≤ f and ∀b:B(x).b ≤X x.
F
• g(x) = b:B(x) g(b) by continuity of g.
F
• f ′ (x) = b:B(x) f (b) by definition of f ′ .
Thus, one concludes that g(x) ≤Y f ′ (x) ≤Y f (x).

✷

5. Robustness
The safe reachability maps introduced in Def 3.6 and 4.9 are of the form
A:Po(C(S1 ), C(S2 )), with S1 and S2 metric spaces. We say that such an A is
robust at C when small extensions to C cause small extensions to A(C).
Definition 5.1 (Robustness). Given two metric spaces (Si , di ), i ∈ {1, 2}, we
△
say that a map A:Po(C(S1 ), C(S2 )) is robust ⇐⇒
∀C:C(S1 ).∀ǫ > 0.∃δ > 0.A(Cδ ) ⊆ A(C)ǫ ,
△

where Sδ :C(Si ) is the closure of the open subset B(S, δ) = {y|∃x:S.di (x, y) < δ}.
For discrete systems, robustness is not an issue (when the metric space S1 is
discrete every monotonic map is robust), while robustness of safe reachability
RsH :Po(C(S), C(S)) for a HS H on S is very sensitive to the HS, and restricting
to purely continuous systems does not help either (see Example 5.9).
The main result of this section is that robustness and D-continuity coincide
when the Si are compact metric spaces. In this case, an analysis A becomes
robust when replaced by its best D-continuous approximation. Remarkable
instances of A, for which the main result applies, are safe reachability maps
Rs:Po(Hc (H0 ) × C(S0 ), C(S0 )), where H0 is a compact HS on S with support
S0 and Hc (H0 ) is the complete lattice of closed hybrid systems that refine H0 ,
ie, H ≥ H0 :Hc (S).
In order to relate different properties of monotonic maps in Po(X, Y ), it is
conceptually useful to move to the category Top of topological spaces, by considering suitable topologies on the underlying sets |X| and |Y |. For a complete
lattice X, one can define two topologies on |X|: Alexandrov topology OA (X),
and Scott topology OS (X) ⊆ OA (X). The partial order ≤X can be recovered
as the specialization order of the two topologies. Thus, topologies are more
informative than partial orders: the Alexandrov continuous maps, ie, the maps
in Top(OA (X), OA (Y )), are the monotonic maps from X to Y , while the Scott
continuous maps Top(OS (X), OS (Y )) are the D-continuous maps from X to Y .
Furthermore, for robustness one can identify a suitable topology on C(S).
18

Definition 5.2 (Topologies). When S is a topological space and S:P(S), let
△
↑ S = {C:C(S)|S ≤ C}. We define three topologies on C(S):
△

• U Alexandrov open ⇐⇒ U is upward closed, ie, C:U =⇒ ↑ C ⊆ U .
F
△
• U Scott open ⇐⇒ U is upward closed and ( D):U =⇒ ∃C:D.C:U ,
for any directed subset D of closed subsets.
△

• U open in the Upper topology ⇐⇒ C:U =⇒ ∃O:O(S).C: ↑ O ⊆ U .
Moreover, when (S, d) is a metric space, we define a fourth topology on C(S):
△

• U open in the Robust topology ⇐⇒ C:U =⇒ ∃δ > 0. ↑ B(C, δ) ⊆ U .
Lemma 5.3. In a metric space (S, d), the following implications hold:
1.
2.
3.
4.

U
U
U
U

Scott open =⇒
open for the Robust topology =⇒
open for the Upper topology =⇒
Alexandrov open.

Proof. We exploit the following facts, which are valid in any metric space:
(F1) B(B(S, δ), δ ′ ) ⊆ B(S, δ + δ ′ ).
(F2) S ⊆ S = ∩δ>0 B(S, δ).
△

(F3) B(S, δ) ⊆ Sδ = B(S, δ) ⊆ B(S, δ ′ ) whenever δ < δ ′ .
Now we prove the implications:
△

• (1) =⇒ (2). If U is Scott open and C:U , let On = B(C, 2−n ), we prove
that ↑ On ⊆ U for some n.
△

Let Cn = On . Then, Cn ⊇ On ⊇ Cn+1 , and C = C = (∩n Cn ):U . Thus,
Cn :U , for some n.
Since On ⊆ Cn :U and U is upward closed, then ↑ On ⊆ U .
• (2) =⇒ (3). If U is open in the Robust topology and C:U , by definition,
there exists a δ > 0 for which ↑ B(C, δ) ⊆ U . Then, B(C, δ) is the open
subset that witnesses that U is open in the Upper topology.
• (3) =⇒ (4). If U is open in the Upper topology, then U is the union of
upward closed subsets of the form ↑ O, therefore it is Alexandrov open. ✷
As anticipated, the Robust topology captures the robustness property:
Theorem 5.4. Given two metric spaces (Si , di ), and a map A:Set(C(S1 ), C(S2 )),
the following properties are equivalent:
1. A is monotonic and robust in the sense of Def 5.1.
19

2. A is continuous wrt the Robust topologies.
Proof. See Appendix A.
Lemma 5.5. We have the following inclusions among topologies on C(S):
1. The Upper topology is included in the Scott topology, when S is compact.
2. The Alexandrov topology is included in the Robust topology, when S is a
discrete metric space (eg, d(x, y) = 1 when x 6= y).
Proof. When S is a compact topological space, any closed subset of S is compact. To prove that the Upper topology is included in the Scott topology, it suffices to show that for any open subset O of S, the subset ↑ O of C(S) is Scott open.
Clearly ↑ O is upward closed. Now, let C be the complement of O. If {Ki |i:I}
is an I-indexed directed set of closed subsets such that K = (∩i:I Ki ) ⊆ O,
then Ki′ = Ki ∩ C is another I-indexed directed subset D′ of closed subsets
whose intersection is ∅. Since compact subsets (therefore, also the closed subsets) have the finite intersection property and D′ is directed, some Ki′ must be
∅, or equivalently, Ki : ↑ O.
If (S, d) is discrete, then S = S = B(S, 1), as all subsets are both open and
closed. Therefore, when U is Alexandrov open, ie, U is the union of all ↑ C with
C:U , it is also open in the Robust topology, because ↑ C =↑ B(C, 1).
✷
Remark 5.6. The Robust topology depends on the metric d, while the other
topologies on C(S) are definable for any topological space S. There are metric
spaces (S, d) where the four topologies on C(S) differ. For instance, in the
space S = {x|x > 0} of positive reals with the usual metric d(x, y) = |y − x|,
△
△
let xn = 2−n and δn = xn+1 . Then, C = {xn |n:ω} is a closed subset of S,
O = ∪n B(xn , δn ) is an open subset of S, and the following counter-examples
show that the four topologies differ:
• ↑ C is Alexandrov open, but it is not open in the other topologies.
• ↑ O is open in the Upper topology, but it is not open in the Robust
topology, because C: ↑ O but there is no δ > 0 such that B(C, δ) ⊆ O,
because (0, δ) ⊆ B(C, δ) but (0, δ) 6⊆ O.
• ↑ ∅ = {∅} is open in the Robust topology, because B(∅, δ) = ∅, but it is not
Scott open, because Cn = {x|x ≥ 2n } is an ω-chain of closed non-empty
subsets of S whose intersection is ∅.
In finite dimensional Banach spaces like Rn , the compact subsets are exactly
the closed subsets C that are bounded, ie, C ⊂ B(0, δ) for some δ > 0. On
the contrary, in infinite dimensional Banach spaces (under the strong topology)
they form a proper subset of the closed bounded ones. For instance, neither the
closure nor the boundary of a ball B(0, δ) is compact.
Theorem 5.7. Given a map A:Po(C(S1 ), C(S2 )), with S1 and S2 metric spaces:
20

1. If S1 and S2 are compact, then, A is robust ⇐⇒ A is Scott continuous.
2. If S1 and S2 are discrete, then, A is robust.
Proof. We use Lemma 5.3 and 5.5:
1. If Si is a compact metric space, the Upper and Scott topologies on C(Si )
coincide. The result follows as the Robust topology is between the two.
2. If Si is a discrete metric space, the Alexandrov and Robust topologies on
C(Si ) coincide. The result follows as every the monotonic map is Alexandrov continuous.
✷
Remark 5.8. Theorem 5.7 says that for discrete metric spaces robustness is
not an interesting notion, because every monotonic map A:Po(C(S1 ), C(S2 )) is
robust, and moreover C(Si ) = P(Si ). When the metric spaces are compact, there
is a best robust approximation of A given by A✷ . In all other cases robustness
is an interesting property, but there is no best way to approximate A with a
robust map, because the subset of robust maps is not closed wrt arbitrary sups
computed in Po(C(S1 ), C(S2 )).
Example 5.9. We give an example of a compact HS H with support C, whose
safe reachability map RsH :Po(C(C), C(C)) is not robust.
Let H be HE of Example 2.6—which can only flow—and let C = [0, M ].
Since C is compact, robustness is equivalent to Scott continuity. Consider the
ω-chain (In |n) with In = [0, M/2n ], whose sup is the singleton {0}. Then:
RsH ({0}) = {0}.

RsH (In ) = [0, M ],

Thus, RsH does not preserve the sup of the ω-chain (In |n). Consider its best
Scott continuous approximation Rs✷
H (see Thm 4.14), which is given by:
• Rs✷
H (∅) = ∅.
• Rs✷
H (U ) = [m, M ] with m = min(U ), when U 6= ∅ is compact.
Then, RsH ({0}) = {0} ⊂ [0, M ] = Rs✷
H ({0}).
6. Figures and Examples
We go through the hybrid systems introduced in Sec 2 and for each of them
we compare the sets computed by different analyses. More precisely, given a
HS H on S and a state s0 in the support S(H) of H, take as set of initial states
I = {s0 }, then define four subsets Sf ⊆ Ss ⊆ Sr ⊆ SR of S:
△

• Sf = Rf H (I) set of states reachable in finitely many transition.
△

• Ss = RsH (I) safe approximation of the set of states reachable in finite
time. One should use I in place of I, but a singleton is already closed.

21

M

M

m0

t

t

m0

0

0
(a) m0 > 0

(b) m0 = 0

Figure 1: Trajectories and reachable states of HE (Expand). In each case the set of states
reachable from I = {m0 } is on the left of the trajectory starting from m0 .

To define Sr one must restrict RsH to a map in Po(C(S0 ), C(S0 )), where
S0 is a sufficiently large compact subset of S. When H is compact, the
canonical choice for S0 is S(H).
△

• Sr = Rs✷
H (I) approximation of Ss robust wrt perturbations to I.
To define SR one must restrict Rs to a map in Po(Hc (H0 )×C(S0 ), C(S0 )),
where H0 is a sufficiently large compact HS on S and S0 = S(H0 ). There
is no canonical choice. H0 must capture the allowed perturbations to H,
thus H0 ≤ H in Hc (S), where H is the closure of H.
△

△

✷
(I) robust wrt perturbations
• SR = Rs✷ (H, I) approximation of Sr′ = RsH
to H & I allowed by H0 .

In Figures we adopt the following color coding for states and trajectories:
• a bullet

indicates the initial state s0

• blue - Sf and the part of a trajectory reachable in finitely many transitions
• green - Ss − Sf and the rest of a trajectory not reachable in finitely many
transitions, like Zeno points and beyond
• red - Sr − Ss , there is no analogue for a trajectory starting from s0 .
6.1. Expand
HE of Example 2.6 is a compact deterministic HS on R, whose behavior is
depicted in Fig 1. The canonical choice for S0 is the interval [0, M ]. For H0 we
take F0 = S0 × [−M, M ] and G0 = ∅, whose support is still S0 .
• Sf = Ss = Sr = SR = [m0 , M ] when 0 < m0 ≤ M
• Sf = Ss = [0] ⊂ [0, M ] = Sr = SR when 0 = m0 .
We now explain why making the set of reachable states robust wrt perturbations
to H does not make a difference in the case 0 < m0 ≤ M . To approximate SR
we take a small δ > 0 and define Iδ ≪ I in C(S0 ) and Hδ ≪ H in Hc (H0 ).
Let Iδ = [m0 − δ, M ] and Fδ = {(m, ṁ)|0 ≤ m ≤ M ∧ m − δ ≤ ṁ ≤ M }. By
taking 2 ∗ δ < m0 we can ensure that Fδ (m) ⊂ (0, M ] for any m:Iδ , therefore
SR = Rs✷ (H, I) ⊆ Rs(Hδ , Iδ ) = [m0 − δ, M ] → Sr when δ → 0.
22

6.2. Decay
HD of Example 2.7 is a deterministic HS on R, whose behavior is depicted
in Fig 2. Its closure is compact but it is no longer deterministic. The canonical
choice for S0 is the interval [0, M ]. For H0 we take F0 = S0 × [−M, M ] and
G0 = S0 × S0 , whose support is still S0 .
M

M

m0
t

t

m0

0

0
(a) m0 > 0

(b) m0 = 0

Figure 2: Trajectories and reachable states of HD (Decay). In each case the set of states
reachable from I = {m0 } is on the left of the trajectory starting from m0 .

• Sf = (0, m0 ] ⊂ [0, M ] = Ss = Sr = SR when 0 < m0 ≤ M
• Sf = Ss = Sr = SR = [0, M ] when 0 = m0 .
Ss = Sr = SR = S0 , because Ss = S0 and these subsets cannot be bigger than
the support of H0 . This result does not change, when H0 is replaced with a HS
with a bigger support, but the proof is not as simple (see Sec 6.1).
6.3. Bouncing Ball
HB of Example 2.8 is a deterministic HS on R2 , its behavior depends on
the coefficient of restitution b (see Fig 3). The closure of HB is not compact
and its support is the closed subset {(h, v)|0 ≥ h}. However, compactness is
irrelevant to define and compare Sf and Ss . Let s0 = (0, v0 ) with 0 < v0 < V
△
and S(u) = {(h, v)|0 ≥ h ∧ E(h, v) = E(0, u)} be the set of states whose energy
2
E(h, v) = h + v2 is exactly E(0, u), then the sets Sf and Ss are (see Fig 4):
S
1. Sf = Ss = n S(bn v0 ) when b < −1
2. Sf = S
Ss = S(v0 ) when b = −1 (elastic
bounce)
S
3. Sf = n S(bn v0 ) ⊂ Sf ∪ S(0) ∪ ( n S(bn V )) = Ss when −1 < b < 0
4. Sf = Ss = S(v0 ) ∪ S(0) ∪ S(V ) when b = 0 (inelastic bounce)
5. Sf = S(v0 ) ∪ S ′ (b, v0 ) ⊂ Sf ∪ S(0) ∪ S(V ) ∪ S ′ (b, V ) = Ss when 0 < b < 1,
△
with S ′ (b, u) = {(0, −bnu)|0 ≤ n} sequence of instantaneous slowdowns
6. Sf = Ss = S(v0 ) when b = 1
7. Sf = Ss = S(v0 ) ∪ S ′ (b, v0 ) when 1 < b, now S ′ (b, u) is a sequence of
instantaneous accelerations.
To make HB compact, the simplest is to put an upper bound to the energy of
the system, say E0 = E(0, V0 ) with V0 > V , and allow only b st |b| ≤ 1, so that
the energy cannot increase when the ball bounces. So we replace HB with the
following compact HS H, whose support is S0 = {(h, v)|0 ≤ h ∧ E(h, v) ≤ E0 }
23

h

0

h

t

0

0 2 4 6 8
v

h

t

0

0 2 4 6 8

t
0 2 4 6 8

v

−bv0
v0

V
v0

t

(a) b < −1

h

0

v

(b) b = −1

t

t

0

0 2 4 6 8

0

v

V
v0

t

h

V
t v0

(c) −1 < b < 0

2

4

v
V
v0

t

(d) b = 0

t

(e) 0 < b < 1

Figure 3: Trajectories of HB (Bouncing ball). All trajectories start from (h = 0, v = v0 ).
bV

h

h

−bV

−bv0
−bV

v
v0 V

v
−v0

v0

(a) b < −1

−V−v0

(b) −1 < b < 0

−bv0

h

−bV

−V−v0

v
v0 V

(c) 0 < b < 1

Figure 4: Set of reachable states of HB (Bouncing ball). The set I is always {(h = 0, v = v0 )}.
In case (a) there is an expanding sequence of parabolas (−b)n v0 → +∞. In case (b) there are
two shrinking sequences of parabolas (−b)n v0 → 0 and (−b)n V → 0.

• F = {((h, v), (ḣ, v̇))|(h, v):S0 ∧ ḣ = v ∧ v̇ = −1}
• G = {((0, v), (0, v + ))|0 ≤ −v ≤ V0 ∧ v + = b ∗ v} ⊎ {((0, 0), (0, V ))}.
To define SR we fix a compact HS H0 with support S0 . The simplest choice is
to take F0 = F and replace G with a G0 independent from b, namely
• G0 = {((0, v), (0, v + ))|0 ≤ −v ≤ V0 ∧ |v + | ≤ −v} ⊎ {((0, 0), (0, V ))}.
The relations among Ss , Sr and SR , when |b| ≤ 1 and 0 < v0 < V < V0 , are
S
1. Ss = Sr = S(v0 ) ⊂ {S(v)|v:[0, V ]} = SR when b = −1 (elastic bounce)
S
S
2. Sf = Sr = SR = n S(bn v0 ) ∪ S(0) ∪ ( n S(bn V )) when −1 < b < 0
3. Ss = Sr = SR = S(v0 ) ∪ S(0) ∪ S(V ) when b = 0 (inelastic bounce)
4. Ss = Sr = SR = S(v0 ) ∪ S ′ (b, v0 ) ∪ S(0) ∪ S(V ) ∪ S ′ (b, V ) when 0 < b < 1
5. Ss = Sr = S(v0 ) ⊂ S(v0 ) ∪ S(V ) ∪ {(0, v)| − v:[0, V ]} = SR when b = 1.
There is an informal explanation for SR in the case b = −1 (elastic bounce).
After each bounce the ball may lose a bit of energy, thus after sufficiently many
bounces it may stop (minimum energy). After a kick the energy will reach the
maximum value allowed, and then it may decrease again after each bounce.
Thus any level of energy in [0, E(0, V )] is reachable, assuming 0 < v0 < V .
24

More formally we define Hδ ≪ H in Hc (H0 ) st Hδ → H when δ → 0. Since H0
allows only perturbations in G, we define Gδ (for δ > 0) as
{((0, v), (0, v + ))|0 ≤ −v ≤ V0 ∧ |v + | ≤ −v ∧ −v − δ ≤ v + } ⊎ {((0, 0), (0, V ))}
When −v is small, ie 0 ≤ −v ≤ δ ≤ V , |v + | ≤ −v and the energy is ≤
2
Otherwise, 0 < δ < −v, v + :[−v − δ, −v] and the energy loss is ≤ V δ − δ2 .

δ2
2 .

Remark 6.1. It is important what H0 is chosen to capture the hard constrains
on the HS H of interest, because it can affect how SR is computed. For instance,
for the bouncing ball one may replace H0 with a more relaxed H0′
• G′0 = {((0, v), (0, v + ))|0 ≤ −v ≤ V0 ∧ |v + | ≤ V0 } ⊎ {((0, 0), (0, V ))}
H0′ has the same support of H0 , but H0′ < H0 , because after a bounce the ball
can increase its energy as far as it stays below the upper bound E(0, V0 ). This
change results in a bigger subset SR when |b| = 1, namely
• S0 = SR when b = −1, ie any state in the support of H is reachable
because of the more permissive perturbations
• S(v0 ) ∪ S(V ) ∪ {(0, v)| − v:[0, V0 ]} = SR when b = 1.
Conclusions and Future Work
The main contributions of this paper concern reachability analysis in the
context of hybrid (and continuous) systems.
Firstly, we have proposed safe reachability RsH (I), which computes an overapproximation of the set of states reachable in finite time from the set I of
initial states by the hybrid system H, and compared it with the more naive
reachability Rf H (I), which computes only an under-approximation.
Secondly, and more importantly, we have addressed the issue of robustness
of an analysis A cast as a monotonic map A:Po(X, Y ) between complete lattices
X and Y of a particular form (ie, hyperspaces of metric spaces). Robustness of
A means that A(xδ ) → A(x) as δ → 0, where xδ is a small perturbation of x
depending on a δ > 0, which measures the level of inaccuracy. In some cases (ie,
when the metric spaces are compact) robustness amounts to Scott continuity,
and one can exploit the following facts:
• Every monotonic map A:Po(X, Y ) between complete lattices has a best
Scott continuous approximation A✷ ≤ A:Po(X, Y ).
• When X is a continuous lattice, A✷ (x) is the sup of {A(b)|b ≪X x}, ie, it
is computed by applying A to way-below approximations of x.
While the importance of safe/sound analyses is widely recognized, the issue of
robustness is mostly overlooked (one reason being that for discrete systems it is
not an issue). In our view, robustness has at least two immediate implications:
25

Modeling languages. There should be syntactic support to distinguish between hard and soft constraints on a hybrid system H. Hard constraints
must be satisfied also by small perturbations Hδ . Thus, they identify the
complete lattice (hyperspace) X where H is placed, while soft constraints
provide the additional information to identify H uniquely within X. The
distinction would be needed by tools that implement a robust analysis and
can be ignored by other tools. In [GKC13] there is no explicit annotation
for soft constraints, instead there is a re-interpretation of logical formula,
which injects δ-noise in specific sub-formulas.
Finite model checking. Counterexample-guided Abstraction & Refinement
(CEGAR) is a general way of analyzing a system H with an infinite state
space by leveraging finite model checking tools (see [CGJ+ 00, CFH+ 03]).
In the setting of abstract interpretation, CEGAR amounts to approximating an analysis A:Po(X, X) with finite analyses A′ :Po(Xf , Xf ), ie:
X
✻

A

γ

≤

∪

Xf

✲ X
✻
γ

γ sub-lattice inclusion

∪

A′

✲ Xf

Xf finite (complete) lattice

Whenever Xf is fixed, there is a best approximation Af :Po(Xf , Xf ) of A
△
given by Af = γ R ◦ A ◦ γ.

If H is a HS on S = Rn and its support is included in a compact subset K,
then there are three reachability analyses Rs✷
H ≤ RsH ≤ Rf H :Po(X, X),
where X = C(K) is a continuous lattice with a countable base, but uncountably many elements (unless K is finite). One may wonder whether
replacing X with a finite sub-lattice Xf would make the three analyses
indistinguishable: the answer is no (counterexamples can be given using
HE and HD in Examples 2.6 and 2.7).
However, there is a way to turn a finite approximation A′ :Po(Xf , Xf ) of
A:Po(X, X) into a finite approximation A′′ of A✷ , provided that X is a
△
continuous lattice, namely, A′′ (x) = A′ (xb ) where xb is the biggest element
in Xf such that γ(b) ≪X γ(x).

As future work we plan to address computability issues. More specifically,
given a compact HS H0 on S with support S0 , is Rs✷ :Po(Hc (H0 )×C(S0 ), C(S0 ))
computable? When S has a countable dense subset, all continuous lattices
involved have a countable base, and the question can be formulated in a wellestablished setting. In [EP07] the authors study computability of the evolution
map for a compact and continuous flow automaton (ccFA for short). In our
setting, a ccFA is a tuple (C, f, G, I), with C a compact subset of Rn called
invariant, f :Top(C, Rn ) the flow function, G:C(C × C) the jump relation, and
I:C(C) the set of initial states. The graph of f is flow relation f :C(C × V ), with
26

V = f (C). Therefore, (f, G) is a compact HS on Rn with support included in
the compact subset K = C ∪ V .
The main contributions in [EP07] are: the definition of the denotational
semantics [[(C, f, G, I)]]:Top(T, C(C)) ∼
= C(T × C) of a ccFA (C, f, G, I), which
is computable for effectively given ccFA (cf. [EP07, Thm 38]); and computational
adequacy, ie [[C, f, G, I]] = Ef (f,G) (I), for separated ccFA (cf. [EP07, Thm 25]).
Most of the steps in defining the denotational semantics of a ccFA use Scott
continuous maps, but for the lack of a continuous lattice/domain of ccFA. It
would be interesting to see if their denotational semantics extends to compact
HS, giving a Scott continuous computable map [[−]]:Po(Hc (H0 ) × C(S0 ), C(S0 )),
and then compare it with the map Rs✷ between the same lattices.
References
[ACH+ 95] Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A
Henzinger, P-H Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis,
and Sergio Yovine. The algorithmic analysis of hybrid systems. Theoretical computer science, 138(1):3–34, 1995.
[AJ94] S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M.
Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3, pages 1–168. Clarendon Press, Oxford,
1994.
[CC92] Patrick Cousot and Radhia Cousot. Abstract interpretation frameworks. Journal of logic and computation, 2(4):511–547, 1992.
[CFH+ 03] Edmund Clarke, Ansgar Fehnker, Zhi Han, Bruce Krogh, Olaf Stursberg, and Michael Theobald. Verification of hybrid systems based
on counterexample-guided abstraction refinement. In TACAS, volume 3, pages 192–207. Springer, 2003.
[CGJ+ 00] Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In Computer aided verification, pages 154–169. Springer, 2000.
[Con90] John B. Conway. A Course in Functional Analysis. Springer, 2nd
edition edition, 1990.
[CR04] Pieter Jan Laurens Cuijpers and Michel Adriaan Reniers. Topological (bi-) simulation. Electronic Notes in Theoretical Computer
Science, 100:49–64, 2004.
[Cui07] Pieter J. L. Cuijpers. On bicontinuous bisimulation and the preservation of stability. In Alberto Bemporad, Antonio Bicchi, and Giorgio Buttazzo, editors, Hybrid Systems: Computation and Control,
volume 4416 of Lecture Notes in Computer Science, pages 676–679.
Springer, 2007.
27

[Dur16] Adam Duracz. Rigorous Simulation: Its Theory and Applications.
PhD thesis, Halmstad University Press, 2016.
[Eda95] Abbas Edalat. Dynamical systems, measures and fractals via domain
theory. Information and Computation, 120(1):32–48, July 1995.
[EP07] Abbas Edalat and Dirk Pattinson. Denotational semantics of hybrid automata. The Journal of Logic and Algebraic Programming,
73(1):3–21, 2007.
[Frä99] Martin Fränzle. Analysis of hybrid systems: An ounce of realism can
save an infinity of states. In Computer Science Logic, pages 126–139.
Springer, 1999.
[GHK+ 03] G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. W. Mislove,
and D. S. Scott. Continuous Lattices and Domains, volume 93 of
Encycloedia of Mathematics and its Applications. Cambridge University Press, 2003.
[GKC13] Sicun Gao, Soonho Kong, and Edmund M Clarke. Delta-complete
reachability analysis (part 1). Technical report, Carnegie-Mellon
Univ. School of Computer Science, 2013.
[GST09] Rafal Goebel, Ricardo G Sanfelice, and A Teel. Hybrid dynamical
systems. Control Systems, IEEE, 29(2):28–93, 2009.
[Kel75] John L Kelley. General topology. Springer, 1975.
[Kel82] Gregory Maxwell Kelly. Basic concepts of enriched category theory.
Number 64 in Lecture Notes in Mathematics. CUP Archive, 1982.
[Pla08] André Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41(2):143–189, 2008.

28

Appendix A. Proofs
Proof (of Thm 3.3). Ef (I) and Rf (I) are the least prefix-points of some
monotonic maps on complete lattices of the form (P(S), ⊆). Thus, we can exploit the universal property of the least prefix-point X for a monotonic map F ,
ie, F (Y ) ≤ Y =⇒ X ≤ Y .
1. Consider the monotonic maps F and FI on P(T × S):
△

F (S) = {(t + d, s′ )|∃s.(t, s):S ∧ s

✲ s′ },

d

△

FI (S) = ({0} × I) ∪ F (S).

Ef (I) is the least prefix-point of FI . Since FI0 (S) ⊆ FI1 (S) when I0 ⊆ I1 ,
a prefix-point for FI1 is also a prefix-point for FI0 . Hence, we conclude
that Ef (I0 ) ⊆ Ef (I1 ).
Since I ⊆ ∪K when I:K, then Ef (I) ⊆ Ef (∪K). Now, let U = {Ef (I)|I:K}.
To prove Ef (∪K) ⊆ ∪U , observe that:
• F preserves unions, thus F (∪U ) = ∪{F (S)|S:U };
• ∀S:U.F (S) ⊆ S, thus F (∪U ) = ∪U ;

• ∀I:K.∃S:U.{0} × I ⊆ S, thus {0} × (∪K) ⊆ ∪U .

Therefore, ∪U is a prefix-point for F∪K .
2. Consider the monotonic maps G and GI on P(S):
△

G(S) = {s′ |∃s:S.s

✲ s′ },

△

GI (S) = I ∪ G(S).

Rf (I) is the least prefix-point of GI . By analogy with the previous point,
one can prove that Rf is monotonic and preserves unions.
Let S be a prefix-point of GI , ie, GI (S) ⊆ S. Then:
• I ⊆ S, because I ⊆ GI (S).

• GS (S) ⊆ S, because G(S) ⊆ GI (S) and GS (S) = S ∪ G(S).

By taking S = Rf (I), we conclude I ⊆ Rf (I) ⊆ Rf (Rf (I)) ⊆ Rf (I).
To prove π(Ef (I)) = Rf (I), observe that:
• ∀E:P(T × S).π(FI (E)) = GI (π(E)). Hence, π(Ef (I)) ⊇ Rf (I).

• ∀S:P(S).GI (S) ⊆ S =⇒ FI (T × S) ⊆ T × S.

Therefore, Ef (I) ⊆ T × Rf (I), and consequently, π(Ef (I)) ⊆ Rf (I).
3. Consider the monotonic maps FI on P(T×S), GI on P(S), GtJ on P(R×S),
whose least prefix-points are Ef H (I), Rf H (I), and Rf t(H) (J), respectively.
✲ (t + d, s′ ) ⇐⇒ 0 ≤ d ∧ s d✲ s′ , by Prop 2.10, these
Since (t, s)
H

t(H)

maps are related as follows:

• ∀E:P(T × S).FI (E) = Gt{0}×I (E), so Ef H (I) = (Rf t(H) ({0} × I).

• ∀S:P(R × S).π(GtJ (S)) = Gπ(J) (π(S)), so π(Rf t(H) (J)) ⊇ Rf H (π(J)).

• ∀S:P(S).Gπ(J) (S) ⊆ S =⇒ GtJ (R × S) ⊆ R × S.
29

As a result, Rf t(H) (J) ⊆ R × Rf H (π(J)), and π(Rf t(H) (J)) ⊆ Rf H (π(J)).
✷
Proof (of Thm 3.8). Es(I) and Rs(I) are defined as least prefix-points of
monotonic maps on complete lattices of the form (C(S), ⊆), C(S) is closed wrt
arbitrary intersections and finite unions computed in P(S), and the monotonic
map S 7→ S from P(S) to C(S) preserves finite unions.

1. Es(I) is the least prefix-point of a monotonic map FI′ on C(T × S) given
by:
d
△
F ′ (S) = ({0} × I) ∪ {(t + d, s′ )|∃s.(t, s):S ∧ s ✲ s′ },
I

and the properties of Es are proved similar to those of Ef , except for the
need to restrict to finite unions.
2. Rs(I) is the least prefix-point of a monotonic map G′I on C(S) given by:
△

G′I (S) = I ∪ {s′ |∃s:S.s

✲ s′ },

and the properties of Rs are proved by analogy with those of Rf . In
particular, π(Es(I)) ⊆ Rs(I) follows from:
∀S:C(S).G′I (S) ⊆ S =⇒ FI′ (T × S) ⊆ T × S.
As a result, Es(I) ⊆ T × Rs(I), and consequently π(Es(I)) ⊆ Rs(I).
3. If I:P(S) and S:P(T × S), then I ⊆ I:C(S) and FI (S) ⊆ FI′ (S):C(T × S).
Hence, Ef (I) ⊆ Es(I):C(T × S), and consequently Ef (I) ⊆ Es(I).
The inclusion Rf (I) ⊆ Rs(I) follows from Ef (I) ⊆ Es(I), since:
• Rf (I) = π(Ef (I)), by Thm 3.3.

• π(Es(I)) ⊆ Rs(I), by the previous point.

4. Consider the monotonic maps FI′ on C(T × S), G′I on C(S), and GtJ on
C(R × S), whose least prefix-points are EsH (I), RsH (I) and Rst(H) (J),
✲ (t + d, s′ ) ⇐⇒ 0 ≤ d ∧ s d✲ s′ , by
respectively. Since (t, s)
t(H)

Prop 2.10, these maps are related as follows:

H

• ∀E:C(T × S).FI′ (E) = Gt{0}×I (E), so EsH (I) = (Rst(H) ({0} × I).
′
• ∀S:C(S).Gπ(J)
(S) ⊆ S =⇒ GtJ (R × S) ⊆ R × S.

Hence, Rst(H) (J) ⊆ R × RsH (π(J)), and π(Rst(H) (J)) ⊆ RsH (π(J)).

✷

Proof (of Thm 4.10). A Banach space is a metric space, and one can rely
on characterizations of topological notions or exploit properties that are specific
to metric spaces, eg, x:U ⇐⇒ x is the limit of a sequence (xn |n:ω) in U .
1. t(F, G) = (F ′ , G′ ), where F ′ = C1 ×F and G′ = C2 ×G with C1 = R×{1}
and C2 = {(t, t)|t:R}, modulo the isomorphism (R × S)2 ✛ R2 × S2 . C1
and C2 are closed subsets of R2 . Thus, F ′ = C1 × F and G′ = C2 × G, ie,
t(H) = t(H).
30

2. T(H, C) ⊆ C means that C ≤ T(H, C). Hence, C ≤ T(H, C) ≤ T(H′ , S ′ )
when H ≤ H′ and C ≤ S ′ , because T is monotonic.
For Rf and Rs one can proceed as above, by observing that T(H, C) ⊆ C
✲ ”, and therefore
means “C is closed wrt the transition relation
H

C ⊆ Rf (H, C) ⊆ Rs(H, C) ⊆ C, by the assumptions on C and by definition
of Rf (H, C) and Rs(H, C).
✲ :
3. We prove that S(H) is closed under the transition relation
✲ s′ , then s G s′ . Therefore, s′ :S(H) ⊆ S(H).

H

0

• If s

H

• If s

H

✲ s′ with d > 0, then there exists f :Top([0, d], S) such that

d

f (0, d) ⊆ S(H) and s′ = f (d). Hence, s′ :S(H), because f is continuous.

4. It should be clear that S(H) ≤ S(H), S(H) ≤ S(H):P(S), as the maps S
and f R (U ) = U are monotonic. To prove S(H) = S(H), it suffices to show
that S(H) ≤ S(H), since U = U .
• H = F + G = F + G. Therefore, s:S(H) ⇐⇒
∃x.(x:F ∧ s = π1 (x)) ∨ (x:G ∧ s = π1 (x)) ∨ (x:G ∧ s = π2 (x)).

• Assume wlog that x:F ∧ s = π1 (x), we have to show that s:S(H).

• x:F implies that there exists a sequence (xn |n:ω) in F with limit x.

• Let sn = π1 (xn ). Then (sn |n:ω) is a sequence in S(H) with limit s,
because π1 is continuous. Thus, s:S(H).
5. S(H) is the union π1 (F ) ∪ π1 (G) ∪ π2 (G), and projections πi :S × S ✲ S
are continuous maps. The image of a compact set along a continuous
map is always compact. Therefore, if H is compact—ie, F and G are
compact—then S(H) is compact, because it is the union of three compact
subsets. Moreover, in metric spaces compact subsets are always closed. ✷
Proof (of Thm 5.4). We exploit the facts (F1-F3) in the proof of Lemma 5.3.
(1) =⇒ (2). Given U2 ⊆ C(S2 ) open (for the Robust topology), we have to
△
prove that U1 = A−1 (U2 ) ⊆ C(S1 ) is open. U1 is upward closed, because U2 is
upward closed and A is monotonic. If C:U1 , ie, A(C):U2 , we have to find δ > 0
such that↑ B(C, δ) ⊆ U1 , ie, C ′ ⊆ B(C, δ) =⇒ A(C ′ ):U2 :
• A(C):U2 and U2 open imply that ↑ B(A(C), δ ′ ) ⊆ U2 for some δ ′ > 0.
• Now, let ǫ be in (0, δ ′ ). By (F3), we get A(C)ǫ ⊆ B(A(C), δ ′ ).
• By robustness of A, there exists δ > 0 such that A(Cδ ) ⊆ A(C)ǫ .
• By monotonicity of A, we have A(C ′ ) ⊆ B(A(C), δ ′ ), ie, A(C ′ ):U2 , when
C ′ ⊆ B(C, δ) ⊆ Cδ .

31

(2) =⇒ (1). The Robust topology on C(Si ) is between Scott and Alexandrov
topologies, which have the same specialization order, ie, reverse inclusion. Thus,
A is monotonic wrt the specialization orders, because it is continuous wrt the
Robust topologies.
△
For C:C(S1 ) and ǫ > 0, let U2 = {C ′ :C(S2 )|∃ǫ′ > 0.B(C ′ , ǫ′ ) ⊆ B(A(C), ǫ)}.
Clearly A(C):U2 ⊆↑ B(A(C), ǫ) ⊆↑ A(C)ǫ . We prove that U2 is open for the
Robust topology, ie, ∀C ′ :U2 .∃δ > 0. ↑ B(C ′ , δ) ⊆ U2 :
• C ′ :U2 implies B(C ′ , ǫ′ ) ⊆ B(A(C), ǫ) for some ǫ′ > 0.
• By (F1), B(B(C ′ , δ), δ) ⊆ B(C ′ , ǫ′ ), where δ = ǫ′ /2.
• Therefore, ↑ B(C ′ , δ) ⊆ U2 .
△

U1 = A−1 (U2 ) is open in the Robust topology, because U2 is open and A is
continuous. But C:U1 . Therefore, there exists δ ′ > 0 such that ↑ B(C, δ ′ ) ⊆ U1 .
If δ is in (0, δ ′ ), then (F3) implies that Cδ ⊆ B(C, δ ′ ). Hence, Cδ :U1 and
A(Cδ ):U2 ⊆↑ A(C)ǫ , which means that A(Cδ ) ⊆ A(C)ǫ .
✷

32

