# Noncompact surfaces, triangulations and rigidity

Stephen C. Power  Dept. Math. Stats.
Lancaster University
Lancaster LA1 4YF
U.K<EMAIL_ADDRESS>
###### Abstract.

Every noncompact surface is shown to have a (3,6)-tight triangulation and a
characterisation of such triangulations is given in terms of length
constraints on the boundary walks of superfaces of a given genus. Applications
are given to the generic rigidity of associated countable bar-joint frameworks
in ${\mathbb{R}}^{3}$. In particular, every noncompact surface has a
(3,6)-tight triangulation that is minimally 3-rigid. A proof of Kerékjártó’s
classification of noncompact surfaces is also given.

MSC2020 Mathematics Subject Classification. 52C25, 05C10

##  1\. Introduction

Perhaps the first example of a noncompact surface that springs to mind is a
sphere, torus or Klein bottle, with several points or closed discs removed.
Further examples are given by unbounded surfaces, such as an infinite cylinder
with infinitely many handles, and by more exotic variations obtained by
deleting a closed totally disconnected subset. We show that every noncompact
surface has a triangulation whose underlying graph is a countable union of
finite $(3,6)$-tight graphs, in the sense of Definition 4.1. This is first
done in a constructive way, with moves that preserve minimal 3-rigidity as
well as (3,6)-tightness. A second nonconstructive proof follows from a
characterisation of general (3,6)-tight triangulations of compact surfaces.

For compact surfaces without boundary the Euler formulae imply that only the
sphere has a (3,6)-tight triangulation; the (3,6)-tight cellular embedded
graphs $G\subset S$ of other compact surfaces necessarily have a number of
nontriangular faces. If the boundary walks of these faces happen to be
disjoint cycles of $G$ then $G$ may be regarded as a (3,6)-tight triangulation
of the compact bordered surface formed by the excision of these faces.

A motivation for determining (3,6)-sparse and (3,6)-tight triangulations of
noncompact surfaces comes from their relevance to the rigidity or otherwise of
infinite triangulated bar-joint frameworks in ${\mathbb{R}}^{3}$. A finite
connected bar-joint framework $(G,p)$ in ${\mathbb{R}}^{3}$, with joints
located generically, is minimally rigid if it is rigid (infinitesimally or
continuously) and if removing any edge results in a framework that is
flexible. If this is the case we say, without ambiguity, that the graph is
minimally 3-rigid. A necessary condition for this, although not a sufficient
one, is that $G$ is a (3,6)-tight. The origins of such graph rigidity can be
traced back to Cauchy’s proof in 1813 that a convex polyhedron in
${\mathbb{R}}^{3}$ is a continuously rigid plate-and-hinge structure [2], and
to Maxwell’s 1864 observation that the structure graph of a rigid bar-joint
framework must obey certain counting rules [13].

In the construction of triangulation indicated above we make use of certain
model surfaces $S_{\gamma}$ and the fact that every noncompact suface is
homeomorphic to an $S_{\gamma}$. Such a model surface is a topological
connected sum of low genus compact bordered surfaces where the structure graph
of the connections is a countable tree. The initial bordered surface is one of
${\mathbb{S}}_{0}\backslash{\mathbb{D}},{\mathbb{S}}_{1}\backslash{\mathbb{D}}$
and ${\mathbb{P}}\backslash{\mathbb{D}}$, and the other components are
${\mathbb{S}}_{0}\backslash 2{\mathbb{D}},{\mathbb{S}}_{1}\backslash
2{\mathbb{D}},{\mathbb{P}}\backslash 2{\mathbb{D}}$ and branching surfaces,
such as ${\mathbb{S}}_{0}\backslash 3{\mathbb{D}}$. Here,
${\mathbb{S}}_{0},{\mathbb{S}}_{1}$ are the sphere and torus, ${\mathbb{P}}$
is the projective plane, and $2{\mathbb{D}}$ denotes the union of the
interiors of 2 disjoint embedded closed discs.

As a separate application of model surfaces we give a short proof of
Kerékjártó’s 1923 classification of noncompact surfaces [10]. This has also
been given in detail in Richards [16]. The ingredients of the proof concern
the manner in which $S$ is the union of an inclusion chain of compact bordered
surfaces together with the distribution of genus, in terms of the distribution
of handles and crosscaps, within these subsurfaces.

The development is organised as follows. In Section 2 we define the model
surfaces and show that every noncompact surface is homeomorphic to a model
surface. In Section 3 we define various homeomorphism invariants, such as the
totally disconnected Hausdorff space $\beta(S)$, known as the _ideal boundary_
of $S$, and we prove Kerékjártó’s theorem. Theorem 3.2 shows that the model
surfaces $S_{\gamma}$ cover all the invariants of Kerékjártó’s classification
scheme, and so they may be viewed as an alternative to Richards’ constructed
surfaces in the proof of Theorem 2 of [16]. In Section 4 we show that every
noncompact surface has a (3,6)-tight triangulation obtained by a countable
construction sequence. This involves vertex-splitting moves, Henneberg
0-extension moves and joins with appropriately sparse triangulations of low
genus compact bordered surfaces. In Section 5 the identification of general
(3,6)-triangulations $G\subset S$ is given in terms of length constraints on
the boundary walks of superfaces of a given genus. In the final section,
exploiting the fact that the construction moves above preserve minimal
3-rigidity, we give applications to the generic rigidity of associated
infinite bar-joint frameworks.

For a broad background on compact surfaces, embedded graphs and triangulations
see Gross and Tucker [7] and Mohar and Thomassen [14]. Graver et al [6] give
the generic rigidity theory of finite bar-joint frameworks. Generic rigidity
for infinite frameworks is considered, for example, in [11], [12] and [9].

##  2\. The model surfaces $S_{\gamma}$

A _surface_ is a pathwise connected metrizable Hausdorff space for which every
point has a neighbourhood that is homeomorphic to the open disc
${\mathbb{D}}$. Examples of compact surfaces are obtained by gluing in a
pairwise manner the sides of several polygons whose total side count is even.
In this case the (paired) edges provide an embedded graph in the compact
surface, the faces of which are cellular, that is, homeomorphic to open discs.
Since the polygons may be partitioned into triangles such a surface is said to
be triangulable, or to be a triangulated surface. In fact every compact
surface is homeomorphic to a triangulated surface [18] and it follows readily
from this that every noncompact surface admits a triangulation.

A _subsurface_ of a surface $S$ (either compact or noncompact) is a pathwise
connected set in $S$ that is closed in $S$ with boundary consisting of a
_finite_ number of disjoint closed curves. We also refer to a subsurface of
$S$ as a _bordered surface_ or _bordered subsurface_. The _genus_ $g=g(S)$ of
$S$ is defined to be either the maximum of the genus of a compact bordered
subsurface of $S$ or to be infinity if there is no finite maximum. We recall
that the reduced genus $g_{r}(A)$ of a compact bordered surface $A$ is equal
to $g(A)$ if $A$ is orientable and to $g(A)/2$ otherwise.

The classification theorem for compact surfaces asserts that each such surface
is homeomorphic to either a sphere with $g\geq 0$ added handles, or to a
sphere with $g\geq 1$ added crosscaps [7], [14]. We now consider a family of
noncompact surfaces that admit countable additions of handles and crosscaps is
a structured manner.

###  2.1. The surfaces $S_{\gamma}$

Let $T_{\rm bin}=(V_{\rm bin},E_{\rm bin})$ be the binary tree associated with
the usual construction of the middle thirds Cantor set $C$ in $[0,1]$. A
natural labelling of the vertices is by the symbols

$s=\phi,0,2,00,02,20,22,000,\dots,222,0000\dots$

where the digit symbols $s$ of length $|s|=k$ label the closed intervals
$I_{s}$ of length $3^{-k}$ in the construction. Thus the vertex $v_{s}$ of the
tree at level $k$ is adjacent to $v_{s0}$ and $v_{s2}$ at level $k+1$. Since
$C$ consists of the points $x$ in $[0,1]$ with a ternary expansion
$0.s_{1}s_{2}\dots$, with $s_{k}=0$ or $2$, there is a bijection between $C$
and the infinite downward directed paths with source vertex $v_{\phi}$
associated with such ternary expansions.

Let ${\mathbb{S}}_{0},{\mathbb{S}}_{1}$ be the sphere and the torus
respectively, let ${\mathbb{P}}$ be the real projective plane, and denote the
connected sum surface of a pair $S_{a},S_{b}$ of these spaces as
$S_{a}+S_{b}$. This sum is obtained by excising the interior of embedded
closed discs $D_{a}$ in $S_{a}$ and $D_{b}$ in $S_{b}$ and gluing the results
together at the resulting boundary cycles. For multiple connected sums, such
as $S_{a}+S_{b}+S_{c}+S_{d}$, it is assumed that the connected sum arises from
a pairs of disjoint excision disks in $S_{b}$ and in $S_{c}$. Similarly we may
define the infinite connected sum $S=\sum_{k=1}^{\infty}S_{k}$ with
$S_{k}\in\\{{\mathbb{S}}_{0},{\mathbb{S}}_{1},{\mathbb{P}}\\}$ for each $k$.
This noncompact surface is the union of the compact bordered surfaces

$S^{n}=\left(\sum_{k=1}^{n-1}S_{k}\right)+(S_{n}\backslash D_{n}^{0}),\quad
n=2,3,\dots.$

Here $D_{n}^{0}$ is the interior of the “exit” deletion disc for $S_{n}$ in
preparation for the connected sum with $S_{n+1}$. Thus,
$\sum_{\mathbb{N}}{\mathbb{S}}_{0}$ is homeomorphic to the plane.

Suppose now that $T=(V,E)$ is a countable subtree of $T_{\rm bin}$ with
$v_{\phi}\in V$ and with map
$\gamma:V\to\\{{\mathbb{S}}_{0},{\mathbb{S}}_{1},{\mathbb{P}}\\}$. Define
similarly the noncompact surface $S_{\gamma}$ as the infinite connected sum
$S_{\gamma}=\sum_{v\in V}\gamma(v).$ More precisely, each vertex of $T$ is
either a terminal vertex, with degree $r=1$, or a vertex of degree $r=2$ or 3.
In each case the connected sum with $\gamma(v)$ is formed with $r$ excision
discs. Once again for $n\geq 0$ the surface $S_{\gamma}$ has a compact
bordered subsurface $S_{\gamma}^{n}$ associated with the truncation of the
tree $T$ at level $n$. Also the complement $S_{\gamma}\backslash
S_{\gamma}^{n}$ has closure equal to a union of disjoint bordered surfaces,
each with a single cycle as boundary.

The model surfaces above are connected sums over countable trees with vertex
degrees bounded by 3. However, since the concatenations of the branching
surface ${\mathbb{S}}\backslash 2{\mathbb{D}}$ (see Figure 1) yields general
branching surfaces of the form ${\mathbb{S}}\backslash r{\mathbb{D}}$ it is
clear that the surfaces $S_{\gamma}$ include, up to homeomorphism, similar
infinite connected sums over a general countable directed tree.

######  Example 2.1.

(i) Let $T$, as a downward directed tree with source $v_{\phi}$, have no
terminal vertices and let $\gamma(v)={\mathbb{S}}_{0}$ for all vertices $v$.
If there are only finitely many infinite directed paths $\pi$, with source
$v_{\phi}$, then $C_{T}$ is a finite set and $S_{\gamma}$ is homeomorphic to
the sphere with finitely many points deleted. In this case triangulations
$G\subset S$ and the generic rigidity and flexibility of their bar-joint
frameworks are considered in Kitson and Power [12].

(ii) If $T=T_{\rm bin}$ and $\gamma(v)={\mathbb{S}}_{0}$ for every vertex then
$S_{\gamma}$ is homeomorphic to ${\mathbb{S}}_{0}\backslash X$ where $X$ is
homeomorphic to a Cantor set.

(iii) Let $T$ have no terminal vertices and let $C_{T}$ be the set
$\\{z_{1},z_{2},\dots\\}\cup\\{z_{\infty}\\}$ with a single accumulation
point, namely $z_{\infty}$, for the relative topology as a subset of $C$. Let
$\pi$ be the path for $z_{\infty}$ and let $\gamma(v)={\mathbb{S}}_{1}$ for
all vertices of $\pi$ and $\gamma(v)={\mathbb{S}}_{0}$ for all other vertices.
Then $S_{\gamma}$ has infinite genus and is homeomorphic to the unit sphere
modified by (i), the deletion of a convergent sequence of distinct points
together with the limit point $z_{*}$, and (ii), the addition of a sequence of
diminishing handles that cluster at $z_{*}$.

We also note the following.

(A) The surface $S_{\gamma}$ may be viewed in various ways as the union of
compact bordered surfaces with disjoint interiors. For example, let
$T(v,n,m)$, for $m>n$, be the finite subtree of the tree $T$ with source
vertex $v$ at level $n>0$ and all the possible vertices on the paths from $v$
up to level $m$. Then the restriction of a given map $\gamma$ for $T$ to these
vertices determines a compact bordered surface $S(v,n,m)$ whose boundary has a
single “entrance cycle” and $r$ “exit cycles”, where $r$ is the number of
terminal vertices of $T(v,n,m)$. Also the reduced genus of this bordered
surface is the sum of the values $g_{r}(\gamma(w))$ over the vertices of
$T(v,n,m)$ at levels $n,n+1,\dots,m-1$, where
$g_{r}({\mathbb{S}}_{0})=0,g_{r}({\mathbb{P}})=1/2,g_{r}({\mathbb{S}}_{1})=1$.

(B) The classification of compact bordered surfaces ${\mathcal{S}}$ ensures
that if ${\mathcal{S}}$ has $r+1$ boundary cycles, with a distinguished
entrance cycle and $r$ exit cycles, then ${\mathcal{S}}$ is homeomorphic to a
surface of the form $S(v,n,m)$ where the homeomorphism matches the
distinguished entrance cycle.

######  Theorem 2.2.

Each noncompact surface $S$ is homeomorphic to a surface $S_{\gamma}$.

###### Proof.

Assume, for topological convenience, that $G\subset S$ is a triangulation of
$S$. Since $G$ is a countable union it follows that $S$ is the union of an
inclusion chain of connected compact subsets $A_{1}\subset A_{2}\subset\dots,$
each of which is the closure of the union of a finite set of faces of $G$ and
we may assume that $A_{n}$ is contained in the interior of $A_{n+1}$ for all
$n$. However, $A_{1}$ need not be a compact bordered subsurface. In fact the
boundary of $A_{1}$ corresponds to a collection of closed boundary walks for
the nontriangular faces its the embedded subgraph of $G$, denoted $G(A_{1})$,
and the boundary walks mat have repeated vertices or shared vertices. To
remedy this we construct an enlargement of $A_{1}$ in a sufficiently small
neighbourhood of the boundary that is a bordered surface. This can be done,
together with the construction of a refined triangulation $G^{\prime}$ of $S$,
by performing barycentric subdivision on all the faces of $G$ that are
incident to a vertex of a particular closed boundary walk $c$. Adding further
edges to neighbouring faces determines the triangulation $G^{\prime}$ and the
boundary walk $c$ is effectively replaced by a cycle of edges disjoint from
the other boundary walks. Repeating this for the remaining closed boundary
results a new triangulation and the bordered surface $A_{1}^{\prime}$.

We next enlarge $A_{1}^{\prime}$ further in order to construct a compact
bordered surface $A_{1}^{\prime\prime}$ containing $A_{1}^{\prime}$ with the
additional property that each component of the closure of $S\backslash
A_{1}^{\prime\prime}$, has boundary consisting of a _single_ boundary cycle of
$A_{1}^{\prime\prime}$. Suppose, for example, that $U$ is a component whose
boundary consists of 2 boundary cycles, $c_{1},c_{2}$ of $A_{1}^{\prime}$.
Then there are faces $F_{1},F_{2},\dots,F_{r}$ in the interior of $U$ forming
a path between edges $e_{1},e_{2}$ in $c_{1},c_{2}$ respectively in the
following sense: $e_{1}$ is an edge of $F_{1}$, $e_{2}$ is an edge of $F_{r}$,
and each pair $F_{i},F_{i+1}$ share a single edge. Augmenting the faces of
$A_{1}^{\prime}$ by these faces determines a new compact bordered surface with
a single boundary curve replacing $c_{1},c_{2}$. Repeating this construction
gives the desired compact bordered surface $A_{1}^{\prime\prime}$, with the
components of the complement being in bijective correspondence with the
boundary cycles of $A_{1}^{\prime\prime}$.

Repeating such constructions we obtain an inclusion chain of compact bordered
surfaces $B_{1}\subset B_{2}\subset\dots$, together with an associated
triangulation such that for each $n$ the components of $S\backslash B_{n}$
have closures that are subsurfaces with a single boundary cycle. This chain
determines a general directed tree $T=(V,E)$ where, (i) the vertices at level
$n$ are labelled by the boundary cycles of $B_{n}$, (ii) a single source
vertex is adjacent to vertices at level 1, (iii) a vertex $v$ at level $n$ is
either a terminal vertex or is adjacent to vertices $v^{\prime}$ at level
$n+1$ where the boundary cycle for $v^{\prime}$ is contained in the component
of the complement of $B_{n}$ with boundary cycle labelled by $v$. We see then
that $S$ is the infinite union of $B_{1}$ and the compact bordered subsurfaces
that form the connected components of $S_{n}=(B_{n+1}\backslash B_{n})^{-}$
for $n=1,2,\dots$. Such a component bordered subsurface, ${\mathcal{S}}$ say,
has a distinguished entrance boundary cycle and a number, say $r_{n}$, of exit
boundary cycles. In particular, noting (B) above, ${\mathcal{S}}$ is
homeomorphic to a topological connected sum of the form

$({\mathcal{S}}_{1}\backslash{\mathbb{D}})+{\mathcal{S}}_{2}+{\mathcal{S}}_{3}+\dots+{\mathcal{S}}_{t-1}+({\mathcal{S}}_{t}\backslash
r_{n}{\mathbb{D}}),$

where each ${\mathcal{S}}_{i}$ is one of
${\mathbb{S}}_{0},{\mathbb{S}}_{1},{\mathbb{P}}$. Combining these
homeomorphisms, essentially by concatenations, it follows that $S$ is
homeomorphic to a surface $S_{\gamma}$. ∎

The proof above corresponds to the construction given in Ahlfors and Sario [1]
of a so-called _canonical exhaustion_ of a noncompact surface by an inclusion
chain of bordered surfaces.

##  3\. Kerékjártó’s theorem

We give a short proof of Kerékjártó’s classification theorem for noncompact
surfaces that is broadly similar to Richards’ proof [16] but with some
economies through the use of the model surfaces and Theorem 2.2. We remark
that Goldman [5] has given an algebraic proof involving the calculation of
singular homology groups.

A noncompact surface $S$ is said to be _orientable_ if every compact bordered
subsurface is orientable and to be _infinitely nonorientable_ if there is no
compact bordered subsurface $A$ for which every component of $S\backslash A$
is orientable.

If $S$ fails to be orientable or infinitely nonorientable then it is said to
be of _odd_ or _even nonorientability type_ according to whether every
sufficiently large compact subsurface contains an odd or even number of cross
caps. This may also be expressed in terms of the reduced genus, where even
(resp. odd) nonorientability type holds if every sufficiently large compact
bordered subsurface $A$ is nonorientable and has integral (resp. nonintegral)
reduced genus. In all our considerations we do not in fact need to know that
the odd/even nonorientability types are distinct properties up to
homeomorphism but this is the case for reasons of cobordism. Consider, for
example, the nonorientable connected sum surfaces

$S_{1}={\mathbb{P}}+\sum_{\mathbb{N}}{\mathbb{S}}_{1},\quad
S_{2}={\mathbb{P}}+{\mathbb{P}}+\sum_{\mathbb{N}}{\mathbb{S}}_{1},\quad
S_{3}={\mathbb{P}}+{\mathbb{P}}+{\mathbb{P}}+\sum_{\mathbb{N}}{\mathbb{S}}_{1},$

with infinite genus. Then it follows that $S_{1}$ and $S_{3}$ are homeomorphic
since ${\mathbb{P}}+{\mathbb{S}}_{1}$ and
${\mathbb{P}}+{\mathbb{P}}+{\mathbb{P}}$ are homeomorphic. On the other hand
there is no compact nonorientable bordered subsurface $A$ of $S_{2}$ with
$g_{r}(A)=1/2$ and a single boundary curve, whose complementary surface
$S_{2}\backslash A$ is orientable and so $S_{1},S_{2}$ are not homeomorhic.

The _ideal boundary_ of $S$ is defined as a set of equivalence classes of so-
called _boundary components_ of $S$. Such a component is a decreasing sequence
$p=(P_{n})$ of pathwise connected noncompact sets, $p=P_{1}\supset
P_{2}\supset\dots$, such that, (i) the boundary of $P_{i}$ in $S$ is a set of
disjoint cycles, (ii) for each compact subset $A$ the intersection $A\cap
P_{n}$ is empty for sufficiently large $n$. The boundary components
$p=(P_{n})$ and $p^{\prime}=(P_{n}^{\prime})$ are said to be _equivalent_ if
for any $n$ the inclusion $P_{n}\subseteq P_{N}^{\prime}$ holds for some $N$
as well as vice versa. The ideal boundary $\beta(S)$ is then the set of these
equivalence classes. A class $p^{*}$ is also known as an _end_ of the surface.

The ideal boundary is topologised in the following manner. For any set $U$ in
$S$ whose boundary in $S$ is compact the set $U^{*}$ is defined as the set of
all boundary components $p^{*}$, represented by a sequence $p=P_{1}\supseteq
P_{2}\supseteq\dots$, such that $P_{n}\subset U$ for $n$ sufficiently large.
The collection $U^{*}$ is a basis for the topology of $\beta(S)$ and it can be
shown that $\beta(S)$ is a nonempty compact, separable and totally
disconnected topological space. See also Section 37 of [1].

Returning to the model surfaces $S_{\gamma}$, we see from the countability of
the tree $T$ that there is a subset $C_{T}$ of the middle thirds Cantor set
$C$ that is determined by the directed paths $\pi$ of $T$ of infinite length.
This is the set of points $x=0.s_{1}s_{2}\dots$ with ternary expansions
associated with these paths, and, with the relative topology, is a compact
totally disconnected nonempty subset of $C$. It is routine to show that the
equivalence classes $p^{*}$ are in bijective correspondence with the paths
$\pi$ and that the ideal boundary $\beta(S_{\gamma})$ is homeomorphic to
$C_{T}$.

Let $P$ be a pathwise connected noncompact subset of $S$. It is said to be
_planar_ if it is homeomorphic to a subset of the plane.

######  Definition 3.1.

A point $p^{*}$ in $\beta(S)$ represented by $p=P_{1}\supset
P_{2}\supset\dots$ is planar (resp. orientable) if the sets $P_{n}$ are planar
(resp. orientable) for all sufficiently large $n$. The subset
$\beta^{\prime}(S)$ (resp. $\beta^{\prime\prime}(S)$) consists of the points
$p^{*}$ that are not planar (resp. not orientable).

The subset $\beta^{\prime}(S_{\gamma})$ of nonplanar points is readily
identifiable as the subset $C_{T}^{\prime}$ of points $x$ in $C_{T}$ whose
paths $\pi$ have vertices that are sources of directed paths that include a
vertex $w$ with $\gamma(w)\neq{\mathbb{S}}_{0}$. In particular this is
possible even with $\gamma(v)={\mathbb{S}}_{0}$ for all the vertices of $\pi$.

Let us compare the surface $S_{\gamma}$ of Example 2.1(iii) with $S_{\mu}$
where $\mu$ is defined on the same tree $T$ with $\mu(v)={\mathbb{P}}$ if and
only if $v$ is adjacent to a vertex of $\pi$ although not itself a vertex of
$\pi$. Thus every directed path of the tree has just one vertex with
$\mu$-value equal to ${\mathbb{P}}$. There is a natural identification of
$\beta(S_{\gamma})$ and $\beta(S_{\mu})$ with the set $C_{T}$ of infinite
paths of $T$. Also, the set of planar points of $\beta(S_{\gamma})$ (resp.
$\beta(S_{\mu})$) is the open set that is the union of the clopen set of all
paths that pass through a vertex all of whose successors have $\gamma$-value
(resp. $\mu$-value) equal to ${\mathbb{S}}_{0}$. It follows that these sets
coincide and so the complements,
$\beta^{\prime}(S_{\gamma}),\beta^{\prime}(S_{\mu})$ are equal. Similarly,
$\beta^{\prime\prime}(S_{\gamma})=\beta^{\prime\prime}(S_{\mu})$. It follows
readily that $S_{\gamma}$ and $S_{\mu}$ are homeomorphic by virtue of the fact
that (i), they can be viewed as the union of component compact bordered
surfaces (as in the note (A)), with components associated with finite subtrees
of $T$, and (ii), where corresponding bordered surfaces are homeomorphic.

######  Theorem 3.2.

Let $(X,Y,Z)$ be a triple of compact, separable, totally disconnected spaces
with $X\supset Y\supset Z$. Then there is a noncompact surface $S$ such that
the triple $(X,Y,Z)$ is topologically equivalent to
$\beta(S)\supset\beta^{\prime}(S)\supset\beta^{\prime}(S)$ by means of a
homeomorphism from $X$ to $\beta(S)$.

###### Proof.

It is well-known that any compact, separable, totally disconnected space $X$
is homeomorphic to a subset of the Cantor set $C$, and so we may assume that
$X$, and also $Y$ and $Z$, are subsets of $C$. Let $T$ be the subtree of
$T_{\rm bin}$ corresponding to $X$ and suppose first that $Y\neq X,Z\neq Y$
and $Z\neq\phi$.

For a point $z$ in $Z$ with path $\pi_{z}$ define $\gamma(w)={\mathbb{P}}_{1}$
for all vertices of $\pi_{z}$. For $y$ in $Y\backslash Z$ with path $\pi_{y}$
define $\gamma(u)={\mathbb{S}}_{1}$ for all the vertices $u$ of $\pi_{y}$ for
which $\gamma(u)$ is not defined. Finally, for $x$ in $X\backslash Y$ with
path $\pi_{x}$ define $\gamma(v)={\mathbb{S}}_{0}$ for all the vertices $v$ of
$\pi_{x}$ for which $\gamma(v)$ is not yet defined. Now $\gamma$ is fully
defined and it follows readily from the definitions that
$\beta(S_{\gamma})=X,\beta^{\prime}(S_{\gamma})=Y,\beta^{\prime}(S_{\gamma})=Z$.
In view of our remarks and examples concerning odd and even nonorientability
types the other cases are similarly straightforward. ∎

The triple $\beta(S)\supset\beta^{\prime}(S)\supset\beta^{\prime}(S)$ is a
homeomorphism invariant. To obtain a complete set of classifying invariants it
turns out that it is sufficient to add the (possibly infinite) genus and the
orientability type, of which there are four possibilities. This is
Kerékjártó’s theorem.

######  Theorem 3.3.

Let $S_{1}$ and $S_{2}$ be noncompact surfaces having the same genus and the
same orientability type. Then $S_{1}$ is homeomorphic to $S_{2}$ if and only
if there is a homeomorphism $\phi:\beta(S_{1})\to\beta(S_{2})$ such that
$\phi(\beta^{\prime}(S_{1}))=\phi(\beta^{\prime}(S_{2}))$ and
$\phi(\beta^{\prime\prime}(S_{1}))=\phi(\beta^{\prime\prime}(S_{2}))$.

###### Proof.

We may assume that the surfaces are $S_{\gamma}$ and $S_{\mu}$ with trees
$T_{\gamma}$ and $T_{\mu}$, that they are of the same genus and orientablility
type, and that the triples
$\beta(S_{\gamma})\supset\beta^{\prime}(S_{\gamma})\supset\beta^{\prime\prime}(S_{\gamma})$
and
$\beta(S_{\mu})\supset\beta^{\prime}(S_{\mu})\supset\beta^{\prime\prime}(S_{\mu})$
coincide as triples of subsets of $C$. In particular the directed subtrees
$T_{\gamma}^{\infty}$ and $T_{\mu}^{\infty}$ determined by the directed
infinite paths with source $v_{\phi}$ are identical. We claim that it follows
from these assumptions that there is an inclusion chain ($T_{\gamma}^{n}$)
(resp. ($T_{\mu}^{n})$)) of finite subtrees of $T_{\gamma}$ (resp. $T_{\mu}$),
where the orientability type and total reduced genus of the restriction
$\gamma$ to $T_{\gamma}^{n}$ agrees with that of the restriction of $\mu$ to
$T_{\mu}^{n}$. The _total reduced genus_ for $T_{\gamma}^{n}$ is by definition
the sum of $g_{r}(\gamma(v))$ over the vertices $v$ of $T_{\gamma}^{n}$. The
claim is purely combinatorial and follows from examination of the various
cases. The subtree inclusion chains determine compact bordered surface
inclusion chains, $B_{1}\subset B_{2}\subset\dots$ and $C_{1}\subset
C_{2}\subset\dots$ for which there exists a sequence of homeomorphisms
$\alpha_{k}:B_{k}\to C_{k}$ (respecting entrance and exit cycles) where for
all $k$ the restriction of $\alpha_{k+1}$ to $B_{k}$ is equal to $\alpha_{k}$.
This completes the determination of the desired homeomorphism. ∎

##  4\. Triangulations of noncompact surfaces

We now show that every noncompact surface $S$ has a (3,6)-tight triangulation
in the sense of the next definition. This is done in a constructive manner, in
the setting of a model surface, by means of moves corresponding to Henneberg
0-extension, vertex-splitting and finite graph substitutions.

The Maxwell count $f(G)$ of a finite graph $G=(V,E)$ is $3|V|-|E|$.

######  Definition 4.1.

(i) A finite graph is _$(3,6)$ -sparse_ if it satisfies the local count
$f(G^{\prime})\geq 6$ for each subgraph $G^{\prime}=(V^{\prime},E^{\prime})$
with at least 3 vertices and is _$(3,6)$ -tight_ if in addition $f(G)=6$. (ii)
A countable graph $G$ is _$(3,6)$ -sparse_ (resp. _$(3,6)$ -tight_) if there
exists a tower $G_{1}\subset G_{2}\subset\dots$ of finite $(3,6)$-sparse
subgraphs (resp. $(3,6)$-tight subgraphs) whose union is $G$.

###  4.1. Constructive (3,6)-tight triangulations

The surface ${\mathbb{S}}_{0}\backslash 3{\mathbb{D}}$ with boundary $\partial
B$ consisting of disjoint cycles $a,b,c$ is depicted in Figure 1. We refer to
this surface (known also as topological pants) as a _branching surface_. The
next lemma will enable the extensions of finite (3,6)-tight triangulations
that correspond to the branching aspect of a binary tree.

The Hennenberg 0-extension move, in the context of (3,6)-tight graphs, is the
graph move $G\to G^{\prime}$ that adds a single vertex $v$ of degree 3 and
edges $w_{1}v,w_{2}v,w_{3}v$ with $w_{1},w_{2},w_{3}$ distinct vertices of
$G$. For surface embedded graphs a 0-extension move can be used to introduce a
vertex of degree 3 in a face and in this way we may replace a nontriangular
face by new faces.

######  Lemma 4.2.

let $G$ be a (3,6)-tight graph with a cycle $d$ of length $|d|\geq 3$. Then
for any values of $|b|\geq 3,|c|\geq 3$ with $|d|-3=|b|-3+|c|-3$ there is a
triangulation $H$ of $B={\mathbb{S}}_{0}\backslash 3{\mathbb{D}}$, with
boundary cycles $a,b,c$ of lengths $|a|,|b|,|c|$ with $|a|=|d|$ such that the
join $G^{+}=G\cup_{d=a}H$ is (3,6)-tight. Moreover, there exist such
triangulations $H$ that may be obtained from the cycle $d$ by 0-extension
moves.

###### Proof.

Apply a 0-extension move to the graph of the cycle $d$, viewed as a planar
graph, as illustrated in Figure 2(i), to create further cycles
$b^{\prime},c^{\prime}$ of lengths $|b^{\prime}|=|b|,|c^{\prime}|=|c|$. Apply
further 0-extension moves, within the face for the $b^{\prime}$-cycle to
obtain a cycle $b$, of the same length, that is disjoint from the cycle $d$,
as illustrated in Figure 2(ii). Doing the same for $c^{\prime}$ we obtain a
triangulation $H$ of ${\mathbb{S}}_{0}\backslash 3{\mathbb{D}}$. The
0-extension move preserves (3,6)-sparsity and (3,6)-tightness. Thus the proof
of the lemma is completed on observing that $G^{+}$ is constructed from $G$ by
0-extension moves. ∎

$a$$b$$c$$a$$b$$c$

Figure 1. Depictions of the branching surface $B={\mathbb{S}}_{0}\backslash
3{\mathbb{D}}$. Figure 2. (i) A Hennenberg 0-extension move adding a vertex of
degree 3 and 3 incident edges to an 8-cycle. (ii) Further 0-extension moves
giving a 5-cycle that is disjoint from the 8-cycle.

Lemma 4.2 has a simple generalisation to the branching surface with
${\mathbb{S}}_{0}\backslash(m+1){\mathbb{D}}$ with $m\geq 2$ exit cycles. In
particular, from a single (3,6)-tight “block” one can construct a so-called
_block and hole graph_ , with 1 block and $m$ holes, that is (3,6)-tight. For
simplicity we define the block specifically as the (3,6)-tight graph obtained
from an $r$-cycle, with $r\geq 3$, by adding two vertices and the $2r$ edges
from the $r$-cycle vertices to the added vertices. This block graph is also
known as a _discus graph_ ${\mathcal{D}}_{r}$, with perimeter of $r$ edges.
See also Remark 4.6.

The following elementary substitution lemma features in the proof of Lemma 4.4
and is useful for sequential constructions. It has a companion lemma, with the
(3,6)-tight condition replaced by minimal 3-rigidity, that we make use of in
Section 6.

######  Lemma 4.3.

Let $A,A^{\prime}$ be compact bordered surfaces, let $G\subset
A,G^{\prime}\subset A^{\prime}$ be (3,6)-tight triangulations, and let
$d,d^{\prime}$ be cycles of edges of $G,G^{\prime}$ corresponding to one of
the boundary cycles of $A,A^{\prime}$. Suppose that $B$ is a compact bordered
surface with a triangulation $H$ with a boundary cycle $a$ and that
$|a|=|d|=|d^{\prime}|$. Then $G\cup_{\rm d=a}H$ is (3,6)-tight if and only if
$G^{\prime}\cup_{\rm d^{\prime}=a}H$ is (3,6)-tight.

###### Proof.

Let $G\cup H$ be (3,6)-tight and let $K\subset G^{\prime}\cup H$ a subgraph
with at least 3 vertices. We claim that $f(K)\geq 6$. If $K\subset G^{\prime}$
or $K\subset H$ this is clear and so we may assume that $K$ has edges in
$G^{\prime}$ and in $H$. Now

$6\leq f(G\cup(K\cap H))=f(G)+f(K\cap H)-f((K\cap H)\cap G)$

and so $f(K\cap H)-f((K\cap H)\cap G)\geq 0$. Also, $f((K\cap H)\cap
G)=f((K\cap H)\cap G^{\prime})$. Thus

$f(K)=f((K\cap G^{\prime})\cup(K\cap H)=f(K\cap G^{\prime})+(f(K\cap
H)-f(K\cap H\cap G)),$

and so $f(K)\geq 6$. It follows similarly that $f(G^{\prime}\cup H)=6$. ∎

In the proof of the next lemma we make use of the triangulations given in
Figure 3. It is elementary to show that, as graphs, they are generated from
$K_{3}$ by a sequence of 0-extension moves.

Figure 3. (3,6)-tight triangulations of the bordered surfaces (i)
$B={\mathbb{P}}\backslash{\mathbb{D}}$ with $g_{r}(B)=1/2$, (ii)
$B={\mathbb{S}}_{1}\backslash{\mathbb{D}}$ with $g_{r}(B)=1$.

We next use 0-extension and vertex-splitting moves on the embedded graphs of
Figure 3 in order to introduce a block graph whose removal yields a
(3,6)-sparse triangulation of ${\mathbb{P}}\backslash 2{\mathbb{D}}$ (resp.
${\mathbb{S}}_{1}\backslash 2{\mathbb{D}}$) with 2 nontriangular face cycles
of lengths $r$ and $r+3$ (resp. $r$ and $r+6$).

######  Lemma 4.4.

Let $G$ be a (3,6)-tight graph with a cycle $d$ of length $\delta\geq 3$ and
let $B$ be one of the compact bordered surfaces ${\mathbb{S}}_{0}\backslash
2{\mathbb{D}},{\mathbb{P}}\backslash 2{\mathbb{D}},{\mathbb{S}}_{1}\backslash
2{\mathbb{D}}$. Suppose that $\beta=\delta+6g_{r}(B)$. Then there is a
triangulation $H$ of $B$ with boundary cycles $a,b$ of lengths $\delta,\beta$
such that the join $G^{+}=G\cup_{d=a}H$ is (3,6)-tight

###### Proof.

The case $B={\mathbb{S}}_{0}\backslash 2{\mathbb{D}}$ is covered by the
remarks following Lemma 4.2 and so we consider first $B={\mathbb{P}}\backslash
2{\mathbb{D}}$. Let $G_{1}$ be the (3,6)-tight triangulation of
${\mathbb{P}}\backslash{\mathbb{D}}$ given in Figure 3. Let
$K_{3}\cup_{e}C_{6}$ be a subgraph composed of a facial 3-cycle and the
boundary cycle of the nontriangular face, with common edge $e$. Applying two
0-extension moves to the $K_{3}$ subgraph to create ${\mathcal{D}}_{3}\cup
C_{6}$ from $K_{3}\cup_{e}C_{6}$. Further vertex splitting moves are possible
to create ${\mathcal{D}}_{\delta}\cup C_{\delta+3}$. See the illustration in
Figure 4.

Figure 4. A double 0-extension move,
$K_{3}\cup_{e}C_{6}\to{\mathcal{D}}_{3}\cup_{e}C_{6}$, followed by a vertex-
splitting move
${\mathcal{D}}_{3}\cup_{e}C_{6}\to{\mathcal{D}}_{4}\cup_{e}C_{5}$.

These moves extend to moves on $G_{1}$ to create the graph, $G_{2}$ say, that
has the form ${\mathcal{D}}_{\delta}\cup_{d}H_{1}$ where the perimeter cycle
$d$ of ${\mathcal{D}}_{\delta}$ is identified with a cycle of the same length
in $H_{1}$. Viewing $H_{1}$ as an embeded graph in ${\mathbb{P}}$ we see that
it is cellular with 2 nontrangular faces bordered by the cycles of lengths
$\delta$ and $\delta+3$. These cycles share some vertices and so we perform
0-extension moves inside one of the nontriangular faces to obtain a graph $H$
from $H_{1}$ that is a triangulation of ${\mathbb{P}}\backslash
2{\mathbb{D}}$. The containing graph $G_{3}$ obtained from $G_{2}$ by
performing these 0-extensions has the form ${\mathcal{D}}_{\delta}\cup_{d}H$
is (3,6)-tight. The lemma now follows in this case from Lemma 4.3.

The argument for $B={\mathbb{S}}_{1}\backslash 2{\mathbb{D}}$, starting with
the triangulation of ${\mathbb{S}}_{1}\backslash{\mathbb{D}}$ in Figure 3(ii),
is entirely similar. ∎

######  Theorem 4.5.

Every noncompact surface has a triangulation that is (3,6)-tight.

###### Proof.

In view of Theorem 2.2 it suffices to show that each surface $S_{\gamma}$ has
a (3,6)-tight triangulation $G$. We obtain $G$ as a union of (3,6)-tight
triangulations $G_{\gamma}^{k}$ of the bordered surfaces $S_{\gamma}^{k}$
associated with levels $k\geq 0$. We may assume that $T=T_{\rm bin}$, the
argument for subtrees being entirely similar.

At level $k=0$, if $\gamma(v_{\phi})={\mathbb{S}}_{0}$ then let
$G_{\gamma}^{0}$ be any triangulation of
${\mathbb{S}}_{0}\backslash{\mathbb{D}}$ where the boundary cycle is a
3-cycle. This is (3,6)-tight. If $\gamma(v_{\phi})$ is equal to ${\mathbb{P}}$
(resp. ${\mathbb{S}}_{1}$) there is a (3,6)-tight triangulation where the
boundary cycle is a 6-cycle (resp. 9-cycle).

To construct $G_{\gamma}^{k+1}$ from $G_{\gamma}^{k}$ note first that
$G_{\gamma}^{k}$ has $2^{k}$ boundary cycles. Let $d$, with length $|d|\geq
3$, denote the first of these cycles. Join to $S_{\gamma}^{k}$ the branching
surface ${\mathbb{S}}_{0}\backslash 3{\mathbb{D}}$ with boundary cycles
$a,b,c$, by identifying $d$ with $a$. In this way we obtain the compact
bordered surface,

$S_{\gamma}^{k}\cup_{d=a}({\mathbb{S}}_{0}\backslash 3{\mathbb{D}}),$

and we may view the new border cycles $b,c$ as replacing the border cycle $d$.
Using Lemma 4.2 the (3,6)-tight triangulation may be extended to this bordered
surface. Repeating such additions for the other boundary cycles of
$G_{\gamma}^{k}$ gives an intermediate (3,6)-tight triangulation, that we
denote as $H_{\gamma}^{k+1}$, of a compact bordered surface with $2^{k+1}$
boundary cycles.

Join to the boundary cycles of this intermediate surface copies of
${\mathbb{S}}_{0}\backslash 2{\mathbb{D}},{\mathbb{P}}\backslash
2{\mathbb{D}},{\mathbb{S}}_{1}\backslash 2{\mathbb{D}}$, according to the
values of $\gamma(v)$ at level $k+1$. This results in the surface
$S_{\gamma}^{k+1}$. Moreover, using Lemma 4.4, the (3,6)-tight triangulation
$H_{\gamma}^{k+1}$ may be progressively extended, terminating in a (3,6)-tight
triangulation $G_{\gamma}^{k+1}$ of $S_{\gamma}^{k+1}$. This is true for all
$k$ and gives the desired triangulation. ∎

######  Remark 4.6.

In Cruickshank, Kitson and Power [3] a complete characterision of
$(3,6)$-tight block and hole graphs with a single block was given in terms of
the satisfaction of _girth inequalities_. These inequalities require that any
closed walk $d$ around a set of hole boundary cycles $a_{1},\dots a_{k}$
should satisfy

$|d|-3\geq(|a_{1}|-3)+\dots+(|a_{k}|-3).$

It follows from this that the graph $G^{+}$ in Lemma 4.2 is (3,6)-tight if and
only if $H$ _satisfies the boundary girth inequalities_ in the sense that
every closed walk $w$ that is homotopic to $a$ (resp. $b$, resp. $c$) has
length at least $|a|$ (resp. $|b|$, resp. $|c|$).

##  5\. General (3,6)-tight triangulations.

We next obtain a characterisation of general (3,6)-tight triangulations as a
consequence of the characterisation for compact bordered surfaces.. See also
[15] for this compact case. This leads to an alternative nonconstructive proof
of Theorem 4.5.

Let $G\subset S$ be a cellularly embedded graph in a compact surface $S$. A
_superface_ of $G$ is a face $U$ (not necessarily cellular) of a subgraph $H$
of $G$. We assume that superfaces are _proper_ in the sense of containing no
vertices of degree 0 or 1. A _balanced_ superface is one for which the
complement of its closure is nonempty and connected. A _simple_ superface is
one whose closed boundary walks are disjoint cycles. For a simple superface
$U$ whose topological boundary is given by disjoint cycles $d_{1},\dots,d_{s}$
the closure $U^{-}$ of $U$ is a bordered surface of genus $g(U)$ and reduced
genus $g_{r}(U)$.

Let $U$ be a superface of $S$ which is both simple and balanced, with boundary
cycles $d_{1},\dots,d_{s}$ and complementary superface $W$. In particular both
$U^{-}$ and $W^{-}$ are connected bordered surfaces. Then the following
standard addition formula holds. See also [16].

$g_{r}(S)=g_{r}(U^{-})+g_{r}(W^{-})+(s-1).$

As noted in [15], if $G\subset S$ is cellular with $f(G)=3v-e=\alpha\geq 6$
and with nontriangular faces, $U_{1},\dots,U_{n}$, with closed boundary walks
$c_{1},\dots,c_{n}$, then the Euler formula for $G$ gives

$\sum_{k}(|c_{k}|-3)=6g_{r}(S)+f(G)-6.$

We call this the _face walk identity_ for the embedded graph $G$ in $S$.

Suppose, again, that $U$ is balanced and simple with complementary superface
$W$. Let $G_{W}$ denote the subgraph of $G$ whose edges lie in the closure of
$W$. This is an embedded graph in the bordered surface $W^{-}$. It is also an
embedded graph in the surface, $S_{W}$ say, obtained by capping the boundary
cycles with open discs. Since $g_{r}(S_{W})=g_{r}(W^{-})=g_{r}(W)$ we may use
these quantities interchangeably. It follows that we have the face-walk
identity,

$\sum_{k=1}^{s}(|d_{k}|-3)+\sum_{k\in
I(W)}(|c_{k}|-3)=6g_{r}(S_{W})+f(G_{W})-6,$

where we write $I(W)$ for the set of indices $k$ for which the face $U_{k}$ of
$G$ is contained in $W$.

######  Lemma 5.1.

Let $G$ be a cellularly embedded graph in the compact surface $S$ with
$f(G)=6$, let $U$ be a balanced, simple superface of $G$ with complementary
superface $W$, and let $d_{1},\dots,d_{s}$ be the common boundary cycles of
$U$ and $W$. Then the following inequalities are equivalent.

(i) $f(G_{W})\geq 6$.

(ii)

$\sum_{k=1}^{s}(|d_{k}|-3)+\sum_{k\in I(W)}(|c_{k}|-3)\geq 6g_{r}(W).$

(iii)

$\sum_{k=1}^{s}(|d_{k}|-3)\geq\sum_{k\in I(U)}(|c_{k}|-3)-6(g_{r}(U)+s-1).$

###### Proof.

The equivalence of (i) and (ii) follows from the face walk identity for
$G_{W}$ in $S_{W}$. By the face-walk identity for $G$ observe that (ii) holds
if and only if

$\sum_{k=1}^{s}(|d_{k}|-3)+(6g_{r}(S)-\sum_{k\in I(U)}(|c_{k}|-3))\geq
6g_{r}(W),$

and, in view of the reduced genus addition formula, this holds if and only if
(iii) holds. ∎

######  Definition 5.2.

A cellularly embedded graph $G$, in the compact surface $S$, with Maxwell
count 6 _satisfies the girth inequalities_ , or _satisfies the (3,6)-tight
girth inequalities_ , if the inequality (iii) of Lemma 5.1 holds for every
balanced superface $U$ of $G$ with closed boundary walks $d_{1},\dots,d_{s}$.

Note that the boundary walks in this definition are general and need not be
cycles and need not be disjoint. The following equivalences were shown in
[15].

######  Theorem 5.3.

Let $G$ be a cellularly embedded graph in a compact surface with $f(G)=6$.
Then the following are equivalent.

(i) $G$ is (3,6)-tight.

(ii) $f(G_{U})\geq 6$ for every superface $U$ of $G$.

(iii) $G$ satisfies the (3,6)-tight girth inequalities.

###### Proof.

The equivalence of (i) and (ii) is due to Qays Shakir [17]. We give the short
proof from [15]. The implication (i) implies (ii) is immediate. Assume (ii)
holds and suppose, by way of contradiction, that $K$ is a maximal subgraph of
$G$ with at least 3 vertices and $f(K)\leq 5$. Let $U$ be a face of $K$ and
let $G_{U}^{c}$ be the subgraph of $G$ determined by the edges in the
complement of the closure of $U$. Since $G$ is the union of $G_{U}$ and
$G_{U}^{c}$ we have $f(G)=f(G_{U})+f(G_{U}^{c})-f(\partial U)$ as well as
$f(G)=6$. The condition $f(G_{U}^{c})\geq 6$ is therefore equivalent to
$f(G_{U})-f(\partial U)\leq 0$. Thus, since $K\cap G_{U}=\partial U$, we have

$f(K\cup G_{U})=f(K)+f(G_{U})-f(K\cap G_{U})\leq f(K).$

By the maximality of $K$ it follows that $K=K\cup G_{U}$. Since this is true
for all faces $U$ of $K$ it follows that $K=G$, a contradiction.

The equivalence of (ii) and (iii) follows in two routine steps. (See also
[15].) Firstly, Lemma 5.1 can be generalised to balanced superfaces $U$ that
are not necessarily simple. This follows from the association of a balanced
superface of $G$ with a balanced simple superface of a larger embedded graph
in $S$ obtained by vertex splitting moves. Secondly (ii) is equivalent to
having $f(G_{U})\geq 6$ for every _balanced_ superface. ∎

In view of Theorem 5.3 the next theorem has Theorem 4.5 as an immediate
corollary. A key point in the proof is that a partial barycentric subdivision
of a triangulation $H$ of a compact bordered surface, that adds no new
vertices to the boundary, preserves the Maxwell count $f(H)=6$ but strictly
increases the minimum length of an “interior path” between 2 boundary vertices
that visits no other boundary vertices. Thus if $H$ is a triangulation with
$f(H)=6$ then we can derive a (3,6)-tight triangulation by performing
barycentric subdivision a finite number of times to ensure that all the girth
inequalities hold. In the proof this is done in a step by step manner within a
surface $S_{\gamma}$ but it could equally well be performed on a general
branching inclusion chain $B_{1}\subset B_{2}\subset\dots$, as given in the
last paragraph of Theorem 2.2.

######  Theorem 5.4.

Let $S$ be a noncompact surface. Then there are compact bordered subsurfaces
$S_{1}\subset S_{2}\dots$ with union equal to $S$, together with
triangulations $G_{k}\subset S_{k}$ with $f(G_{k})=6$, such that for every $k$
the embedded graph $G_{k}$ in $S_{k}$ satisfies the girth inequalities.

###### Proof.

We may assume, using earlier notation, that $S$ is equal to $S_{\gamma}$ with
inclusion chain $S_{\gamma}^{0}\subset S_{\gamma}^{1}\subset
S_{\gamma}^{2}\subset\dots$. Let $G_{0}$ be a (3,6)-tight triangulation of
$S_{\gamma}^{0}$, making use of the triangulations of Figure 3 in the cases
${\mathbb{P}}\backslash{\mathbb{D}}$ and
${\mathbb{S}}_{1}\backslash{\mathbb{D}}$. Suppose, by way of induction, that
$G_{n}$ is a (3,6)-tight triangulation of $S_{\gamma}^{n}$. Recall that
$S_{\gamma}^{n+1}$ is obtained from $S_{\gamma}^{n}$ by successively adding
component bordered surfaces of 4 types, namely the branching surface
${\mathbb{S}}_{0}\backslash 3{\mathbb{D}}$ and the bordered surfaces
${\mathbb{S}}_{0}\backslash 2{\mathbb{D}},{\mathbb{P}}\backslash
2{\mathbb{D}}$ and ${\mathbb{S}}_{1}\backslash 2{\mathbb{D}}$. We claim that
each successive addition can be triangulated so that the resulting
triangulation is (3,6)-tight.

Suppose then that $B$ is a component bordered surface to be added to the
compact bordered surface $A$ where $G_{A}\subset A$ is a (3,6)-tight
triangulation, with $G_{A}$ satisfying the girth inequalities. Here $B$ is one
of the surfaces ${\mathbb{S}}_{0}\backslash
3{\mathbb{D}},{\mathbb{S}}_{0}\backslash 2{\mathbb{D}},{\mathbb{P}}\backslash
2{\mathbb{D}}$ and ${\mathbb{S}}_{1}\backslash 2{\mathbb{D}}$. Suppose, for
example, that $B={\mathbb{S}}_{1}\backslash 2{\mathbb{D}}$ must be
triangulated in a way that includes the predetermined input border cycle of
length $\delta$. Construct first any such triangulation $G_{B}$ where the exit
cycle has length $\delta+6g_{r}(B)=\delta+6$. Then $f(G_{A}\cup G_{B})=6$.
Next, as in our preliminary comments, perform partial barycentric subdivisions
on all the faces of $G_{B}$ where new vertices are only introduced in the
interior of $B$. We claim that after finitely many iterations of such
subdivision, the resulting triangulation, $H_{B}$ say, has the property that
the embedded graph $G_{A}\cup H_{B}$ satisfies the girth inequalities. To
confirm the claim it suffices, since $G_{A}$ satisfies the girth inequalities,
to verify this for a balanced superface $U$ of $G_{A}\cup H_{B}$ that has a
closed walk, $d_{1}$ say, in the set $\\{d_{1},\dots,d_{s}\\}$ of its closed
boundary walks, with a subwalk $\pi$, interior to $B$, between 2 vertices of
$H_{B}$. Thus the length $|d_{1}|$ is at least as great as the number of
barycentric iterations. The girth inequality for $U$ requires that

$\sum_{k=1}^{s}(|d_{k}|-3)\geq\sum_{k\in I(U)}(|c_{k}|-3)-6(g_{r}(U)+s-1)$

where $I(U)$ is the index set for the boundary cycles $c_{k}$ of $G_{A}\cup
H_{B}$ that are interior to the superface $U$. Since the right-hand side is
bounded independently of the number barycentric divisions, the claim and the
theorem follow. ∎

######  Remark 5.5.

It is not the case that every (3,6)-tight triangulation $G\subset S$ of a
noncompact surface $S$ has an inclusion chain $G_{1}\subset G_{2}\subset\dots$
of the type given in Theorem 5.4. The reason for this is that the required
Maxwell condition $f(G_{k})=6$ may only hold when $G_{k}$ is the triangulation
of a bordered pseudosurface where the boundary is formed of cycles that are
not disjoint. Figure 5 shows such a branching surface $B$, with a single
crosscap, and it may be triangulated in an arbitrary way subject to the
requirement $|b|-3+|c|-3=|a|-3+6g_{r}(B)$. This ensures that its join, on the
identification of $a$ with a cycle in a (3,6)-tight graph, should satisfy the
Maxwell count. Concatenate a sequence $B_{1},B_{2},\dots$ of such triangulated
bordered pseudosurfaces (leaving no boundary unconcatenated). The resulting
inclusion chain $G_{1}\subset G_{2}\subset\dots$ gives a triangulation $G$ of
the union $B$ of the $B_{n}$. This satisfies $f(G_{k})=6$ for all $k$. Finally
we may perform partial barycentric subdivision finitely many times, as in the
previous proof, so that the new triangulation $G^{\prime}$ is (3,6)-tight but
there is no compact bordered surface $A\subset S$ with induced triangulation
$H\subset G$ with $f(H)=6$. Indeed, any such $A$ has a boundary that is a
union of a nondisjoint set of cycles.

$a$b$c$

Figure 5. A bordered branching pseudosurface $B$ with $g_{r}(B)=1/2$.

######  Remark 5.6.

Lemma 5.1(ii) can be used to show that a periodic surface in
${\mathbb{R}}^{3}$ with infinite genus fails to have a periodic (3,6)-tight
triangulation. For example, the bordered surface in Figure 6 shows a geometric
realisation, $S_{0}$ say, of ${\mathbb{S}}_{0}\backslash 6{\mathbb{D}}$, with
the symmetry of a cube. We assume that the distance between opposite boundary
circles is unity. The 3-periodic surface, $S$ say, formed by an infinite
concatenation of translates of $S_{0}$ has infinite genus and a singleton
ideal boundary. The minimal surface realisation of $S$ is known as the Schwarz
P surface.

Figure 6. Building block for the Schwarz P surface..

Let $S_{n}$ be the compact bordered subsurface formed by the join of $n^{3}$
copies of $S_{0}$, in cubic form, and suppose that $S_{n}$ lies in the
interior of a similar subsurface $S_{m}$ with $m>n$. Suppose, for simplicity,
that $G$ is a periodic triangulation, under integral translations, determined
by a triangulation of $S_{0}$. Let $W$ be the balanced simple superface of
$G_{m}\subset S_{m}$ that is equal to the interior of $S_{m}\backslash S_{n}$.
It has a set of boundary cycles, $d_{1},\dots d_{t}$ say, consisting of the
union of the boundary cycles for $S_{n}$ and $S_{m}$. From Lemma 5.1(ii) we
see that the condition $f(G_{W})\geq 6$ is equivalent to

$\sum_{k=1}^{t}(|d_{k}|-3)\geq 6g_{r}(W).$

By the periodicity, for fixed $n$ the left hand side is of order $m^{2}$.
However, the right hand side is of order $m^{3}$ and so the inequality
$f(G_{W})\geq 6$ cannot hold for large $m$ and so $G$ fails to be (3,6)-tight.

##  6\. Bar-joint frameworks

A bar-joint framework $(G,p)$ in ${\mathbb{R}}^{3}$ consists of a finite or
countable simple graph $G=(V,E)$ and a placement $p:V\to{\mathbb{R}}^{3}$ such
that $p(v),p(w)$ are distinct for each edge $vw$ in $E$. An _infinitesimal
flex_ of $(G,p)$ is an assignment $u:V\to{\mathbb{R}}^{3}$ that satisfies the
infinitesimal flex condition $(u(v)-u(w))\cdot(p(v)-p(w))=0$ for every edge
$vw$. A _trivial infinitesimal flex_ of $(G,p)$ is one that extends to an
infinitesimal flex of any containing framework, which is to say that it is a
linear combination of a translation infinitesimal flex and a rotation
infinitesimal flex. The framework $(G,p)$ is infinitesimally rigid if the only
infinitesimal flexes are trivial, and the graph $G$ is _3-rigid_ if every
generic framework $(G,p)$, where the coordinates of the vertex placements form
an algebraically independent set, is infinitesimally rigid. Also $G$ is
_minimally 3-rigid_ if on deleting any edge of $G$ the resulting graph fails
to be 3-rigid. A finite graph $G$ that is minimally 3-rigid is necessarily
(3,6)-tight, but the converse does not hold as evidenced by the double banana
graph. See also Figure 7 below.

It is well-known that the Henneberg 0-extension move and vertex-splitting
preserve minimal 3-rigidity. See, for example, Whiteley [19], Graver et al
[6], and the appendix of [3]. A sufficient condition for minimal 3-rigidity is
that there exists a sequence of finite subframeworks $(G_{n},p)$, associated
with vertex-induced subgraphs $G_{1}\subset G_{2}\subset\dots,$ each of which
is minimally 3-rigid. That this sequential 3-rigidity condition is not
necessary is shown by examples in Kitson and Power [11], [12].

Let us first consider some low genus examples of noncompact surfaces for which
the ideal boundary is finite.

######  Example 6.1.

Figure 7 (see also [4]) shows an embedded graph in the torus that is
$(3,6)$-tight and 2-connected. The 2 nontriangular faces each have a single
boundary walk that is not a cycle, and $G$ can be viewed also as a
triangulation of a pseudosurface. Since $G$ is 2-connected it is not 3-rigid.
We may extend this example to an infinite triangulation of the punctured
surface $S={\mathbb{S}}_{1}\backslash\\{x_{1},x_{2}\\}$ by indefinitely
repeated 0-extension moves on boundary vertices, in the manner of Figure
2(ii). Thus there is a (3,6)-tight triangulation of $S$ that is not 3-rigid.
On the other hand the (3,6)-tight triangulations of the singly punctured torus
are minimally 3-rigid. This follows readily from the main result in [4].

Figure 7. A finite (3,6)-tight embedded graph $G\subset{\mathbb{S}}_{1}$ that
is not 3-rigid.

######  Example 6.2.

In Kastis and Power [8] it is shown that every (3,6)-tight embedded graph
$G\subset{\mathbb{P}}$ is minimally 3-rigid and moreover is obtained from
$K_{3}$ by general vertex splitting moves. (See also [15].) It follows from
this that any (3,6)-tight triangulation of a finitely punctured projective
plane is minimally 3-rigid.

The following rigid subgraph substitution lemma (the companion to Lemma 4.3)
is well-known and follows readily from the definitions of infinitesimal
flexibility and 3-rigidity.

######  Lemma 6.3.

Let $A,A^{\prime}$ be compact bordered surfaces, let $G\subset
A,G^{\prime}\subset A^{\prime}$ be minimally 3-rigid triangulations, and let
$d,d^{\prime}$ be cycles of edges of $G,G^{\prime}$ corresponding to one of
the boundary cycles of $A,A^{\prime}$. Suppose that $B$ is a compact bordered
surface with a triangulation $H$ with a boundary cycle $a$ and that
$|a|=|d|=|d^{\prime}|$. Then $G\cup_{\rm d=a}H$ is minimally 3-rigid if and
only if $G^{\prime}\cup_{\rm d^{\prime}=a}H$ is minimally 3-rigid.

######  Theorem 6.4.

Let $S$ be a noncompact surface. Then there is a (3,6)-tight triangulation of
$S$ whose graph is minimally 3-rigid.

###### Proof.

In the proof of Theorem 4.5 the (3,6)-tight triangulation of any given model
surface $S_{\gamma}$ is constructed as a union of an upward chain of graphs
$G_{n},n=0,1,2,\dots,$ each of which is a (3,6)-tight triangulation of a
compact bordered surface, say $S_{n}$. The first embedded graph can be taken
to be $G_{0}\subset S_{0}\backslash{\mathbb{D}}$, a triangulation with a
single triangular boundary. This is minimally 3-rigid as well as (3,6)-tight.
Assume, by way of an induction step, that $G_{n}\subset S_{n}$ is minimally
3-rigid. The triangulation of $G_{n+1}\subset S_{n+1}$ is obtained from a
particular extended triangulation of $G_{n}$ into the join $S_{n+1}=S_{n}\cup
B$ where $B$ is one of 4 bordered surfaces, namely ${\mathbb{S}}_{0}\backslash
3{\mathbb{D}},{\mathbb{S}}_{0}\backslash 2{\mathbb{D}},{\mathbb{P}}\backslash
2{\mathbb{D}},{\mathbb{S}}_{1}\backslash 2{\mathbb{D}}$. Moreover join takes
place over a single boundary cycle of $G_{n}$ of length $\delta$ say. In the
case of ${\mathbb{S}}_{0}\backslash 3{\mathbb{D}}$ or
${\mathbb{S}}_{0}\backslash 2{\mathbb{D}}$ the extended triangulation is
obtained by a sequence of moves that preserve minimal 3-rigitity, namely
0-extension and vertex splitting. On the other hand the (3,6)-tightness of the
extended triangulation of $G_{n}\subset B$ for the other 2 cases followed from
the substitution lemma, Lemma 4.3 and the sequential construction, by
0-extension and vertex-splitting moves, of the triangulation of $B$ provided
by Lemma 4.4. Thus the minimal 3-rigidity of $G_{n+1}$, and hence the
completion of the induction step, and the proof of the theorem, follows from
Lemma 6.3. ∎

## References

  * [1] L.V. Ahfors and L. Sario, _Riemann surfaces_ , Princeton Univ. Press, Princeton, N.J., 1960.
  * [2] A. Cauchy, Sur les polygones et polyèdres. Second Mémoir. J École Polytechn. 9 (1813) 87-99; Oeuvres. T. 1. Paris 1905, pp. 26-38.
  * [3] J. Cruickshank, D. Kitson and S. C. Power, The generic rigidity of triangulated spheres with blocks and holes, J. Combin. Theory Ser. B 122 (2017), 550-577.
  * [4] J. Cruickshank, D. Kitson and S. C. Power, The rigidity of a partially triangulated torus, Proc. London Math. Soc., 2018, https://doi.org/10.1112/plms.12215
  * [5] M. E. Goldman, An algebraic characterisation of noncompact 2-manifolds, Trans. Amer. Math. Soc., 156 (1971), 241-258.
  * [6] J. Graver, B. Servatius and H. Servatius, _Combinatorial rigidity_ , Graduate Studies in Mathematics, American Mathematical Society, Providence, RI, 1993.
  * [7] J. L Gross and T. W. Tucker, _Topological graph theory_ , Dover, New York, 2001.
  * [8] E. Kastis and S. C. Power, Projective plane graphs and 3-rigidity, arXiv:2003.05514.
  * [9] E. Kastis, D. Kitson and S. C. Power, Coboundary operators for infinite frameworks, Math. Proc. of the Royal Irish Academy, 119A (2019), 93-110.
  * [10] B. Kerékjártó, _Vorlesungen über Topologie_. I, Springer, Berlin, 1923.
  * [11] D. Kitson and S. C. Power, The rigidity of infinite graphs, Discrete Comput Geom 60 (2018), 531-557.
  * [12] D. Kitson and S. C. Power, The rigidity of infinite graphs II. Graphs and Combinatorics 38, 83 (2022).
  * [13] J.C. Maxwell, On the calculation of the equilibrium and stiffness of frames, The London, Edinburgh, and Dublin Philosophical Magazine and Journal of Science 27 (1864), 294-99.
  * [14] B. Mohar and C. Thomassen, _Graphs on surfaces_ , Johns Hopkins University, 2001.
  * [15] S. C. Power, Partially triangulated surfaces and girth constraints, arXiv:2309.10638.
  * [16] I. Richards, On the classification of noncompact surfaces, Trans. Amer. Math. Soc., 106 (1963), 259-269.
  * [17] Q. Shakir, Notes for the talk _Sparsity of surface facegraphs_ , given at the workshop on Graph Rigidity and Applications, Lancaster University, April 2023.
  * [18] C. Thomassen, The Jordan-Schönfleis Theorem and the classification of surfaces, Amer. Math. Monthly., 99 (1992), 116-130.
  * [19] W. Whiteley, Vertex splitting in isostatic frameworks, Structural Topology, 16 (1990), 23-30.


thus $v[r\mapsto 0]_{r\in\emptyset}=v\models\mathit{Inv}(l_{u})$. Now, with
Definition 3 of semantic we it follows that
$(l_{u},v)\xrightarrow{a}(l_{u},v)$ is a transition in $\llbracket
T\backslash\\!\backslash S\rrbracket_{\mathrm{sem}}$. From the state label
renaming function $f$ from Lemma 20 we have that
$q_{2}^{X}=f((l_{u},v))=u=q_{2}^{Y}$. And from Definition 22 of the reduced
$\sim$-quotient of $\llbracket T\backslash\\!\backslash
S\rrbracket_{\mathrm{sem}}$ we have that $q_{1}^{Y}\xrightarrow{a}q_{2}^{Y}$
is a transition in $\llbracket T\backslash\\!\backslash
S\rrbracket_{\mathrm{sem}}^{\rho}=X$.

    9. 9.

$a\in\mathit{Act}_{i}^{T}\cup\mathit{Act}_{o}^{S}$, $q_{1}^{Y}=e$,
$q_{2}^{Y}=e$. Since the source and target states are the error state, it
holds that $q_{1}^{Y},q_{2}^{Y}\notin\mathrm{cons}^{Y}$. Thus this case is not
feasible.

In all feasible cases we can show that $q_{1}^{X}=q_{1}^{Y}$ or
$q_{1}^{X}=((l^{T},l^{S}),v)$ with $v\not\models\mathit{Inv}(l^{S})$ and
$q_{2}^{X}=q_{2}^{Y}$. Since $q_{1}^{Y},q_{2}^{Y}\in\mathrm{cons}^{Y}$ and
$((l^{T},l^{S}),v)\in Q^{X^{\Delta}}$ by construction of $R$, it follows from
Lemma 25 that $q_{1}^{X},q_{2}^{X}\in\mathrm{cons}^{X}$. Therefore, we can
conclude that $q_{1}^{X}\xlongrightarrow{a}{}^{\\!\\!X^{\Delta}}q_{2}^{X}$.
And from the construction of the bisimulation relation $R$ it follows that
$(q_{2}^{X},q_{2}^{Y})\in R$.

  * •

$q_{1}^{Y}\xlongrightarrow{a}{}^{\\!\\!Y^{\Delta}}q_{2}^{Y}$, $q_{2}^{Y}\in
Q^{Y}$, and $a\in\mathit{Act}^{Y}\setminus\mathit{Act}^{X}$. This case is
infeasible, as $\mathit{Act}^{X}=\mathit{Act}^{Y}\cup\\{i_{\mathit{new}}\\}$.

  * •

$q_{1}^{X}\xlongrightarrow{d}{}^{\\!\\!X^{\Delta}}q_{2}^{X}$, $q_{2}^{X}\in
Q^{X}$, and $d\in\mathbb{R}_{\geq 0}$. From Definition 12 of adversarial
pruning we have that $q_{1}^{X}\xlongrightarrow{d}{}^{\\!\\!X}q_{2}^{X}$ and
$q_{1}^{X},q_{2}^{X}\in\mathrm{cons}^{X}$. Following Definition 3 of the
semantic and Definition 22 of the reduced $\sim$-quotient of $\llbracket
T\backslash\\!\backslash S\rrbracket_{\mathrm{sem}}$, it follows that
$q_{1}^{X}=(l_{1},v_{1})$ and $q_{2}^{X}=(l_{1},v_{1}+d)$ with
$l_{1}\in\mathit{Loc}^{T\backslash\\!\backslash S}$,
$v_{1}\in[\mathit{Clk}\mapsto\mathbb{R}_{\geq 0}]$,
$v_{1}+d\models\mathit{Inv}(l_{1})$, and $\forall
d^{\prime}\in\mathbb{R}_{\geq
0},d^{\prime}<d:v_{1}+d^{\prime}\models\mathit{Inv}(l_{1})$. Since
$q_{1}^{X}\in\mathrm{cons}^{X}$, it follows that $l_{1}=(l_{1}^{T},l_{1}^{S})$
or $l_{1}=l_{u}$. Therefore, from Definition 19 of the quotient for TIOA, we
have that and $\mathit{Inv}(l_{1})=\mathbf{T}$. Note that we do not directly
get information about whether the valuation $v_{1}+d$ satisfy the location
invariant in $T$ or $S$.

Now consider first the simple case where $l_{1}=l_{u}$. From Definition 18 of
the quotient for TIOTS, it follows directly that
$u\xlongrightarrow{d}{}^{\\!\\!Y}u$. And note with Lemma 20 that
$q_{2}^{X}=f((l_{u},v_{1}+d))=u=q_{2}^{Y}$ and thus $(q_{2}^{X},q_{2}^{Y})\in
R$.

Now consider the case where $l_{1}=(l_{1}^{T},l_{1}^{S})$. We have to consider
whether delays are possible in $\llbracket T\rrbracket_{\mathrm{sem}}$ and
$\llbracket S\rrbracket_{\mathrm{sem}}$ in order to show that $Y$ can follow
the delay and that the resulting state pair is in the bisimulation relation
$R$.

    * –

$q_{1}^{\llbracket
T\rrbracket_{\mathrm{sem}}}\xlongrightarrow{d}{}^{\\!\\!\llbracket
T\rrbracket_{\mathrm{sem}}}q_{2}^{\llbracket T\rrbracket_{\mathrm{sem}}}$ and
$q_{1}^{\llbracket
S\rrbracket_{\mathrm{sem}}}\xlongrightarrow{d}{}^{\\!\\!\llbracket
S\rrbracket_{\mathrm{sem}}}q_{2}^{\llbracket S\rrbracket_{\mathrm{sem}}}$. In
this case, it follows from Definition 3 of the semantic that
$q_{1}^{\llbracket T\rrbracket_{\mathrm{sem}}}=(l_{1}^{T},v_{1}^{T})$,
$\forall c\in\mathit{Clk}^{T}:v_{1}^{T}(c)=v_{1}(c)$, $q_{2}^{\llbracket
T\rrbracket_{\mathrm{sem}}}=(l_{1}^{T},v_{1}^{T}+d)$,
$v_{1}^{T}+d\models\mathit{Inv}(l_{1}^{T})$, and $\forall
d^{\prime}\in\mathbb{R}_{\geq
0},d^{\prime}<d:v_{1}^{T}+d^{\prime}\models\mathit{Inv}(l_{1}^{T})$; similarly
we have that $q_{1}^{\llbracket
S\rrbracket_{\mathrm{sem}}}=(l_{1}^{S},v_{1}^{S})$, $\forall
c\in\mathit{Clk}^{S}:v_{1}^{S}(c)=v_{1}(c)$, $q_{2}^{\llbracket
S\rrbracket_{\mathrm{sem}}}=(l_{1}^{S},v_{1}^{S}+d)$,
$v_{1}^{S}+d\models\mathit{Inv}(l_{1}^{S})$, and $\forall
d^{\prime}\in\mathbb{R}_{\geq
0},d^{\prime}<d:v_{1}^{S}+d^{\prime}\models\mathit{Inv}(l_{1}^{S})$. From
Definition 18 of the quotient for TIOTS it follows that
$(q_{1}^{T},q_{1}^{S})\xlongrightarrow{d}{}^{\\!\\!Y}(q_{2}^{T},q_{2}^{S})$.
Observe with Lemma 20 that $q_{1}^{Y}=(q_{1}^{\llbracket
T\rrbracket_{\mathrm{sem}}},q_{1}^{\llbracket
S\rrbracket_{\mathrm{sem}}})=(l_{1}^{T},l_{1}^{S},v_{1})=q_{1}^{X}$ and
$q_{2}^{Y}=(q_{2}^{\llbracket T\rrbracket_{\mathrm{sem}}},q_{2}^{\llbracket
S\rrbracket_{\mathrm{sem}}})=(l_{1}^{T},l_{1}^{S},v_{2})=q_{2}^{X}$. Thus
$(q_{2}^{X},q_{2}^{Y})\in R$.

    * –

$q_{1}^{\llbracket
T\rrbracket_{\mathrm{sem}}}\xlongrightarrow{d}{}^{\\!\\!\llbracket
T\rrbracket_{\mathrm{sem}}}q_{2}^{\llbracket T\rrbracket_{\mathrm{sem}}}$ and
$q_{1}^{\llbracket
S\rrbracket_{\mathrm{sem}}}\arrownot\xlongrightarrow{d}{}^{\\!\\!\llbracket
S\rrbracket_{\mathrm{sem}}}$. In this case, it follows from Definition 3 of
the semantic that $q_{1}^{\llbracket
T\rrbracket_{\mathrm{sem}}}=(l_{1}^{T},v_{1}^{T})$, $\forall
c\in\mathit{Clk}^{T}:v_{1}^{T}(c)=v_{1}(c)$, $q_{2}^{\llbracket
T\rrbracket_{\mathrm{sem}}}=(l_{1}^{T},v_{1}^{T}+d)$,
$v_{1}^{T}+d\models\mathit{Inv}(l_{1}^{T})$, and $\forall
d^{\prime}\in\mathbb{R}_{\geq
0},d^{\prime}<d:v_{1}^{T}+d^{\prime}\models\mathit{Inv}(l_{1}^{T})$; similarly
we have that $q_{1}^{\llbracket
S\rrbracket_{\mathrm{sem}}}=(l_{1}^{S},v_{1}^{S})$, $\forall
c\in\mathit{Clk}^{S}:v_{1}^{S}(c)=v_{1}(c)$, and $\exists
d^{\prime}\in\mathbb{R}_{\geq 0},d^{\prime}\leq
d:v_{1}^{S}+d^{\prime}\not\models\mathit{Inv}(l_{1}^{S})$. We have to consider
two cases.

      * *

$v_{1}^{S}\models\mathit{Inv}(l_{1}^{S})$. Since
$\mathit{Clk}^{T}\cap\mathit{Clk}^{S}=\emptyset$,
$v_{1}\models\mathit{Inv}(l_{1}^{S})$. Since $(q_{1}^{X},q_{1}^{Y})\in R$ and
$v_{1}^{S}\models\mathit{Inv}(l_{1}^{S})$, we have that $q_{1}^{Y}=q_{1}^{X}$.
From Definition 18 of the quotient for TIOTS, it follows that
$q_{1}^{Y}=((l_{1}^{T},v_{1}^{T}),(l_{1}^{S},v_{1}^{S}))\xlongrightarrow{d}{}^{\\!\\!Y}u=q_{2}^{Y}$.
From the construction of $R$ we have that $q_{2}^{X}\in A$, thus we can
confirm that $(q_{2}^{T},q_{2}^{Y})\in R$.

      * *

$v_{1}^{S}\not\models\mathit{Inv}(l_{1}^{S})$. Again, since
$\mathit{Clk}^{T}\cap\mathit{Clk}^{S}=\emptyset$,
$v_{1}\not\models\mathit{Inv}(l_{1}^{S})$. Since $(q_{1}^{X},q_{1}^{Y})\in R$
and $v_{1}^{S}\not\models\mathit{Inv}(l_{1}^{S})$, we have that $q_{1}^{X}\in
A$, thus $q_{1}^{Y}=u$. From Definition 18 of the quotient for TIOTS, it
follows that $u\xlongrightarrow{d}{}^{\\!\\!Y}u$. And by construction of $R$
it follows that $(q_{2}^{X},q_{2}^{Y})\in R$.

    * –

$q_{1}^{\llbracket
T\rrbracket_{\mathrm{sem}}}\arrownot\xlongrightarrow{d}{}^{\\!\\!\llbracket
T\rrbracket_{\mathrm{sem}}}q_{2}^{\llbracket T\rrbracket_{\mathrm{sem}}}$ and
$q_{1}^{\llbracket
S\rrbracket_{\mathrm{sem}}}\arrownot\xlongrightarrow{d}{}^{\\!\\!\llbracket
S\rrbracket_{\mathrm{sem}}}$. This case follows the exact same reasoning as
the one above, since Definition 18 of the quotient for TIOTS does not care
whether a delay $d$ is possible in $\llbracket T\rrbracket_{\mathrm{sem}}$
once it is not possible in $\llbracket S\rrbracket_{\mathrm{sem}}$.

    * –

$q_{1}^{\llbracket
T\rrbracket_{\mathrm{sem}}}\arrownot\xlongrightarrow{d}{}^{\\!\\!\llbracket
T\rrbracket_{\mathrm{sem}}}q_{2}^{\llbracket T\rrbracket_{\mathrm{sem}}}$ and
$q_{1}^{\llbracket
S\rrbracket_{\mathrm{sem}}}\xlongrightarrow{d}{}^{\\!\\!\llbracket
S\rrbracket_{\mathrm{sem}}}q_{2}^{\llbracket S\rrbracket_{\mathrm{sem}}}$. In
this case, it follows directly from Definition 18 of the quotient for TIOTS
that there is no delay possible in $Y$, i.e., $(q_{1}^{\llbracket
T\rrbracket_{\mathrm{sem}}},q_{1}^{\llbracket
S\rrbracket_{\mathrm{sem}}})\arrownot\xlongrightarrow{d}{}^{\\!\\!\llbracket
T\rrbracket_{\mathrm{sem}}\backslash\\!\backslash\llbracket
S\rrbracket_{\mathrm{sem}}}$. It follows from Definition 3 of the semantic
that $q_{1}^{\llbracket T\rrbracket_{\mathrm{sem}}}=(l_{1}^{T},v_{1}^{T})$,
$\forall c\in\mathit{Clk}^{T}:v_{1}^{T}(c)=v_{1}(c)$, and $\exists
d^{\prime}\in\mathbb{R}_{\geq 0},d^{\prime}\leq
d:v_{1}^{T}+d^{\prime}\not\models\mathit{Inv}(l_{1}^{T})$; similarly we have
that $q_{1}^{\llbracket S\rrbracket_{\mathrm{sem}}}=(l_{1}^{S},v_{1}^{S})$,
$\forall c\in\mathit{Clk}^{S}:v_{1}^{S}(c)=v_{1}(c)$, $q_{2}^{\llbracket
S\rrbracket_{\mathrm{sem}}}=(l_{1}^{S},v_{1}^{S}+d)$,
$v_{1}^{S}+d\models\mathit{Inv}(l_{1}^{S})$, and $\forall
d^{\prime}\in\mathbb{R}_{\geq
0},d^{\prime}<d:v_{1}^{S}+d^{\prime}\models\mathit{Inv}(l_{1}^{S})$. Without
loss of generality, we can assume that
$v_{1}^{T}+0\not\models\mathit{Inv}(l_{1}^{T})$181818In case there would be a
$d^{\prime}<d$ such that $v_{1}^{T}+d^{\prime}\models\mathit{Inv}(l_{1}^{T})$,
we can use the first case to simulate the delay $d^{\prime}$ in$Y$., which
simplifies to $v_{1}^{T}\not\models\mathit{Inv}(l_{1}^{T})$. Combining this
information, we have that
$v_{1}\models\neg\mathit{Inv}(l_{1}^{T})\wedge\mathit{Inv}(l_{1}^{S})$, where
we used the fact that $\mathit{Clk}^{T}\cap\mathit{Clk}^{S}=\emptyset$. Now,
using Definition 19 of the quotient for TIOA and Definition 3 of the
semantics, we have that
$(l_{1}^{T},l_{1}^{S},v_{1})\xlongrightarrow{i_{\mathit{new}}}{}^{\\!\\!\llbracket
T\backslash\\!\backslash S\rrbracket_{\mathrm{sem}}}(l_{e},v_{1})$. Since
$(l_{e},v_{1})\notin\mathrm{cons}^{X}$ and $i_{\mathit{new}}$ is an input, it
follows that $(l_{1}^{T},l_{1}^{S},v_{1})=q_{1}^{X}\notin\mathrm{cons}^{X}$.
This contradicts with our assumption that $q_{1}^{X}\in\mathrm{cons}^{X}$.
Therefore, this case is infeasible.

In all feasible cases we can show that $(q_{2}^{X},q_{2}^{Y})\in R$. Since
$q_{1}^{X},q_{2}^{X}\in\mathrm{cons}^{X}$ and $A\subseteq Q^{X^{\Delta}}$ by
construction of $R$, it follows from Lemma 25 that
$q_{1}^{Y},q_{2}^{Y}\in\mathrm{cons}^{Y}$. Therefore, we can conclude that
$q_{1}^{Y}\xlongrightarrow{d}{}^{\\!\\!Y^{\Delta}}q_{2}^{Y}$.

  * •

$q_{1}^{Y}\xlongrightarrow{d}{}^{\\!\\!Y^{\Delta}}q_{2}^{Y}$, $q_{2}^{Y}\in
Q^{Y}$, and $d\in\mathbb{R}_{\geq 0}$. From Definition 12 of adversarial
pruning we have that $q_{1}^{Y}\xlongrightarrow{d}{}^{\\!\\!Y}q_{2}^{Y}$ and
$q_{1}^{Y},q_{2}^{Y}\in\mathrm{cons}^{Y}$. Consider the following three cases
from Definition 18 of the quotient for TIOTS.

    * –

$q_{1}^{Y}=(q_{1}^{\llbracket T\rrbracket_{\mathrm{sem}}},q_{1}^{\llbracket
S\rrbracket_{\mathrm{sem}}})$, $q_{2}^{Y}=(q_{2}^{\llbracket
T\rrbracket_{\mathrm{sem}}},q_{2}^{\llbracket S\rrbracket_{\mathrm{sem}}})$,
$q_{1}^{\llbracket
T\rrbracket_{\mathrm{sem}}}\xlongrightarrow{d}{}^{\\!\\!\llbracket
T\rrbracket_{\mathrm{sem}}}q_{2}^{\llbracket T\rrbracket_{\mathrm{sem}}}$, and
$q_{1}^{\llbracket
S\rrbracket_{\mathrm{sem}}}\xlongrightarrow{d}{}^{\\!\\!\llbracket
S\rrbracket_{\mathrm{sem}}}q_{2}^{\llbracket S\rrbracket_{\mathrm{sem}}}$.
From Definition 3 of the semantic it follows that $q_{1}^{\llbracket
T\rrbracket_{\mathrm{sem}}}=(l_{1}^{T},v_{1}^{T})$, $q_{2}^{\llbracket
T\rrbracket_{\mathrm{sem}}}=(l_{1}^{T},v_{1}^{T}+d)$,
$v_{1}^{T}+d\models\mathit{Inv}(l_{1}^{T})$, $\forall
d^{\prime}\in\mathbb{R}_{\geq
0},d^{\prime}<d:v_{1}^{T}+d^{\prime}\models\mathit{Inv}(l_{1}^{T})$,
$q_{1}^{\llbracket S\rrbracket_{\mathrm{sem}}}=(l_{1}^{S},v_{1}^{S})$,
$q_{2}^{\llbracket S\rrbracket_{\mathrm{sem}}}=(l_{1}^{S},v_{1}^{S}+d)$,
$v_{1}^{S}+d\models\mathit{Inv}(l_{1}^{S})$, and $\forall
d^{\prime}\in\mathbb{R}_{\geq
0},d^{\prime}<d:v_{1}^{S}+d^{\prime}\models\mathit{Inv}(l_{1}^{S})$. Now, from
Definition 19 of the quotient for TIOA we have that
$\mathit{Inv}((l_{1}^{S},l_{1}^{T}))=\mathbf{T}$ in $T\backslash\\!\backslash
S$, thus using Definitions 3 and 22 we have
$q_{1}^{X}=(l_{1}^{S},l_{1}^{T},v_{1})\xlongrightarrow{d}{}^{\\!\\!X}(l_{1}^{S},l_{1}^{T},v_{1}+d)=q_{2}^{X}$.
Observe that $q_{1}^{X}=q_{1}^{Y}$ and $q_{2}^{X}=q_{2}^{Y}$, thus
$q_{2}^{X},q_{2}^{Y}\in R$.

    * –

$q_{1}^{Y}=(q_{1}^{\llbracket T\rrbracket_{\mathrm{sem}}},q_{1}^{\llbracket
S\rrbracket_{\mathrm{sem}}})$, $q_{2}^{Y}=u$, and $q_{1}^{\llbracket
S\rrbracket_{\mathrm{sem}}}\arrownot\xlongrightarrow{d}{}^{\\!\\!\llbracket
S\rrbracket_{\mathrm{sem}}}q_{2}^{\llbracket S\rrbracket_{\mathrm{sem}}}$.
From Definition 3 of the semantic it follows that $q_{1}^{\llbracket
T\rrbracket_{\mathrm{sem}}}=(l_{1}^{T},v_{1}^{T})$, $q_{1}^{\llbracket
S\rrbracket_{\mathrm{sem}}}=(l_{1}^{S},v_{1}^{S})$, and $\exists
d^{\prime}\in\mathbb{R}_{\geq 0},d^{\prime}\leq
d:v_{1}^{S}+d^{\prime}\not\models\mathit{Inv}(l_{1}^{S})$. Now, from
Definition 19 of the quotient for TIOA we have that
$\mathit{Inv}((l_{1}^{S},l_{1}^{T}))=\mathbf{T}$ in $T\backslash\\!\backslash
S$, thus using Definitions 3 and 22 we have
$q_{1}^{X}=(l_{1}^{S},l_{1}^{T},v_{1})\xlongrightarrow{d}{}^{\\!\\!X}(l_{1}^{S},l_{1}^{T},v_{1}+d)=q_{2}^{X}$.
We have to consider two cases to show that $(q_{2}^{X},q_{2}^{Y})\in R$.

      * *

$v_{1}^{S}\models\mathit{Inv}(l_{1}^{S})$. In this case $q_{1}^{X}\notin A$
and $q_{2}^{X}\in A$. Therefore, $(q_{2}^{X},q_{2}^{Y})\in R$.

      * *

$v_{1}^{S}\not\models\mathit{Inv}(l_{1}^{S})$. In this case
$q_{1}^{X},q_{2}^{X}\in A$. From the construction of $R$ it follows that any
state from $A$ can only be related to state $u$ in $Y$, but
$q_{1}^{Y}=(q_{1}^{\llbracket T\rrbracket_{\mathrm{sem}}},q_{1}^{\llbracket
S\rrbracket_{\mathrm{sem}}})$. This contradiction renders this case
infeasible.

    * –

$q_{1}^{Y}=u$ and $q_{2}^{Y}=u$. From Definition 19 of the quotient for TIOA,
it follows directly that $(l_{u},v)\
{\xlongrightarrow{d}{}^{\\!\\!X}}\allowbreak(l_{u},v)$ for any
$v\in[\mathit{Clk}\mapsto\mathbb{R}_{\geq 0}]$. And note with Lemma 20 that
$q_{1}^{X}=q_{2}^{X}=f((l_{u},v))=u=q_{1}^{Y}=q_{2}^{Y}$ and thus
$(q_{2}^{X},q_{2}^{Y})\in R$.

In all feasible cases we can show that $(q_{2}^{X},q_{2}^{Y})\in R$. Since
$q_{1}^{Y},q_{2}^{Y}\in\mathrm{cons}^{Y}$ and $A\subseteq Q^{X^{\Delta}}$ by
construction of $R$, it follows from Lemma 25 that
$q_{1}^{X},q_{2}^{X}\in\mathrm{cons}^{X}$. Therefore, we can conclude that
$q_{1}^{X}\xlongrightarrow{d}{}^{\\!\\!X^{\Delta}}q_{2}^{X}$.

We have show for state pair $(q_{1}^{X},q_{1}^{Y})\in R$ that all the six
cases of bisimulation hold. Since we have chosen an arbitrary state pair from
$R$, it holds for all state pairs in $R$. This concludes the proof.

## References

  *   * (1) Henzinger, T.A., Sifakis, J.: The embedded systems design challenge. In: International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 4085, pp. 1–15. Springer, Berlin, Heidelberg (2006). https://doi.org/10.1007/11813040_1
  * (2) Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J.-B., Reinkemeier, P., Sangiovanni-Vincentelli, A., Damm, W., Henzinger, T.A., Larsen, K.G.: Contracts for System Design vol. 12, pp. 124–400 (2018). https://doi.org/10.1561/1000000053
  * (3) de Alfaro, L., Henzinger, T.A.: Interface-based design. In: Engineering Theories of Software Intensive Systems. NATO Science Series, vol. 195, pp. 83–104. Springer, Dordrecht (2005). https://doi.org/10.1007/1-4020-3532-2_3
  * (4) Chakabarti, A., de Alfaro, L., Henzinger, T.A., Stoelinga, M.I.A.: Resource interfaces. In: Proceedings of the International Workshop on Embedded Software. Lecture Notes in Computer Science, vol. 2855, pp. 117–133. Springer, Berlin, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45212-6_9
  * (5) de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings of the Annual Symposium on Foundations of Software Engineering, pp. 109–120. ACM Press, New York, NY (2001). https://doi.org/10.1145/503209.503226
  * (6) Larsen, K.G.: Modal specifications. In: Automatic Verification Methods for Finite State Systems. Lecture Notes in Computer Science, vol. 407, pp. 232–246. Springer, Berlin, Heidelberg (1989). https://doi.org/10.1007/3-540-52148-8_19
  * (7) Milner, R.: Communication and Concurrency. Prentice Hall, USA (1989)
  * (8) Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. Technical Report MIT/LCS/TM-373, The MIT Press (1988)
  * (9) de Alfaro, L., Henzinger, T.A., Stoelinga, M.I.A.: Timed interfaces. In: Proceedings of the International Workshop on Embedded Software. Lecture Notes in Computer Science, vol. 2491, pp. 108–122. Springer, Berlin, Heidelberg (2002). https://doi.org/10.1007/3-540-45828-X_9
  * (10) de Alfaro, L., Faella, M.: An accelerated algorithm for 3-color parity games with an application to timed games. In: Proceedings of the International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 4590, pp. 108–120. Springer, Berlin, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_13
  * (11) Bertrand, N., Pinchinat, S., Raclet, J.-B.: Refinement and consistency of timed modal specifications. In: Proceedings of the International Conference on Language and Automata Theory and Applications. Lecture Notes in Computer Science, vol. 5457, pp. 152–163. Springer, Berlin, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00982-2_13
  * (12) Bertrand, N., Legay, A., Pinchinat, S., Raclet, J.-B.: A compositional approach on modal specifications for timed systems. In: Proceedings of International Conference on Formal Engineering Methods. Lecture Notes in Computer Science, vol. 5885, pp. 679–697. Springer, Berlin, Heidelberg (2009). https://doi.org/10.1007/978-3-642-10373-5_35
  * (13) Čerāns, K., Godskesen, J.C., Larsen, K.G.: Timed modal specification - theory and tools. In: Proceedings of the International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 697, pp. 253–267. Springer, Berlin, Heidelberg (1993). https://doi.org/10.1007/3-540-56922-7_21
  * (14) Thiele, L., Wandeler, E., Stoimenov, N.: Real-time interfaces for composing real-time systems. In: Proceedings of the ACM & IEEE International Conference on Embedded Software, pp. 34–43. ACM, New York, NY, USA (2006). https://doi.org/10.1145/1176887.1176894
  * (15) Lee, I., Leung, J.Y.-T., Son, S.H.: Handbook of Real-Time and Embedded Systems. Chapman, New York, NY, USA (2007). https://doi.org/10.1201/9781420011746
  * (16) Hampus, A., Nyberg, M.: Formally verifying decompositions of stochastic specifications. In: Groote, J.F., Huisman, M. (eds.) Formal Methods for Industrial Critical Systems. Lecture Notes in Computer Science, pp. 193–210. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-15008-1_13
  * (17) Kaynar, D.K., Lynch, N.A., Segala, R., Vaandrager, F.W.: Timed i/o automata: A mathematical framework for modeling and analyzing real-time systems. In: Proceedings of the IEEE Real-Time Systems Symposium, pp. 166–177 (2003). https://doi.org/10.1109/REAL.2003.1253264
  * (18) Bellman, R.: Dynamic Programming. Princeton University Press, New Jersey (1957)
  * (19) Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems, pp. 197–212. Springer, Berlin, Heidelberg (1990). https://doi.org/10.1007/3-540-52148-8_17
  * (20) Behrmann, G., Bengtsson, J., David, A., Larsen, K.G., Pettersson, P., Yi, W.: UppaaL implementation secrets. In: Damm, W., Olderog, E.-R. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems. Lecture Notes in Computer Science, pp. 3–22. Springer, Berlin, Heidelberg (2002). https://doi.org/10.1007/3-540-45739-9_1
  * (21) Larsen, K.G., Nyman, U., Wasowski, A.: Modal I/O automata for interface and product line theories. In: Proceedings of the European Symposium on Programming. Lecture Notes in Computer Science, vol. 4421, pp. 64–79. Springer, Berlin, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71316-6_6
  * (22) Bulychev, P., Chatain, T., David, A., Larsen, K.G.: Efficient on-the-fly algorithm for checking alternating timed simulation. In: Proceedings of the International Conference on Formal Modeling and Analysis of Timed Systems. Lecture Notes in Computer Science, vol. 5813, pp. 73–87. Springer, Berlin, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04368-0_8
  * (23) David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed i/o automata: a complete specification theory for real-time systems. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control. HSCC ’10, pp. 91–100. Association for Computing Machinery. https://doi.org/10.1145/1755952.1755967
  * (24) David, A., Larsen, K.G., Legay, A., Nyman, U., Wąsowski, A.: Methodologies for specification of real-time systems using timed i/o automata. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) Formal Methods for Components and Objects. Lecture Notes in Computer Science, pp. 290–310. Springer. https://doi.org/10.1007/978-3-642-17071-3_15
  * (25) David, A., Larsen, K.G., Legay, A., Nyman, U., Traonouez, L.-M., Wąsowski, A.: Real-time specifications. International Journal on Software Tools for Technology Transfer 17(1), 17–45 (2015). https://doi.org/10.1007/s10009-013-0286-x
  * (26) Henzinger, T.A., Manna, Z., Pnueli, A.: Timed transition systems. In: REX Workshop. Lecture Notes in Computer Science, vol. 600, pp. 226–251. Springer, Berlin, Heidelberg (1991). https://doi.org/10.1007/BFb0031995
  * (27) Lynch, N.: I/O automata: A model for discrete event systems. In: Annual Conference on Information Sciences and Systems, Princeton University, Princeton, N.J., pp. 29–38 (1988)
  * (28) Garland, S.J., Lynch, N.A.: The IOA language and toolset: Support for designing, analyzing, and building distributed systems. Technical report, Massachusetts Institute of Technology, Cambridge, MA (1998)
  * (29) Stark, E.W., Cleavland, R., Smolka, S.A.: A process-algebraic language for probabilistic I/O automata. In: Proceedings of the International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 2761, pp. 193–207. Springer, Berlin, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45187-7_13
  * (30) Vaandrager, F.W.: On the relationship between process algebra and input/output automata. In: Proceedings Annual IEEE Symposium on Logic in Computer Science, pp. 387–398 (1991). https://doi.org/10.1109/LICS.1991.151662
  * (31) Nicola, R.D., Segala, R.: A process algebraic view of input/output automata. Theoretical Computer Science 138(2), 391–423 (1995). https://doi.org/10.1016/0304-3975(95)92307-J
  * (32) de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003 - Concurrency Theory. Lecture Notes in Computer Science, pp. 144–158. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45187-7_9
  * (33) Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.: Alternating refinement relations. In: Proceedings of the International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 1466, pp. 163–178. Springer, Berlin, Heidelberg (1998). https://doi.org/10.1007/BFb0055622
  * (34) Caillaud, B., Delahaye, B., Larsen, K.G., Legay, A., Peddersen, M., Wasowski, A.: Compositional design methodology with constraint markov chains. Technical report, Hal-INRIA (2009)
  * (35) Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Proceedings of the International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 3653, pp. 66–80. Springer, Berlin, Heidelberg (2005). https://doi.org/10.1007/11539452_9
  * (36) de Alfaro, L., Henzinger, T.A., Majumdar, R.: Symbolic algorithms for infinite-state games. In: Proceedings of the International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 2154, pp. 536–550. Springer, Berlin, Heidelberg (2001). https://doi.org/10.1007/3-540-44685-0_36
  * (37) Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems (an extended abstract). In: Proceedings of the Annual Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 900, pp. 229–242. Springer, Berlin, Heidelberg (1995). https://doi.org/10.1007/3-540-59042-0_76
  * (38) Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5, 285–309 (1955)
  * (39) Berendsen, J., Vaandrager, F.W.: Compositional abstraction in real-time model checking. In: Proceedings of the International Conference on Formal Modeling and Analysis of Timed Systems. Lecture Notes in Computer Science, vol. 5215, pp. 233–249. Springer, Berlin, Heidelberg (2008). https://doi.org/10.1007/978-3-540-85778-5_17
  * (40) Deng, Z., Liu, J.W.-s.: Scheduling real-time applications in an open environment. In: Proceedings of the IEEE Real-Time Systems Symposium, pp. 308–319 (1997). https://doi.org/10.1109/REAL.1997.641292