TU Braunschweig, Germany<EMAIL_ADDRESS>TU Braunschweig, Germany
<EMAIL_ADDRESS>Eren Keskin and Roland Meyer <ccs2012> <concept>
<concept_id>10003752.10003766</concept_id> <concept_desc>Theory of computation
Formal languages and automata theory</concept_desc>
<concept_significance>500</concept_significance> </concept> <concept>
<concept_id>10003752.10003766.10003776</concept_id> <concept_desc>Theory of
computation Regular languages</concept_desc>
<concept_significance>500</concept_significance> </concept> <concept>
<concept_id>10003752.10003753.10003761.10003762</concept_id>
<concept_desc>Theory of computation Parallel computing models</concept_desc>
<concept_significance>500</concept_significance> </concept> </ccs2012>
[500]Theory of computation Formal languages and automata theory [500]Theory of
computation Regular languages [500]Theory of computation Parallel computing
models. This work was supported by the DFG project EDS@SYN: Effective
Denotational Semantics for Synthesis.

# Separability and Non-Determinizability of WSTS

Eren Keskin  Roland Meyer

###### Abstract

There is a recent separability result for the languages of well-structured
transition systems (WSTS) that is surprisingly general: disjoint WSTS
languages are always separated by a regular language. The result assumes that
one of the languages is accepted by a deterministic WSTS, and it is not known
whether this assumption is needed. There are two ways to get rid of the
assumption, none of which has led to conclusions so far: (i) show that WSTS
can be determinized or (ii) generalize the separability result to non-
deterministic WSTS languages. Our contribution is to show that (i) does not
work but (ii) does. As for (i), we give a non-deterministic WSTS language that
we prove cannot be accepted by a deterministic WSTS. The proof relies on a
novel characterization of the languages accepted by deterministic WSTS. As for
(ii), we show how to find finitely represented inductive invariants without
having the tool of ideal decompositions at hand. Instead, we work with
closures under converging sequences. Our results hold for upward- and
downward-compatible WSTS.

###### keywords:

WSTS, regular separability, determinization.

##  1 Introduction

Czerwinski et al. [16, Theorems 6 and 7] have recently established a
separability result for the languages of well-structured transition systems
(WSTS) [20, 4, 2, 23] that is surprisingly general. Disjoint WSTS languages
are always separated by a regular language: whenever we have
$\mathit{L}(\mathit{U})\cap\mathit{L}(\mathit{V})=\emptyset$, then there is a
regular language $R$ with $\mathit{L}(\mathit{U})\subseteq R$ and
$R\cap\mathit{L}(\mathit{V})=\emptyset$. The result says that WSTS languages
either intersect, or they are far apart in that a finite amount of information
is sufficient to distinguish them. Applications abound, we elaborate on this
in the related work. Unfortunately, the result comes with a grain of salt: it
assumes that one of the WSTS, $\mathit{U}$ or $\mathit{V}$, is deterministic.
All attempts to remove the assumption have failed so far. The assumption is
used for a central argument in the proof, namely that inductive invariants can
be represented in a finite way. With determinism, these invariants are
downward-closed sets in a WQO, and hence decompose into finitely many ideals
[32, 21, 22]. This is precisely the finite amount of information needed for
regularity.

A strategy to circumvent the assumption would be to show that WSTS can be
determinized. Czerwinsky et al. already argue in this direction. In [16,
Theorem 5], they show that both finitely-branching WSTS and WSTS over so-
called $\omega^{2}$-WQOs can be determinized. Unfortunately, this does not
cover all WSTS. To sum up, it is still open whether the regular separability
result holds for all WSTS languages, and we do not understand the impact of
non-determinism on the expressiveness of the WSTS model.

Our first contribution is to prove the regular separability result for all
WSTS languages, without the assumption of determinism. We accept the fact that
determinizing a WSTS no longer yields a WSTS, and carefully study the
resulting class of transition systems. They are formed over a lattice in which
sequences have subsequences that converge in a natural sense. This leads us to
define the closure of a set by adding the limits of all converging sequences.
The key insight is that the closure of an inductive invariant is again an
inductive invariant. Together with the fact that closed sets have finitely
many maximal elements, we arrive at the desired finite representation. In
short, when moving from WQOs to converging lattices, maximal elements of
closed sets form an alternative to ideal decompositions of downward-closed
sets. We call the new transition systems converging.

Our second contribution is to show that WSTS cannot be determinized in
general. We give a WSTS language $T$ that we prove cannot be accepted by a
deterministic WSTS. The proof relies on a novel characterization of the
deterministic WSTS languages: they are precisely the languages whose Nerode
(right) quasi order is a WQO. The characterization provides a first hint on
how to construct $T$. The language should have an infinite antichain in the
Nerode quasi order, for then this cannot be a WQO. The second hint stems from
the determinizability result [16, Theorem 5]. The accepting WSTS should be
infinitely branching and the WQO should be no $\omega^{2}$-WQO. Such WQOs
embed the so-called Rado WQO [8, Section 2]. Moreover, the Rado WQO is known
to have an infinite antichain when constructing downward-closed sets [22,
Proposition 4.2]. The definition of $T$ is thus guided by the idea of
translating the Rado antichain into an antichain in the Nerode quasi order.
Interestingly, the underlying WSTS is deterministic except for the choice of
the initial state.

We develop these results for upward-compatible WSTS [23]. Our third
contribution is to show that they also hold for downward-compatible WSTS. We
achieve this by proving general relationships between the models. A key
insight is that the complement of a deterministic upward-compatible WSTS is a
deterministic downward-compatible WSTS. Moreover, the reversal of an upward-
compatible WSTS language is a downward-compatible WSTS language.

#### Related Work

The converging transition systems (CTS) we use to generalize the regular
separability result [16] have a topological flavor, and indeed are inspired by
Goubault-Larrecq’s Noetherian transition systems [26, 27]. One difference is
that we had to formulate CTS in lattice-theoretic terms to be able to import a
theorem from [16] that links regular separability to the existence of finitely
represented inductive invariants. Another difference is the study of such
invariants (we prove stability under closure) that has no analogue in [26,
27].

We show that deterministic WSTS accept a strictly weaker class of languages
than their non-deterministic counterparts. The work [3] also compares classes
of WSTS languages, but for fixed models (extended Petri nets). We allow the
determinization to freely select the WQO and the transitions, meaning we have
considerably less syntactic constraints to work with. There are also pumping
lemmas to distinguish WSTS languages from (among others) context-free
languages [24]. Our characterization of the deterministic WSTS languages is
stronger than the necessary conditions in pumping lemmas. Our language
witnessing the weakness of deterministic WSTS is accepted by an infinitely-
branching WSTS, a class of systems studied in [7]. That work concentrates on
decidability results and pays attention to effectiveness, while we prove a
statement of existence and do not need such assumptions.

There is recent interest in separability problems for infinite-state systems
[17, 41, 14, 40, 12]. One reason is that standard algorithms rarely apply to
separability problems, but these problems tend to call for new approaches.
With the basic separator technique [18], Czerwinski and Zetzsche have shown
that there is hope for general methods that apply to a range of separability
problems [10, 11, 15]. With the closure of inductive invariants under
converging sequences, we hope to also have contributed a versatile tool.

Another reason for the popularity of separability problems is their usefulness
in verification. In [1], separators act as interpolants in abstraction-guided
verification [9]. In [6], separators are advocated as interfaces in rely-
guarantee reasoning [31]. In this context, our result implies that regular
interfaces yield a complete proof method, provided the system is well-
structured.

##  2 Well-Structured Transition Systems

We recall well-structured transition systems (WSTS) with upward compatibility
[20, 4, 2, 23]. Downward compatibility will be addressed in Section 5.

#### Orders

Let $(Q,\leq)$ be a quasi order and $P\subseteq Q$. We call $P$ a chain, if
$\leq$ restricted to $P$ is a total order. We call $P$ an antichain, if the
elements in $P$ are pairwise incomparable. The upward closure of $P$ is
$\mathord{\uparrow}P=\\{q\in Q\mid\exists p\in P.\ p\leq q\\}$. We call $P$
upward closed, if $P=\mathord{\uparrow}P$. The powerset of $Q$ restricted to
the upward-closed sets is $\mathbb{U}(Q)$. The downward closure is defined
similarly and we use $\mathbb{D}(Q)$ for the downward closed sets. We call
$(Q,\leq)$ a well quasi order (WQO), if for every infinite sequence
$[p_{i}]_{i\in{\rm Nature}}$ in $Q$ there are indices $i<j$ with $p_{i}\leq
p_{j}$.

Let $(Q,\leq)$ be a partially-ordered set. We write $\max P$ for the set of
maximal elements in the subset $P\subseteq Q$. They may not exist, in which
case the set is empty. We call $(Q,\leq)$ a complete lattice, if all
$P\subseteq Q$ have a greatest lower bound in $Q$, also called meet and
denoted by
$\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}P\in
Q$, and a least upper bound in $Q$, also called join and denoted by $\bigsqcup
P\in Q$. A function $f:Q\rightarrow Q$ on the complete lattice is Scott
continuous [39], if it distributes over arbitrary joins in that $f(\bigsqcup
P)=\bigsqcup f(P)$ for all $P\subseteq Q$, where $f(P)=\\{f(p)\mid p\in P\\}$.
We call $(Q,\leq)$ a completely distributive lattice, if it is a complete
lattice where arbitrary meets distribute over arbitrary joins, and vice versa:

$\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{a\in
A}\bigsqcup_{b\in B_{a}}p_{a,b}=\bigsqcup_{f\in
C_{A,B}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{a\in
A}p_{a,f(a)}\qquad\bigsqcup_{a\in
A}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{b\in
B_{a}}p_{a,b}=\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{f\in
C_{A,B}}\bigsqcup_{a\in A}p_{a,f(a)}\ .$

The definition makes use of the Axiom of Choice: $C_{A,B}$ denotes the set of
choice functions that map each $a\in A$ to a choice $b\in B_{a}$. It is also
important to note that, for any set $Q$, $(\mathbb{D}(Q),\subseteq)$ is a
completely distributive lattice.

#### Labeled Transition Systems

A labeled transition system (LTS) is a tuple
$\mathit{U}=(Q,I,\Sigma,\delta,F)$ that consists of a set of states $Q$, in
our setting typically infinite, a set of inital states $I\subseteq Q$, a set
of final states $F\subseteq Q$, a finite alphabet $\Sigma$, and a set of
labeled transitions $\delta:Q\times\Sigma\rightarrow\mathbb{P}(Q)$. The LTS is
deterministic, if $|{I}|=|{\delta(p,a)}|=1$ for all $p\in Q$ and $a\in\Sigma$.
Its language is the set of words that can reach a final state from an initial
state:

$\mathit{L}(\mathit{U})=\\{w\in\Sigma^{*}\mid\delta(I,w)\cap
F\neq\emptyset\\}.$

Here, we extend the transition relation to sets of states and words:
$\delta(P,w.a)=\delta(\delta(P,w),a)$ and $\delta(P,a)=\bigcup_{p\in
P}\delta(p,a)$.

Let $\mathit{U}_{1}$ and $\mathit{U}_{2}$ be LTS with
$\mathit{U}_{i}=(Q_{i},I_{i},\Sigma,\delta_{i},F_{i})$. We define their
synchronized product to be the LTS
$\mathit{U}_{1}\times\mathit{U}_{2}=(Q_{1}\times Q_{2},I_{1}\times
I_{2},\Sigma,\delta,F_{1}\times F_{2})$ where
$(q_{1},q_{2})\in\delta((p_{1},p_{2}),a)$, if $q_{1}\in\delta_{1}(p_{1},a)$
and $q_{2}\in\delta_{2}(p_{2},a)$. Then
$\mathit{L}(\mathit{U}_{1}\times\mathit{U}_{2})=\mathit{L}(\mathit{U}_{1})\cap\mathit{L}(\mathit{U}_{2})$.

#### Compatibility

We work with LTS $\mathit{U}=(Q,I,\Sigma,\delta,F)$ whose states form a quasi
order $(Q,\leq)$ that is compatible with the remaining components as follows.
We have $F=\mathord{\uparrow}F$, the final states are upward closed wrt.
$\leq$. Moreover, $\leq$ is a simulation relation [36]: for all pairs of
related states $p_{1}\leq q_{1}$ and for all letters $a\in\Sigma$ we have:

$\text{for all }p_{2}\in\delta(p_{1},a)\text{ there is
}q_{2}\in\delta(q_{1},a)\text{ with }p_{2}\leq q_{2}.$

We also make the quasi order explicit and call
$\mathit{U}=(Q,\leq,I,\Sigma,\delta,F)$ an _upward-compatible_ LTS (ULTS).

ULTS can be determinized, in the case of $\mathit{U}$ this yields

$\mathit{U}^{\mathit{det}}\quad=\quad(\mathbb{D}(Q),\subseteq,\mathord{\downarrow}I,\Sigma,\delta^{\mathit{det}},F^{\mathit{det}})\
.$

The states are the downward-closed sets ordered by inclusion, the transition
relation is defined by closing the result of the original transition relation
downwards, $\delta^{\mathit{det}}(D,a)=\mathord{\downarrow}\delta(D,a)$ for
all $D\in\mathbb{D}(Q)$ and $a\in\Sigma$, and final are all downward-closed
sets that contain a final state in the original ULTS,
$F^{\mathit{det}}=\\{D\in\mathbb{D}(Q)\mid D\cap F\neq\emptyset\\}$.

######  Lemma 2.1.

Let $\mathit{U}$ be an ULTS. Then $\mathit{U}^{\mathit{det}}$ is a
deterministic ULTS with
$\mathit{L}(\mathit{U}^{\mathit{det}})=\mathit{L}(\mathit{U})$.

We write detULTS for the class of deterministic ULTS. The synchronized product
of ULTS is again an ULTS (with the product order).

#### Well-Structuredness

An _upward-compatible well-structured transition system_ (WSTS) is an ULTS
$\mathit{U}$ whose states $(Q,\leq)$ form a WQO. The synchronized product of
WSTS is again a WSTS. We are interested in $\mathit{L}(\text{WSTS})$, the
class of all languages accepted by WSTS. We also study
$\mathit{L}(\text{detWSTS})\subseteq\mathit{L}(\text{WSTS})$, the class of
languages accepted by deterministic WSTS.

We observe that we can focus on WSTS with a countable number of states.

######  Lemma 2.2.

For every $L\in\mathit{L}(\text{WSTS})$ there is a WSTS $\mathit{U}$ with a
countable number of states so that $L=\mathit{L}(\mathit{U})$.

The lemma needs two arguments: the language consists of a countable number of
words, and we can assume the transition relation to yield downward-closed
sets. The proof can be found in the appendix.

##  3 Regular Separability of WSTS Languages

Two languages $L_{1},L_{2}\subseteq\Sigma^{*}$ are _separable by a regular
language_ , denoted by $L_{1}\mathop{|}L_{2}$, if there is a regular language
$R\subseteq\Sigma^{*}$ with $L_{1}\subseteq R$ and $R\cap L_{2}=\emptyset$.
Our main result is that disjoint WSTS languages are always separable in this
sense.

######  Theorem 3.1.

For $L_{1},L_{2}\in\mathit{L}(\text{WSTS})$, we have $L_{1}\mathop{|}L_{2}$ if
and only if $L_{1}\cap L_{2}=\emptyset$.

This is the same as the main theorem in [16], but does not need the premise
that one of the languages is accepted by a deterministic WSTS. The implication
from left to right is trivial, the implication from right to left is our first
contribution.

###  3.1 Proof Principle for Regular Separability

To establish regular separability, we rely on a proof principle introduced in
[16]. The notion of an inductive invariant will be recalled in a moment.

######  Theorem 3.2 (Proof principle for regular separability, [16, Theorem
11]).

Consider ULTS $\mathit{U},\mathit{V}$, one deterministic. If
$\mathit{U}\times\mathit{V}$ has a finitely represented inductive invariant,
then $\mathit{L}(\mathit{U})\mathop{|}\mathit{L}(\mathit{V})$.

Interestingly, the proof principle does not need the WQO assumption of WSTS
but holds for general ULTS. It does assume one of the ULTS to be
deterministic, though. Recall that an _inductive invariant_ for an ULTS
$(Q,\leq,I,\Sigma,\delta,F)$ is a downward-closed set of states $S\subseteq Q$
that includes all initial states, excludes all final states, and is closed
under taking transitions:

$\displaystyle I\subseteq S\qquad S\cap F=\emptyset\qquad\delta(S,a)\subseteq
S\ .$

The inductive invariant is _finitely represented_ , if there is a finite set
$C\subseteq S$ with $S=\mathord{\downarrow}C$. We refer to a set $C$ that
satisfies this as a _cover_ of $S$.

When trying to invoke Theorem 3.2, finding an inductive invariant for
$\mathit{U}\times\mathit{V}$ is easy: the invariant is guaranteed to exist as
soon as the language
$\mathit{L}(\mathit{U}\times\mathit{V})=\mathit{L}(\mathit{U})\cap\mathit{L}(\mathit{V})$
is empty, which is precisely the hypothesis we start from.

######  Lemma 3.3 ([16, Lemma 10]).

An ULTS $\mathit{U}$ admits an inductive invariant iff
$\mathit{L}(\mathit{U})=\emptyset$.

The difficult part is to find an inductive invariant that can be represented
in a finite way. In [16], this was addressed with ideal decompositions [32,
21, 22]. The ideal decompositions, however, needed the WQO assumption, which
lead to the requirement in the main theorem that one WSTS had to be
deterministic. As we show in Section 4, this is a real restriction: there are
WSTS languages that cannot be accepted by a deterministic WSTS.

Our contribution is to find finitely represented inductive invariants without
making use of ideal decompositions. Our approach is to determinize the given
WSTS with the construction in Lemma 2.1, and accept that we can no longer
guarantee the result to be a WSTS.

###  3.2 Converging Transition Systems: WSTS in Disguise

We propose converging transition systems (CTS), a new class of ULTS that is
general enough to capture determinized WSTS and retains enough structure to
establish the existence of finitely represented inductive invariants. Working
with CTS rather than determinized WSTS leads to a cleaner development (we can
avoid products and downward-closed sets) and allows us to highlight key
arguments. CTS are inspired by Noetherian transition systems [26, 27], but are
formulated in a lattice-theoretic rather than in a topological way.

Recall that determinized WSTS have a state space $(\mathbb{D}(Q),\subseteq)$,
where $(Q,\leq)$ is a WQO. In a WQO, every infinite sequence admits an
increasing subsequence. It is well known [38] that this may not hold for
$(\mathbb{D}(Q),\subseteq)$. However, a natural relaxation holds: every
infinite sequence $[X_{i}]_{i\in{\rm Nature}}$ admits an infinite subsequence
$[X_{\varphi(i)}]_{i\in{\rm Nature}}$, where any element that is present in
one set is present in almost every set. A similar property, defined for
complete lattices, is called convergence in the literature [25]. Our
definition differs from the citation in two ways. We restrict ourselves to
sequences (as opposed to nets), and we require convergence to the join (as
opposed to $\lim\sup=\lim\inf$). This suffices for our setting.

######  Definition 3.4.

A _converging lattice_ $(Q,\leq)$ is a completely distributive lattice, where
every sequence $[p_{i}]_{i\in{\rm Nature}}$ has a converging subsequence
$[p_{\varphi(i)}]_{i\in{\rm Nature}}$. A _converging sequence_
$[q_{i}]_{i\in{\rm Nature}}$ is an infinite sequence with

$\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}q_{j}=\bigsqcup_{i\in{\rm Nature}}q_{i}\ .$

The equality formalizes our explaination from before. In the context of sets,
where join and meet are respectively union and intersection, the right-hand
side of the equation contains all elements that appear in any set in the
sequence. The left side iterates over every finite initial segment, and
includes every element that appears in all sets outside of this segment. Every
element that is missing in only finitely many sets will eventually be
included.

Converging lattices not only generalize downward-closed subsets of WQOs, they
are also a sufficient condition for them. The backward direction is by [38,
Proof of Theorem 3]. The forward direction is by an application of the
following fact [38], also [33, Fact III.3]: $(\mathbb{D}(Q),\subseteq)$ is
well-founded if and only if the order is a WQO. The details are in the
appendix.

######  Lemma 3.5.

$(\mathbb{D}(Q),\subseteq)$ is a converging lattice if and only if $(Q,\leq)$
is a WQO.

The space of converging sequences is closed under the application of
continuous functions as formulated in the next lemma. While we would expect
this result to be known, we have not found a reference. The lemma is central
to our argument, therefore we give the proof.

######  Lemma 3.6.

Let $(Q,\leq)$ be a lattice, $[p_{i}]_{i\in{\rm Nature}}$ a converging
sequence in $Q$, and $f:Q\rightarrow Q$ a Scott continuous function. Then also
$[f(p_{i})]_{i\in{\rm Nature}}$ is converging.

######  Proof 3.7.

Due to convergence of the given sequence, we have $\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{j}=\bigsqcup_{i\in{\rm Nature}}p_{i}$. This equality yields
$f(\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{j})=f(\bigsqcup_{i\in{\rm Nature}}p_{i})$. By Scott continuity of $f$, we
get

$\bigsqcup_{i\in{\rm
Nature}}f(\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{j})=\bigsqcup_{i\in{\rm Nature}}f(p_{i})\ .$

Function $f$ is not assumed to be meet continous. But we can show an
inequality that is sufficient for our needs. For all $S\subseteq Q$ and $s\in
S$, we have
$f(\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}S)\leq
f(s)\sqcup
f(\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}S)$.
Scott continuity and the fact that $s\in S$ yield $f(s)\sqcup
f(\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}S)=f(s\sqcup\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}S)=f(s)$.
We have thus shown
$f(\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}S)\leq
f(s)$ for all $s\in S$. This means
$f(\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}S)\leq\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{s\in
S}f(s)$.

We apply this inequality to the previous equality:

$\bigsqcup_{i\in{\rm Nature}}f(p_{i})=\bigsqcup_{i\in{\rm
Nature}}f(\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{j})\leq\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}f(p_{j})\leq\bigsqcup_{i\in{\rm Nature}}f(p_{i})\ .$

This is $\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}f(p_{j})=\bigsqcup_{i\in{\rm Nature}}f(p_{i})$, as desired.

We explain the considerations that lead us to the definition of CTS given
below. In the light of Lemma 3.5, the states of a CTS should form a converging
lattice. This, however, was not enough to guarantee the existence of finitely
represented inductive invariants. One requirement of invariants is that they
are closed under taking transitions. To understand which sets satisfy this, we
had to restrict the transition relation. We define CTS only as a deterministic
model. Then the transitions form a function $\delta(-,a)$ for every letter
$a\in\Sigma$. Upward compatibility of these functions is not very informative.
Consider determinized WSTS: upward compatibility gives us $\delta(S_{0}\cup
S_{1},a)\supseteq\delta(S_{0},a)$, while we expect $\delta(S_{0}\cup
S_{1},a)=\delta(S_{0},a)\cup\delta(S_{1},a)$. In lattice-theoretic terms, we
expect the transition functions $\delta(-,a)$ to be Scott continuous. A
benefit of this requirement is of course that it makes Lemma 3.6 available. An
invariant should also be disjoint from the final states so that we had to
control this set as well. When determinizing WSTS, a set $D\in\mathbb{D}(Q)$
is final as soon as it contains a single final state. Given the definition of
convergence, we relax this to containing a finite set of final states.

######  Definition 3.8.

A _converging transition system_ (CTS) is an ULTS
$\mathit{U}=(Q,\leq,{y},\Sigma,\delta,F)$ that is deterministic, where
$(Q,\leq)$ is a converging lattice, the functions $\delta(-,a)$ are Scott
continuous for all $a\in\Sigma$, and the final states satisfy

finite acceptance: $\displaystyle\text{ for every }\bigsqcup K\in F\text{
there is a finite set }N\subseteq K\text{ with }\bigsqcup N\in F\ .$

The determinization of a WSTS yields a CTS, as it was one of the goals of the
CTS definition. Somewhat surprisingly, CTS do not add expressiveness but their
languages are already accepted by (non-deterministic) WSTS. The construction
is via join prime elements and can be found in the appendix. Together, the CTS
languages are precisely the WSTS languages, and one may see Definition 3.8 as
a reformulation of the WSTS model.

######  Proposition 3.9.

If $\mathit{U}$ is a WSTS, then $\mathit{U}^{\mathit{det}}$ is a CTS. For
every CTS $\mathit{V}$, there is a WSTS $\mathit{U}$ with
$\mathit{L}(\mathit{V})=\mathit{L}(\mathit{U})$. Together,
$\mathit{L}(\text{WSTS})=\mathit{L}(\text{CTS})$.

The correspondence allows us to import the countability assumption from Lemma
2.2. Indeed, if the WQO $(Q,\leq)$ is countable, then there is only a
countable number of downward-closed sets in $(\mathbb{D}(Q),\subseteq)$. This
is by a standard argument for WSTS: each downward-closed set can be
characterized by its complement, the complement is upward closed, and is
therefore characterized by its finite set of minimal elements.

######  Lemma 3.10.

For every $L\in\mathit{L}(\text{CTS})$, there is a CTS $\mathit{U}$ over a
countable number of states so that $L=\mathit{L}(\mathit{U})$

We will also need that CTS are closed under synchronized products.

######  Lemma 3.11.

If $\mathit{U}$ and $\mathit{V}$ are CTS, so is $\mathit{U}\times\mathit{V}$.

We summarize the findings so far. Given disjoint WSTS languages
$\mathit{L}(\mathit{V}_{1})\cap\mathit{L}(\mathit{V}_{2})=\emptyset$, the goal
is to show regular separability
$\mathit{L}(\mathit{V}_{1})\mathop{|}\mathit{L}(\mathit{V}_{2})$. We first
determinize both WSTS. By Proposition 3.9, $\mathit{V}_{1}^{\mathit{det}}$ and
$\mathit{V}_{2}^{\mathit{det}}$ are CTS. Moreover, by Lemma 2.1,
determinization preserves the language. We use Lemma 3.10 to obtain countable
CTS $\mathit{U}_{1}$ and $\mathit{U}_{2}$ that accept the same languages. To
show regular separability, we now intend to invoke Theorem 3.2 on
$\mathit{U}_{1}$ and $\mathit{U}_{2}$. CTS are already deterministic. It thus
remains to show that $\mathit{U}_{1}\times\mathit{U}_{2}$ has a finitely
represented inductive invariant. With Lemma 3.11,
$\mathit{U}_{1}\times\mathit{U}_{2}$ is another CTS $\mathit{U}$. Moreover,
the product corresponds to language intersection, so
$\mathit{L}(\mathit{U})=\emptyset$. By Lemma 3.3, we know that $\mathit{U}$
has an inductive invariant. We now show how to turn this invariant into a
finitely represented one.

###  3.3 Inductive Invariants in CTS

We show the following surprising property for countable CTS: every inductive
invariant $S$ can be generalized to an inductive invariant $\mathit{cl}(S)$
that is finitely represented. The closure operator is defined by adding to $S$
the joins of all converging sequences:

$\mathit{cl}(S)\quad=\quad\\{\ \bigsqcup_{i\in{\rm
Nature}}p_{i}\mid[p_{i}]_{i\in{\rm Nature}}\text{ a converging sequence in }S\
\\}\ .$

######  Proposition 3.12.

Let $\mathit{U}$ be a countable CTS and $S$ an inductive invariant of
$\mathit{U}$. Then also $\mathit{cl}(S)$ is an inductive invariant of
$\mathit{U}$ and it is finitely represented.

The proposition concludes the proof of Theorem 3.1. We simply invoke it on the
inductive invariant that exists by Lemma 3.3 as discussed above. The rest of
the section is devoted to the proof. We fix a countable CTS
$\mathit{U}=(Q,\leq,y,\Sigma,\delta,F)$ and an inductive invariant $S\subseteq
Q$.

The closure is expansive and idempotent, meaning sequences over joins of
sequences do not add new elements. Here, we need the fact that we have a
completely distributive lattice. Moreover, the closure yields a downward-
closed set. The closure is also trivially monotonic, and hence an upper
closure operator indeed [13], but we will not need monotonicity.

######  Lemma 3.13.

$S\subseteq\mathit{cl}(S)=\mathit{cl}(\mathit{cl}(S))=\mathord{\downarrow}\mathit{cl}(S)$.

######  Lemma 3.14.

$\mathit{cl}(S)$ is an inductive invariant.

######  Proof 3.15.

To prove that $\mathit{cl}(S)$ is an inductive invariant, we must show two
properties for the joins $\bigsqcup_{i\in{\rm Nature}}{p_{i}}=p$ of the
converging sequences $[p_{i}]_{i\in{\rm Nature}}$ in $S$ that we added. First,
we must show that we do not leave $\mathit{cl}(S)$ when taking transitions,
$\delta(p,a)\in\mathit{cl}(S)$ for all $a\in\Sigma$. Second, we must show that
the join is not a final state. We begin with the latter. Towards a
contradiction, suppose $p\in F$. Convergence yields $\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{j}\in F$. By the finite acceptance property of CTS, there must be a
finite set $K\subseteq{\rm Nature}$ with $k=\max K$ so that

$\bigsqcup_{i\in
K}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{j}=\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
k}p_{j}\in F\ .$

Since
$\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
k}p_{j}\leq p_{k}$ and $F$ is upward closed, we obtain $p_{k}\in F$. This is a
contradiction: $p_{k}$ belongs to the inductive invariant $S$ and the
invariant does not intersect the final states.

To show $\delta(p,a)\in\mathit{cl}(S)$, we first note that $\delta(p_{i},a)\in
S$ for all $i\in{\rm Nature}$. This holds as $S$ is an invariant and $p_{i}\in
S$. We now argue that not only the sequence $[\delta(p_{i},a)]_{i\in{\rm
Nature}}$ is in $S$, but also its join is in the closure. We use that the
transition function $\delta(-,a)$ is Scott continuous. This allows us to apply
Lemma 3.6 showing that $[\delta(p_{i},a)]_{i\in{\rm Nature}}$ coverges. Since
the sequence belongs to $S$, we obtain $\bigsqcup_{i\in{\rm
Nature}}\delta(p_{i},a)\in\mathit{cl}(S)$. We conclude by applying Scott
continuity:

$\delta(p,a)=\delta(\bigsqcup_{i\in{\rm Nature}}p_{i},a)=\bigsqcup_{i\in{\rm
Nature}}\delta(p_{i},a)\in\mathit{cl}(S)\ .$

It only remains to show that $\mathit{cl}(S)$ is finitely represented.

######  Proposition 3.16.

There is a finite set $C\subseteq\mathit{cl}(S)$ so that
$\mathord{\downarrow}C=\mathit{cl}(S)$.

We break down the proof of Proposition 3.16 into two steps. First, we show
that $\mathit{cl}(S)$ can be covered by an antichain. Then, we show that
infinite antichain covers do not exist. This implies that there must be a
finite antichain cover. The proofs reason over _closed_ sets, sets that
contain the limits of their converging sequences. We rely on the fact that
closed sets have at least one maximal element.

######  Lemma 3.17.

Consider $G\subseteq Q$ closed and non-empty. Then $\max G\neq\emptyset$.

Moreover, closedness remains intact after certain removals.

######  Lemma 3.18.

Consider $G,H\subseteq Q$ where $G$ is closed. Then
$G\setminus\mathord{\downarrow}H$ is closed.

We postpone the proofs of these lemmas until after the proof of Proposition
3.16.

######  Lemma 3.19.

There is an antichain cover of $\mathit{cl}(S)$.

######  Proof 3.20.

We claim that the maximal elements $\max\mathit{cl}(S)$ form an antichain
cover of $\mathit{cl}(S)$. It is clear that $\max\mathit{cl}(S)$ is an
antichain. Since $\mathit{cl}(S)$ is downward closed by Lemma 3.13, we also
have $\mathord{\downarrow}(\max\mathit{cl}(S))\subseteq\mathit{cl}(S)$. To see
that $\max\mathit{cl}(S)$ is a cover, let
$G=\mathit{cl}(S)\setminus\mathord{\downarrow}(\max\mathit{cl}(S))$ and
suppose $G\neq\emptyset$. Lemma 3.18 tells us that $G$ is closed. By Lemma
3.17, we get $\max G\neq\emptyset$. Consider $p\in\max G$. By the definition
of $G$, we have $p\not\in\max\mathit{cl}(S)$. Then, however, there must be
$q\in\mathit{cl}(S)$ with $p\leq q$. If
$q\in\mathord{\downarrow}(\max\mathit{cl}(S))$, then
$p\in\mathord{\downarrow}(\max\mathit{cl}(S))$ as well, which is a
contradiction to $p\in G$. If conversely
$q\in\mathit{cl}(S)\setminus\mathord{\downarrow}(\max\mathit{cl}(S))=G$, then
we have a contradiction to $p\in\max G$.

Now we prove the second part of Proposition 3.16, which states that there can
be no infinite antichain cover.

######  Lemma 3.21.

There is no infinite antichain cover of $\mathit{cl}(S)$.

######  Proof 3.22.

Suppose there is an infinite antichain cover $C\subseteq\mathit{cl}(S)$. Then,
there is an infinite sequence $[p_{i}]_{i\in{\rm Nature}}$ in $C$. By
Definition 3.4, it has an infinite converging subsequence
$[p_{\varphi(i)}]_{i\in{\rm Nature}}$. The closure operator adds
$\bigsqcup_{i\in{\rm Nature}}p_{\varphi(i)}$ to $\mathit{cl}(S)$. Since $C$ is
a cover of $\mathit{cl}(S)$, there must be $q\in C$ with $\bigsqcup_{i\in{\rm
Nature}}p_{\varphi(i)}\leq q$. So $p_{\varphi(i)}\leq q$ for all $i\in{\rm
Nature}$, while at the same time $q,p_{\varphi(i)}\in C$. This contradicts the
antichain property.

We conclude by showing Lemma 3.17 and 3.18.

######  Proof 3.23 (Proof of Lemma 3.17).

Let $\emptyset\neq G\subseteq Q$ be closed. We prove $G$ chain complete,
meaning for every chain $P\subseteq G$ the limit $\bigsqcup P$ is again in
$G$. Then Zorn’s lemma [30] applies and yields $\max G\neq\emptyset$. We have
Zorn’s lemma, because we agreed on the Axiom of Choice. Towards chain
completeness, consider an increasing sequence $[p_{i}]_{i\in{\rm Nature}}$ in
$G$. We prove that $\bigsqcup_{i\in{\rm Nature}}p_{i}\in G$. For any $i\in{\rm
Nature}$, we have
$\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{i}=p_{i}$. Hence, replacing each meet with the smallest element shows
convergence. Since $[p_{i}]_{i\in{\rm Nature}}$ convergences and $G$ is
closed, we have $\bigsqcup_{i\in{\rm Nature}}p_{i}\in G$.

Although we are in a countable setting, the argument for sequences does not
yet cover all chains. The problem is that the counting processs may not
respect the order. To see this, consider a chain $P\subseteq G$ of ordinal
size $|{P}|=\omega\cdot 2$. The chain is countable, but no counting process
can respect the order. We now argue that still $\bigsqcup P\in G$. By [34,
Theorem 1], there is an (wrt. inclusion) increasing sequence of subsets
$[P_{i}]_{i\in{\rm Nature}}$ in $\mathbb{P}(P)$, where each $P_{i}$ is finite
and $\bigcup_{i\in{\rm Nature}}P_{i}=P$. Finite chains contain maximal
elements, so let $p_{i}=\max P_{i}=\bigsqcup P_{i}$. Then

$\bigsqcup P\ =\ \bigsqcup\bigcup_{i\in{\rm Nature}}P_{i}\ =\
\bigsqcup_{i\in{\rm Nature}}\bigsqcup P_{i}\ =\ \bigsqcup_{i\in{\rm
Nature}}p_{i}\ .$

Since $[P_{i}]_{i\in{\rm Nature}}$ is an increasing sequence, also
$[p_{i}]_{i\in{\rm Nature}}$ is an increasing sequence. As we have shown
before, $\bigsqcup_{i\in{\rm Nature}}p_{i}\in G$. This concludes the proof.

######  Proof 3.24 (Proof of Lemma 3.18).

Consider $G,H\subseteq Q$ with $G$ closed. We show that
$G\setminus\mathord{\downarrow}H$ is closed. Let $[p_{i}]_{i\in{\rm Nature}}$
be a converging sequence in $G\setminus\mathord{\downarrow}H$. Let
$q=\bigsqcup_{i\in{\rm Nature}}p_{i}$ and suppose $q\not\in
G\setminus\mathord{\downarrow}H$. Since $G$ is closed, $q\in G$. Then
necessarily $q\in\mathord{\downarrow}H$. But by definition, $p_{i}\leq q$ for
all $i\in{\rm Nature}$. So $p_{i}\in\mathord{\downarrow}H$ as well. This
contradicts the fact that the sequence $[p_{i}]_{i\in{\rm Nature}}$ lives in
$G\setminus\mathord{\downarrow}H$.

##  4 Non-Determinizability of WSTS

We show that the detWSTS languages form a strict subclass of the WSTS
languages. To this end, we define a WSTS language $T$ that we prove cannot be
accepted by a detWSTS. The proof relies on a novel characterization of the
detWSTS languages that may be of independent interest. In the following, we
call $T$ the _witness language_. This is our main result.

######  Theorem 4.1.

$\mathit{L}(\text{detWSTS})\neq\mathit{L}(\text{WSTS})$.

Towards the definition of $T$, recall that finitely-branching WSTS and WSTS
over so-called $\omega^{2}$-WQOs can be determinized [16, Theorem 5].
Moreover, it is known that $\omega^{2}$-WQOs are precisely the WQOs that do
not embed the Rado WQO [8, Section 2]. This suggests we should accept the
witness language $T$ by an infinitely-branching WSTS over the Rado WQO. We
begin with our characterization of detWSTS languages, as it will provide
additional guidance in the definition of the witness language.

###  4.1 Characterization of the detWSTS Languages

Our characterization is based on a classical concept in formal languages [29,
Theorem 3.9]. The _Nerode quasi order_
$\mathord{\leq_{L}}\subseteq\Sigma^{*}\times\Sigma^{*}$ of a language
$L\subseteq\Sigma^{*}$ is defined by $w\leq_{L}v$, if

$\displaystyle\text{for all }u\in\Sigma^{*}\text{ we have that $w.u\in L$
implies $v.u\in L$.}$

The characterization says that the detWSTS languages are precisely the
languages whose Nerode quasi order is a WQO. Note that this is not the
folklore result [5, Proposition 5.1] saying that a language is regular if and
only if the syntactic quasi order is a WQO.

######  Lemma 4.2 (Characterization of $\mathit{L}(\text{detWSTS})$).

$L\in\mathit{L}(\text{detWSTS})$ iff $\mathord{\leq_{L}}$ is a WQO.

######  Proof 4.3.

$\Rightarrow$ Let $L=\mathit{L}(\mathit{U})$ with
$\mathit{U}=(Q,\leq,i,\Sigma,\delta,F)$ a detWSTS. We extend the order $\leq\
\subseteq Q\times Q$ on the states to an order $\leq_{\mathit{U}}\
\subseteq\Sigma^{*}\times\Sigma^{*}$ on words by setting
$w\leq_{\mathit{U}}v$, if $\delta(i,w)=p$ and $\delta(i,v)=q$ with $p\leq q$.
Since $\mathit{U}$ is deterministic, $p$ and $q$ are guaranteed to exist and
be unique. It is easy to see that $\leq_{\mathit{U}}$ is a WQO. We now show
that $\leq_{\mathit{U}}$ is included in the Nerode quasi order, and so also
$\leq_{L}$ is a WQO. To this end, we consider $w\leq_{\mathit{U}}v$ and
$u\in\Sigma^{*}$ with $w.u\in L$, and show that also $v.u\in L$. We have
$\delta(i,w.u)=\delta(p_{1},u)=p_{2}$ and
$\delta(i,v.u)=\delta(q_{1},u)=q_{2}$ with $p_{1}=\delta(i,w)$ and
$q_{1}=\delta(i,v)$. Since $w\leq_{\mathit{U}}v$, we have $p_{1}\leq q_{1}$.
With the simulation property of WSTS, this implies $p_{2}\leq q_{2}$. Since
$w.u\in L$ and $L=\mathit{L}(\mathit{U})$, we get $p_{2}\in F$. Since $F$ is
upward closed, also $q_{2}\in F$. Hence, $v.u\in\mathit{L}(\mathit{U})=L$ as
desired.

$\Leftarrow$ Consider a language $L\subseteq\Sigma^{*}$ whose Nerode quasi
order $\leq_{L}$ is a WQO. We define the trivial detWSTS
$\mathit{U}_{L}=(\Sigma^{*},\leq_{L},\varepsilon,\Sigma,\delta,L)$. The states
are all words ordered by the Nerode quasi order. The empty word is the initial
state, the language $L$ is the set of final states. Note that $L$ is upward
closed wrt. $\leq_{L}$. The transition relation is defined as expected,
$\delta(w,a)=w.a$. It is readily checked that $\mathit{L}(\mathit{U}_{L})=L$.

The lemma gives a hint on how to construct the witness language $T$: we should
make sure the associated Nerode quasi order $\leq_{T}$ has an infinite
antichain (then it cannot be a WQO). To obtain such an antichain, remember
that $T$ will be accepted by a WSTS over the Rado WQO $(R,\leq_{R})$ [38]. It
is known that $(\mathbb{D}(R),\subseteq)$ has an infinite antichain. Our
strategy for the definition of $T$ will therefore be to translate the infinite
antichain in $(\mathbb{D}(R),\subseteq)$ into an infinite antichain in
$(\Sigma^{*},\leq_{T})$. We turn to the details, starting with the Rado WQO.

###  4.2 Witness Language

#### Rado Order

Our presentation of the Rado WQO [38] follows [35]. The _Rado set_ is the
upper diagonal, $R=\\{(c,r)\mid c<r\\}\subseteq{\rm Nature}^{2}$. The Rado WQO
$\leq_{R}\ \subseteq R\times R$ is defined by:

$\displaystyle(c_{1},r_{1})\leq_{R}(c_{2},r_{2}),\qquad\text{if}\qquad
r_{1}\leq c_{2}\,\,\vee\,\,(c_{1}=c_{2}\,\,\wedge\,\,r_{1}\leq r_{2})\ .$

Given an element $(c,r)$, we call $c$ the _column_ and $r$ the _row_ , as
suggested by Figure 1(left). Columns will play an important role and we denote
column $i$ by $C_{i}=\\{(i,r)\mid i<r\\}\subseteq R$. To arrive at a larger
element in the Rado WQO, one can increase the row while remaining in the same
column, or move to the rightmost column of the current row, and select an
element to the right, Figure 1(middle).

$(0,0)$$(0,1)$$(0,2)$$(0,3)$$(0,4)$$(0,5)$$(0,6)$$(0,7)$$(0,8)$$(1,1)$$(1,2)$$(1,3)$$(1,4)$$(1,5)$$(1,6)$$(1,7)$$(1,8)$$(2,2)$$(2,3)$$(2,4)$$(2,5)$$(2,6)$$(2,7)$$(2,8)$$(3,3)$$(3,4)$$(3,5)$$(3,6)$$(3,7)$$(3,8)$$(4,4)$$(4,5)$$(4,6)$$(4,7)$$(4,8)$$(5,5)$$(5,6)$$(5,7)$$(5,8)$$(6,6)$$(6,7)$$(6,8)$$(7,7)$$(7,8)$column
$3$row $5$

$\ddots$

$(0,0)$$(1,1)$$(2,2)$$(3,3)$$(3,5)$$(3,6)$$(3,7)$$(3,8)$$(4,4)$$(5,5)$$(5,6)$$(5,7)$$(5,8)$$(6,6)$$(6,7)$$(6,8)$$(7,7)$$(7,8)$

$\ddots$

$(0,0)$$(0,1)$$(0,2)$$(0,3)$$(1,1)$$(1,2)$$(1,3)$$(2,2)$$(2,3)$$(3,3)$$(3,4)$$(3,5)$$(3,6)$$(3,7)$$(3,8)$$(4,4)$$(5,5)$$(6,6)$$(7,7)$

$\ddots$

Figure 1: Rado order with the column and row of $(3,5)$ marked (left), with
the elements larger than $(3,5)$ marked (middle), and with the downward
closure of column $3$ marked (right).

It is not difficult to see that $(R,\leq_{R})$ is a WQO [38]. In an infinite
sequence, either the columns eventually plateau out, in which case the rows
lead to comparable elements, or the columns grow unboundedly, in which case
they eventually exceed the row in the initial pair. The interest in the Rado
WQO is that the WQO property is lost when moving to
$(\mathbb{D}(R),\subseteq)$. This failure is due to the following well-known
fact.

######  Lemma 4.4 ([22], Proposition 4.2).

$\\{\mathord{\downarrow}C_{i}\mid i\in{\rm Nature}\\}$ is an infinite
antichain in $(\mathbb{D}(R),\subseteq)$.

To see the lemma, we illustrate the downward closure of a column in Figure
1(right). Inclusion fails to be a WQO as each column $C_{i}$ forms an infinite
set that the downward closure $\mathord{\downarrow}C_{j}$ with $j>i$ cannot
cover. Indeed, $\mathord{\downarrow}C_{j}$ only has the triangle to the
bottom-left of column $C_{j}$ available to cover $C_{i}$, and the triangle is
a finite set. We will use exactly this difference between infinite and finite
sets in our witness language. It will become clearer as we proceed.

#### Definition of $T$

The witness language is the language accepted by
$\mathit{U}_{R}=(R,\leq_{R},C_{0},\Sigma,\delta,R)$. The set of states is the
Rado set, the set of initial states is the first column, and the set of final
states is again the entire Rado set. The latter means that a word is accepted
as long as it admits a run. The letters in
$\Sigma=\\{a,\bar{a},\mathit{zero}\\}$ reflect the operation that the
transitions $\delta\subseteq R\times\Sigma\times R$ perform on the states:

$\displaystyle\delta((c,r),a)\ $ $\displaystyle=\ {(c+1,r+1)}\qquad\qquad$
$\displaystyle\delta((c+1,r+1),\bar{a})\ $ $\displaystyle=\ {(c,r)}$
$\displaystyle\delta((c+1,r),\mathit{zero})\ $ $\displaystyle=\ {(0,c)}\quad$
$\displaystyle\delta((0,r+1),\mathit{zero})\ $ $\displaystyle=\ {(0,r)}\ .$

We will explain the transitions in a moment, but remark that they are designed
in a way that makes $\leq_{R}$ a simulation relation and hence
$\mathit{U}_{R}$ a WSTS.

######  Lemma 4.5.

$T\in\mathit{L}(\text{WSTS})$.

To prove $T\notin\mathit{L}(\text{detWSTS})$, we associate with each column
$C_{i}$ the _column language_
$L_{i}=\\{w\in\Sigma^{*}\mid\delta(C_{0},w)=C_{i}\\}$. It consists of the
words that reach _all_ states in $C_{i}$ from the initial column $C_{0}$. The
column languages are non-empty.

######  Lemma 4.6.

$L_{i}\neq\emptyset$ for all $i\in{\rm Nature}$.

We start from the entire initial column, meaning $\varepsilon\in L_{0}$. The
transitions labeled by $a$ move from all states in one column to all states in
the next column, $L_{i}.a\subseteq L_{i+1}$. This already proves the lemma.
The $\bar{a}$-labeled transitions undo the effect of the $a$-labeled
transitions and decrement the column, $L_{i+1}.\bar{a}\subseteq L_{i}$. In the
initial column, this is impossible, $\delta(C_{0},\bar{a})=\emptyset$. We
illustrate the behaviour of $a$ and $\bar{a}$ in Figure 2(left)

By Lemma 4.4, the columns form an antichain in $(\mathbb{D}(R),\subseteq)$.
The languages $L_{i}$ we have just defined translate this antichain into
(actually several) antichains of the form we need.

######  Lemma 4.7.

Every set $\\{w_{i}\mid w_{i}\in L_{i}\\}$ is an antichain in
$(\Sigma^{*},\leq_{T})$.

Combined, Lemmas 4.6, 4.7, and 4.2 conclude the proof of Theorem 4.1.

######  Proposition 4.8.

$T\notin\mathit{L}(\text{detWSTS})$

In the rest of the section, we prove Lemma 4.7. The lemma claims that entire
column languages are incomparable in the Nerode quasi order, so we write
$L\not\sim_{T}K$ if for all $w\in L$ and all $v\in K$ we have $w\not\leq_{T}v$
and $v\not\leq_{T}w$. Difficult is the incomparability with $L_{0}$ stated in
the next lemma. The proof will explain the purpose of the
$\mathit{zero}$-labeled transitions.

$(0,0)$$(1,1)$$(2,2)$$(2,3)$$(2,4)$$(2,5)$$(2,6)$$(2,7)$$(3,3)$$(3,4)$$(3,5)$$(3,6)$$(3,7)$$(4,4)$$(4,5)$$(4,6)$$(4,7)$$(5,5)$$(6,6)$$\bar{a}$
and $a$

$\ddots$

$(0,0)$$(0,1)$$(0,2)$$(0,3)$$(1,1)$$(1,2)$$(1,3)$$(2,2)$$(2,3)$$(3,3)$$(3,4)$$(3,5)$$(3,6)$$(3,7)$$(4,4)$$(5,5)$$(6,6)$$\mathit{zero}$

$\ddots$

Figure 2: The effect of $a$ and $\bar{a}$-labeled transitions on column $3$
(left) and the effect of $\mathit{zero}$-labeled transitions on columns $0$
and $3$ (right).

######  Lemma 4.9.

$L_{0}\not\sim_{T}L_{k}$ for all $k>0$.

######  Proof 4.10.

Let $w\in L_{0}$ and $v\in L_{k}$, meaning $w$ leads to all states in column
$0$ while $v$ leads to all states in column $k>0$. It is easy to find a suffix
that shows the $v\not\leq_{T}w$, namely $\bar{a}$. Appending $\bar{a}$ to $v$
leads to column $C_{k-1}$, and so $v.\bar{a}\in T$, while there is no
transition on $\bar{a}$ from $C_{0}$, and so $w.\bar{a}\notin T$.

For $w\not\leq_{T}v$, we need the $\mathit{zero}$ transitions. The idea is to
make them fail in $C_{k}$ for $k>0$, and have no effect in $C_{0}$. The
problem is that the states in $C_{k}$ must simulate $(0,r)$ for $r\leq k$. The
trick is to fail with a delay. Instead of having no effect in $C_{0}$, we let
the $\mathit{zero}$ transitions decrement the row. Instead of failing in
$C_{k}$, we let the $\mathit{zero}$ transitions imitate the behavior from
$(0,k)$ and move to $(0,k-1)$. This is illustrated in Figure 2(right).

By working with column languages, the $\mathit{zero}$ transitions fail in
$C_{k}$ with a delay as follows. We have $L_{0}.\mathit{zero}\subseteq L_{0}$
but $L_{k}.\mathit{zero}\not\subseteq L_{0}$, meaning from $C_{0}$ we again
reach the entire column $C_{0}$, while from $C_{k}$ we only reach the state
$(0,k-1)$. The decrement behavior in the initial column allows us to
distinguish the cases by exhausting the rows. Certainly, $\mathit{zero}^{k-1}$
is enabled in large enough states of $C_{0}$, meaning $w.\mathit{zero}^{k}\in
T$. The state $(0,k-1)$ reached by $v.\mathit{zero}$, however, does not enable
corresponding transitions, $v.\mathit{zero}^{k}\notin T$.

When executed in $C_{k}$ with $k>0$, the $\mathit{zero}$ transitions resemble
reset transitions [19]. An analogue of leaving $C_{0}$ unchanged despite
decrements does not exist in the classical model. Moreover, reset nets are
defined over ${\rm Nature}^{k}$ (an $\omega^{2}$-WQO) as opposed to the Rado
set. To conclude the proof of Lemma 4.7, we lift the previous result to
arbitrary column languages.

######  Lemma 4.11.

$L_{i}\not\sim_{T}L_{j}$ for all $i\neq j$.

######  Proof 4.12.

Let $i<j$ and consider $w\in L_{i}$ and $v\in L_{j}$. For $v\not\leq_{T}w$, we
append $\bar{a}^{j}$, which is possible only from the larger column:
$v.\bar{a}^{j}\in T$ but $w.\bar{a}^{j}\notin T$. For $w\not\leq_{T}v$, we
append $\bar{a}^{i}$. Then $w.\bar{a}^{i}\in L_{0}$ while $v.\bar{a}^{i}\in
L_{k}$ with $k>0$. Now Lemma 4.9 applies and yields a suffix $u$ so that
$w.\bar{a}^{i}.u\in T$ but $v.\bar{a}^{i}.u\notin T$.

The WSTS accepting the witness language $T$ only uses non-determinism in the
choice of the initial state. The transitions are deterministic. Moreover, the
Rado WQO is embedded in every non-$\omega^{2}$-WQO [8, Section 2]. Given the
determinizability results from [16, Theorem 5], language $T$ thus shows non-
determinizability of WSTS with minimal requirements.

##  5 Downward-Compatible WSTS

We show that the regular separability and non-determinizability results we
have obtained for upward-compatible WSTS so far can be lifted to downward-
compatible WSTS (DWSTS). In DWSTS, smaller states simulate larger ones and the
set of final states is downward closed. We lift our results by establishing
general relations between the language classes $\mathit{L}(\text{WSTS})$,
$\mathit{L}(\text{DWSTS})$, $\mathit{L}(\text{detWSTS})$, and
$\mathit{L}(\text{detDWSTS})$. Figure 3 summarizes them.

$\mathit{L}(\text{detWSTS})$$\mathit{L}(\text{WSTS})$$\mathit{L}(\text{detDWSTS})$$\mathit{L}(\text{DWSTS})$$=_{\mathit{cmp}}$,
Lemma 5.2$\not\subseteq_{\mathit{rev}}$, $\not\supseteq_{\mathit{rev}}$, Lemma
5.7$=_{\mathit{rev}}$, Lemma 5.1$\subsetneq,\ {\text{\footnotesize
Theorem\leavevmode\nobreak\ \ref{Theorem:WSTSneqDWSTS}}}$$\subsetneq,\
{\text{\footnotesize Theorem\leavevmode\nobreak\
\ref{Theorem:ComplWitnessLanguage}}}$ Figure 3: Relations between language
classes.

#### Downward Compatibility

A _downward-compatible LTS_ (DLTS) is an LTS
$\mathit{D}=(Q,I,\Sigma,\delta,F)$ whose states are equipped with a quasi
order $\leq\ \subseteq Q\times Q$ so that the following holds. The final
states are downward closed, $\mathord{\downarrow}F=F$, and $\geq$ is a
simulation relation. Recall that this means for all $p_{1}\leq q_{1}$ and for
all $q_{2}\in\delta(q_{1},a)$ there is $p_{2}\in\delta(p_{1},a)$ with
$p_{2}\leq q_{2}$. We denote the class of deterministic DLTS by detDLTS. We
use $\mathit{L}(\text{DLTS})$ and $\mathit{L}(\text{detDLTS})$ to refer to the
classes of all DLTS resp. detDLTS languages. If $\leq$ is also a WQO, we call
$\mathit{D}$ a _downward-compatible WSTS_ (DWSTS).

#### Relations between $\mathit{L}(\text{DLTS})$ and
$\mathit{L}(\text{ULTS})$.

The languages accepted by DLTS are the reverse of the languages accepted by
ULTS, and vice-versa. This is easy to see by reversing the transitions. Let
$\mathit{U}=(Q,\leq,I,\Sigma,\delta,F)$ be an ULTS. We define
${\mathit{U}}^{\mathit{rev}}=(Q,\leq,F,\Sigma,{\delta}^{\mathit{rev}},\mathord{\downarrow}I)$
to be its reversal. The initial and final states are swapped and the direction
of the transitions is flipped,
${\delta}^{\mathit{rev}}=\\{(p,a,q)\mid(q,a,p^{\prime})\in\delta,p\leq
p^{\prime}\\}$. Note that we close the initial states downwards and add
transitions from states smaller than the original target. This corresponds to
the assumption that the original transitions relate downward-closed sets. The
construction can also be applied in reverse to get an ULTS
${\mathit{D}}^{\mathit{rev}}$ from a DLTS $\mathit{D}$.

######  Lemma 5.1.

If $\mathit{U}\in\text{ULTS}$ (WSTS), then
${\mathit{U}}^{\mathit{rev}}\in\text{DLTS}$ (DWSTS) and
$\mathit{L}({\mathit{U}}^{\mathit{rev}})={\mathit{L}(\mathit{U})}^{\mathit{rev}}$.
If $\mathit{D}\in\text{DLTS}$ (DWSTS), then
${\mathit{D}}^{\mathit{rev}}\in\text{ULTS}$ (WSTS) and
$\mathit{L}({\mathit{D}}^{\mathit{rev}})={\mathit{L}(\mathit{D})}^{\mathit{rev}}$.

The detDLTS languages are precisely the complements of the detULTS languages.
For a detULTS or detDLTS $\mathit{U}=(Q,\leq,I,\Sigma,\delta,F)$, we define
the complement $\overline{\mathit{U}}=(Q,\leq,I,\Sigma,\delta,\overline{F})$
by complementing the set of final states [37, Theorem 5].

######  Lemma 5.2.

$\mathit{U}\in\text{detULTS}$ $(\text{detWSTS})$ iff
$\overline{\mathit{U}}\in\text{detDLTS}$ $(\text{detDWSTS})$, and
$\mathit{L}(\overline{\mathit{U}})=\overline{\mathit{L}(\mathit{U})}$.

Behind this is the observation that, under determinism, $\leq$ is a simulation
if and only if $\geq$ is [36, Theorem 3.3(ii)]. The details are in the
appendix.

###  5.1 Lifting Results

#### Regular Separability of DWSTS

We obtain the regular separability of disjoint DWSTS languages as a
consequence of the previous results. More precisely, we need Lemma 5.1,
Theorem 3.1, and the closure of the regular languages under reversal.

######  Theorem 5.3.

Let $L_{1},L_{2}\in\mathit{L}(\text{DWSTS})$. We have $L_{1}\mathop{|}L_{2}$
if and only if $L_{1}\cap L_{2}=\emptyset$.

#### Non-Determinizability of DWSTS

To show that DWSTS cannot be determinized, recall our witness language $T$
from Section 4. Surprisingly, we have the following.

######  Lemma 5.4.

${T}^{\mathit{rev}}\in\mathit{L}(\text{detDWSTS})$ and
${\overline{T}}^{\mathit{rev}}\in\mathit{L}(\text{detWSTS})$.

For the first claim, recall that the witness language is accepted by the WSTS
$\mathit{U}_{R}$. The DWSTS ${\mathit{U}_{R}}^{\mathit{rev}}$ has one minimal
initial state, and transition images ${\delta}^{\mathit{rev}}(p,b)$ with one
minimal element for all $p\in R$ and $b\in\Sigma$. Removing simulated states
yields a deterministic DWSTS. The details are in the appendix. For the second
claim, $\overline{{T}^{\mathit{rev}}}\in\mathit{L}(\text{detWSTS})$ by Lemma
5.2. But $\overline{{T}^{\mathit{rev}}}={\overline{T}}^{\mathit{rev}}$, and so
${\overline{T}}^{\mathit{rev}}\in\mathit{L}(\text{detWSTS})$. Behind this is
the fact that bijections commute with complements, and reversal is a
bijection.

The lemma allows us to prove non-determinizability for DWSTS. Notably, we do
not need a characterization for the languages of deterministic DWSTS.

######  Theorem 5.5.

$\overline{T}\in\mathit{L}(\text{DWSTS})\setminus\mathit{L}(\text{detDWSTS})$
and so $\mathit{L}(\text{DWSTS})\neq\mathit{L}(\text{detDWSTS})$.

######  Proof 5.6.

By Lemma 5.4, ${\overline{T}}^{\mathit{rev}}\in\mathit{L}(\text{detWSTS})$.
Lemma 5.1 yields $\overline{T}\in\mathit{L}(\text{DWSTS})$. Suppose
$\overline{T}\in\mathit{L}(\text{detDWSTS})$. Then
$T\in\mathit{L}(\text{detWSTS})$ by Lemma 5.2. This contradicts Proposition
4.8.

###  5.2 Consequences

We have shown that neither upward- nor downward-compatible WSTS can be
determinized. This does not yet rule out the possibility of determinizing an
upward-compatible WSTS into a downward-compatible one, and vice versa. Given
the correspondence in Lemma 5.1, we should allow the determinization to
reverse the language. We now show that also this form of reverse-
determinization is impossible: there are even deterministic languages that
cannot be reverse-determinized. This is by Lemma 5.4, Proposition 4.8, and
Theorem 5.5.

######  Lemma 5.7.

${T}^{\mathit{rev}}\in\mathit{L}(\text{detDWSTS})$ but
$T\notin\mathit{L}(\text{detWSTS})$. Similarly,
${\overline{T}}^{\mathit{rev}}\in\mathit{L}(\text{detWSTS})$ but
$\overline{T}\notin\mathit{L}(\text{detDWSTS})$

After reversal, both witness languages $T$ and $\overline{T}$ can be accepted
by a deterministic WSTS. When it comes to separability, this means the results
from [16] apply to them. A consequence of Lemma 5.7, however, is that there
are WSTS languages that can neither be determinized nor reverse-determinized.
An instance is $K=T.\\#.{\overline{T}}^{\mathit{rev}}$ with $\\#$ a fresh
letter.

######  Lemma 5.8.

$K\in\mathit{L}(\text{WSTS})$, $K\not\in\mathit{L}(\text{detWSTS})$, and
${K}^{\mathit{rev}}\not\in\mathit{L}(\text{detDWSTS})$.

When considering $L\cap K=\emptyset$, the separability result from [16] does
not apply. Theorem 3.1 is stronger and yields $L\mathop{|}K$. The situation is
similar for downward-compatible WSTS and ${K}^{\mathit{rev}}$.

##  6 Conclusion and Future Work

We have shown that disjoint WSTS languages are always separated by a regular
language. This strengthens the popular separability result from [16] by
showing that the premise in that work (one language had to be accepted by a
deterministic WSTS) is not needed. We have also show that deterministic WSTS
accept a strictly weaker class of languages than their non-deterministic
counterparts, meaning the premise was a real restriction.

Behind our separability result is a closure of inductive invariants that adds
limits of converging sequences, and the fact that the transition relation is
compatible with limits. It would be interesting to formulate this in a
topological setting [26, 27]. It would also be interesting to apply our
invariant closure in settings where separability does not coincide with
intersection emptiness and the complexity is open [6]. Finally, it would be
interesting to develop compositional verification technology based on
separability.

## References

  * [1] P. A. Abdulla, M. F. Atig, V. Dave, and S. Narayanan Krishna.  On the separability problem of string constraints.  In CONCUR, volume 171 of LIPIcs, pages 16:1–16:19. Dagstuhl, 2020.
  * [2] P. A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay.  General decidability theorems for infinite-state systems.  In LICS, pages 313–321. IEEE, 1996.
  * [3] P. A. Abdulla, G. Delzanno, and L. Van Begin.  Comparing the expressive power of well-structured transition systems.  In CSL, volume 4646 of LNCS, pages 99–114. Springer, 2007\.
  * [4] P. A. Abdulla and B. Jonsson.  Verifying programs with unreliable channels.  In LICS, pages 160–170. IEEE, 1993.
  * [5] G.Rozenberg A.Salomaa, editor.  Handbook of Formal Languages.  Springer, 1997.
  * [6] P. Baumann, R. Meyer, and G. Zetzsche.  Regular separability in Büchi VASS.  In STACS, volume 254 of LIPIcs, pages 9:1–9:19. Dagstuhl, 2023.
  * [7] M. Blondin, A. Finkel, and P. McKenzie.  Handling infinitely branching WSTS.  In ICALP, volume 8573 of LNCS, pages 13–25. Springer, 2014\.
  * [8] P. Jančar.  A note on well quasi-orderings for powersets.  IPL, 72(5):155–160, 1999.
  * [9] E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, editors.  Handbook of Model Checking.  Springer, 2018.
  * [10] L. Clemente, W. Czerwinski, S. Lasota, and C. Paperman.  Regular separability of Parikh automata.  In ICALP, volume 80 of LIPIcs, pages 117:1–117:13. Dagstuhl, 2017.
  * [11] L. Clemente, W. Czerwinski, S. Lasota, and C. Paperman.  Separability of reachability sets of vector addition systems.  In STACS, volume 66 of LIPIcs, pages 24:1–24:14. Dagstuhl, 2017.
  * [12] L. Clemente, S. Lasota, and R. Piórkowski.  Timed games and deterministic separability.  In ICALP, volume 168 of LIPIcs, pages 121:1–121:16. Dagstuhl, 2020.
  * [13] P. Cousot.  Principles of abstract interpretation.  MIT Press, 2021.
  * [14] W. Czerwinski, P. Hofman, and G. Zetzsche.  Unboundedness problems for languages of vector addition systems.  In ICALP, volume 107 of LIPIcs, pages 119:1–119:15. Dagstuhl, 2018.
  * [15] W. Czerwinski and S. Lasota.  Regular separability of one counter automata.  In LICS, pages 1–12. IEEE, 2017.
  * [16] W. Czerwinski, S. Lasota, R. Meyer, S. Muskalla, K. Narayan Kumar, and P. Saivasan.  Regular separability of well-structured transition systems.  In CONCUR, volume 118 of LIPIcs, pages 35:1–35:18. Dagstuhl, 2018.
  * [17] W. Czerwinski, W. Martens, L. van Rooijen, M. Zeitoun, and G. Zetzsche.  A characterization for decidable separability by piecewise testable languages.  DMTCS, 19(4), 2017.
  * [18] W. Czerwinski and G. Zetzsche.  An approach to regular separability in vector addition systems.  In LICS, pages 341–354. ACM, 2020.
  * [19] C. Dufourd, A. Finkel, and Ph. Schnoebelen.  Reset nets between decidability and undecidability.  In ICALP, pages 103–115. Springer, 1998.
  * [20] A. Finkel.  A generalization of the procedure of Karp and Miller to well structured transition systems.  In ICALP, volume 267 of LNCS, pages 499–508. Springer, 1987\.
  * [21] A. Finkel and J. Goubault-Larrecq.  Forward analysis for WSTS, part II: complete WSTS.  In ICALP, volume 5556 of LNCS, pages 188–199. Springer, 2009\.
  * [22] A. Finkel and J. Goubault-Larrecq.  Forward analysis for WSTS, part II: complete WSTS.  LMCS, 8(3), 2012.
  * [23] A. Finkel and Ph. Schnoebelen.  Well-structured transition systems everywhere!  TCS, 256(1-2):63–92, 2001.
  * [24] G. Geeraerts, J.-F. Raskin, and L. Van Begin.  Well-structured languages.  Acta Informatica, 44(3-4):249–288, 2007.
  * [25] A. R. Gingras.  Convergence lattices.  RMJ, 6(1):85–104, 1976.
  * [26] J. Goubault-Larrecq.  On Noetherian spaces.  In LICS, pages 453–462. IEEE, 2007.
  * [27] J. Goubault-Larrecq.  Noetherian spaces in verification.  In ICALP, volume 6199 of LNCS, pages 2–21. Springer, 2010\.
  * [28] G. Higman.  Ordering by divisibility in abstract algebras.  Proc. LMS, s3-2(1):326–336, 1952.
  * [29] J. E. Hopcroft and J. D. Ullman.  Introduction to Automata Theory, Languages and Computation.  Addison-Wesley, 1979.
  * [30] T. Jech.  Set Theory.  Springer, 2002.
  * [31] C. B. Jones.  Tentative steps toward a development method for interfering programs.  ACM TOPLAS, 5(4):596–619, 1983.
  * [32] M. Kabil and M. Pouzet.  Une extension d’un théorème de P. Jullien sur les âges de mots.  RAIRO Theor. Informatics Appl., 26:449–482, 1992.
  * [33] J. Leroux and S. Schmitz.  Demystifying reachability in vector addition systems.  In LICS, pages 56–67. IEEE, 2015.
  * [34] G. Markowsky.  Chain-complete posets and directed sets with applications.  Algebra Universalis, 6:53–68, 12 1976.
  * [35] E. C. Milner.  Basic WQO- and BQO-Theory, pages 487–502.  Springer, 1985.
  * [36] R. Milner.  An algebraic definition of simulation between programs.  In IJCAI, pages 481–489. Kaufmann, 1971.
  * [37] M. O. Rabin and D. Scott.  Finite automata and their decision problems.  IBM Journal of Research and Development, 3(2):114–125, 1959.
  * [38] R. Rado.  Partial well-ordering of sets of vectors.  Mathematika, 1(2):89–95, 1954.
  * [39] D. Scott.  Continuous lattices.  In Toposes, Algebraic Geometry and Logic, pages 97–136. Springer, 1972.
  * [40] R. S. Thinniyam and G. Zetzsche.  Regular separability and intersection emptiness are independent problems.  In FSTTCS, volume 150 of LIPIcs, pages 51:1–51:15. Dagstuhl, 2019.
  * [41] G. Zetzsche.  Separability by piecewise testable languages and downward closures beyond subwords.  In LICS, pages 929–938. ACM, 2018.

##  Appendix A Proofs Missing From Section 3

In all of the following sections, for any LTS
$\mathit{U}=(Q,I,\Sigma,\delta,F)$, $X\subseteq Q$, and $w,v\in\Sigma^{*}$ we
use the fact that $\delta(X,w.v)=\delta(\delta(X,w),v)$ without explicitly
mentioning it. The correctness of this statement is clear from the definition
of the extended transition relation.

#### Details on Lemma 2.2.

Let $\mathit{U}=(Q,\leq,I,\delta,F)$ be an arbitrary WSTS. We show below that
there is a countable $P$ where the WSTS $\mathit{V}=(P,\leq,I\cap
Q,\gamma,F\cap P)$ accepts $\mathit{L}(\mathit{U})$, with
$\gamma=\delta\cap(P\times\Sigma\times P)$.

######  Proof A.1 (Proof of Lemma 2.2).

We acquire a function $f:\mathit{L}(\mathit{U})\to\mathbb{P}(Q)$ that chooses
an accepting run of a word, and maps the word to the states that appear in
this run. Formally, $f:\mathit{L}(\mathit{U})\to\mathbb{P}(Q)$ such that
$f(a_{0}\ldots a_{n-1})=\\{p_{0},\ldots,p_{n}\\}$ where
$p_{i}\in\delta(I,a_{0}.....a_{i-1})$ for all $i<n$ and $p_{n}\in F$. Assume
wlog. that $\delta(p,a)$ is downward closed for all $p\in Q$ and $a\in\Sigma$.
We let $P=\bigcup_{w\in\mathit{L}(\mathit{U})}f(w)$. Since $P\subseteq Q$,
$I\cap Q\subseteq I$, $\gamma\subseteq\delta$, and $F\cap P\subseteq F$, it is
clear that $\mathit{L}(\mathit{V})\subseteq\mathit{L}(\mathit{U})$. This is
because all states reachable by some word in $\mathit{V}$ are also reachable
by it in $\mathit{U}$. We now prove
$\mathit{L}(\mathit{U})\subseteq\mathit{L}(\mathit{V})$. Let $w=a_{0}\ldots
a_{n-1}\in\mathit{L}(\mathit{U})$. Then, we have
$f(w)=\\{p_{0},\ldots,p_{n}\\}$ where
$(p_{0},a_{0},p_{1}),\ldots,(p_{n-1},a_{n-1},p_{n})\in\delta$, $p_{0}\in I$,
and $p_{n}\in F$. Since $f(w)\subseteq P$, we have
$f(w)=\\{p_{0},\ldots,p_{n}\\}$ where
$(p_{0},a_{0},p_{1}),\ldots,(p_{n-1},a_{n-1},p_{n})\in\delta$, $p_{0}\in I$,
and $p_{n}\in F$. The same sequence of transitions are also present in
$\gamma$, and we have $p_{0}\in I\cap P$ and $p_{n}\in F\cap P$. Then,
$w\in\mathit{L}(\mathit{U})$. We also know that a WQO restricted to a subset
is also a WQO. So we only need to show upward-compatibility. The condition on
final states is clear, since $F$ was upward-closed in $(Q,\leq)$, $F\cap P$ is
upward-closed in $(P,\leq)$. Towards showing $\gamma$ is upward-compatible,
let $p,q\in P$, $p\leq q$, $a\in\Sigma$, and $p^{\prime}\in\gamma(p,a)$. Since
$\gamma\subseteq\delta$, $p^{\prime}\in\delta(p,a)$ as well. We already know
that $\delta$ is upwards compatible so there is some
$q^{\prime}\in\delta(q,a)$ with $p^{\prime}\leq q^{\prime}$. Since
$\delta(q,a)$ is downward closed, we have $p^{\prime}\in\delta(q,a)$ as well.
We already know $p^{\prime}\in P$, so $p^{\prime}\in\gamma(q,a)$. This
concludes the proof.

#### Details on Lemma 3.5.

In $(\mathbb{D}(Q),\subseteq)$ where $(Q,\leq)$ is a WQO, all descending
chains stabilize [33, Fact III.3]. This condition holds for converging
lattices as well. We expect the property to be well known, but we could not
find a suitable reference for it. For the sake of completeness, we include a
proof below.

######  Lemma A.2.

Let $(Q,\leq)$ be a converging lattice and $[p_{i}]_{i\in{\rm Nature}}\in Q$ a
descending sequence. Then, there is a $n\in{\rm Nature}$ where for all $k\geq
n$, $p_{n}=p_{k}$.

######  Proof A.3.

Suppose this is not the case. Then, there is an infinite $[p_{i}]_{i\in{\rm
Nature}}\in Q$ that is strictly descending. This means we have
$p_{i+1}\not\geq p_{i}$ for all $i\in{\rm Nature}$. Per definition of
converging lattice there must be a subsequence $[p_{\phi(i)}]_{i\in{\rm
Nature}}$ that is converging. Transitivity tells that $[p_{\phi(i)}]_{i\in{\rm
Nature}}$ is also a strictly descending. Since $[p_{\phi(i)}]_{i\in{\rm
Nature}}$ converges, we must have

$\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{\phi(j)}=\bigsqcup_{i\in{\rm Nature}}p_{\phi(i)}.$

We know that
$\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
0}p_{\phi(j)}\leq\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
1}p_{\phi(j)}$, which means that we can remove
$\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
0}p_{\phi(j)}$ from the join on the left without changing the result. We
acquire

$p_{\phi(0)}\leq\bigsqcup_{i\in{\rm Nature}}p_{\phi(i)}=\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{\phi(j)}=\bigsqcup_{i\geq
1}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{\phi(j)}\leq p_{\phi(1)}.$

Final inequality follows from
$\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
1}p_{\phi(j)}\leq p_{\phi(1)}$ for all $i\in{\rm Nature}$. We get
$p_{\phi(0)}\leq p_{\phi(1)}$, which is a contradiction to strictness.

######  Proof A.4 (Proof of Lemma 3.5).

Let $(Q,\leq)$ be a quasi order. The forward direction is given in [38]. For
the backward direction, we use the observation in Lemma A.2. It says that
there are no strictly descending infinite sequences in
$(\mathbb{D}(Q),\subseteq)$. This is a characterization of WQO’s [33, Fact
III.3].

#### Details on Proposition 3.9.

We first show the forward direction. Namely, for any
$\mathit{U}=(Q,\subseteq,\mathord{\downarrow}I,\Sigma,\delta,F)\in\text{WSTS}$,
$\mathit{U}^{\mathit{det}}=(\mathbb{D}(Q),\subseteq,\mathord{\downarrow}I,\Sigma,\delta^{\mathit{det}},F^{\mathit{det}})\in
CTS$.

######  Proof A.5 (Proof of Proposition 3.9, Forward Direction).

It is clear per Lemma 3.5 that $(\mathbb{D}(Q),\subseteq)$ is a converging
lattice. To see that transitions are Scott-continuous, let $[X_{i}]_{i\in
A}\in\mathbb{D}(Q)$ with $\delta^{\mathit{det}}(\bigcup_{i\in A}X_{i},a)=Y$.
This is defined as $\delta^{\mathit{det}}(\bigcup_{i\in
A}X_{i},a)=\bigcup_{i\in A}\delta^{\mathit{det}}(X_{i},a)$. It only remains to
show finite acceptance. Let $\bigcup_{i\in A}X_{i}\in F^{\mathit{det}}$.
Definition of $F^{\mathit{det}}$, tells us that there is a $p\in F$ with
$p\in\bigcup_{i\in A}X_{i}$. Therefore, $p\in X_{i}$ for some $i\in{\rm
Nature}$. We get $X_{i}\in F^{\mathit{det}}$. This is a trivial finite join of
a single element, $X_{i}$.

The reverse direction is more involved. Let
$\mathit{U}=(Q,\leq,I,\Sigma,\delta,F)$ be a CTS. We define the set of Join
Prime Elements $\mathsf{JP}(Q)$. We let $p\in\mathsf{JP}(Q)\subseteq Q$ if and
only if

$\text{for all }\\{q_{i}\mid i\in A\\}\subseteq Q\text{ with
}p\leq\bigsqcup_{i\in A}q_{i}\text{ there is }i\in A\text{ with }p\leq q_{i}\
.$

Each element in the lattice can be acquired by a join of elements in
$\mathsf{JP}(Q)$.

######  Lemma A.6.

For all $p\in Q$, there is a $\\{q_{i}\mid i\in A\\}\subseteq Q$ such that
$p=\bigsqcup_{i\in A}q_{i}$.

######  Proof A.7.

Suppose there is a $p\not\in\mathsf{JP}(Q)$ that is not expressible by a join
of $\mathsf{JP}(Q)$ elements. We will inductively build a strictly descending
infinite sequence $[p_{i}]_{i\in{\rm Nature}}$. This is a contradiction to
Lemma A.2. As our invariant, we require for the strictly descending finite
segment $p_{0},\ldots,p_{n}$, that $p_{n}\not\in\mathsf{JP}(Q)$ can not be
expressed by a join of elements in $\mathsf{JP}(Q)$. For the base case, we let
$p_{0}=p\not\in\mathsf{JP}(Q)$ and we already have that $p$ inexpressible by a
join in $\mathsf{JP}(Q)$. For the inductive case, let $p_{0},\ldots,p_{n}$ a
strictly descending sequence with $p_{n}\not\in\mathsf{JP}(Q)$ inexpressible
by a join of elements in $\mathsf{JP}(Q)$. Since $p_{n}\not\in\mathsf{JP}(Q)$,
there must be a join $p_{n}\leq\bigsqcup_{i\in A}q_{i}$ where for all $i\in
A$, we have $p_{n}\not\leq q_{i}$. We can apply a meet with $p_{n}$ on both
sides and get $p_{n}\leq(\bigsqcup_{i\in A}q_{i})\sqcap p_{n}=\bigsqcup_{i\in
A}(q_{i}\sqcap p_{n})=p_{n}$. The last equality makes use of the fact
$p_{n}\leq\bigsqcup_{i\in A}q_{i}$. For any $i\in{\rm Nature}$, we have
$p_{n}\not\leq q_{i}$, so also $p_{n}\sqcap q_{i}\neq p_{n}$. In particular,
we observe $p_{n}\sqcap q_{i}<p_{n}$ for all $i\in{\rm Nature}$. If
$q_{i}\sqcap p_{n}$ were to be expressible by a join in $\mathsf{JP}(Q)$ for
all $i\in A$, then so would be $p_{n}$. Therefore, there must be a
$q_{i}\sqcap p_{n}\not\in\mathsf{JP}(Q)$ that is not expressible by a join in
$\mathsf{JP}(Q)$. Letting $p_{n+1}=q_{i}\sqcap p_{n}<p_{n}$ concludes the
proof.

We show that $\mathsf{JP}(Q)$ is a well quasi order. This is essential to
constructing the WSTS equivalent to $\mathit{U}$.

######  Lemma A.8.

$(\mathsf{JP}(Q),\leq)$ is a well quasi ordering.

######  Proof A.9.

Let $[p_{i}]_{i\in{\rm Nature}}\in\mathsf{JP}(Q)$ be a sequence of join
irreducible elements. We will derive two indices $a<b$ with $p_{a}\leq p_{b}$.
Per convergence, we have a subsequence $[p_{\phi(i)}]_{i\in N}$ that
converges. We get

$\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{\phi(j)}=\bigsqcup_{i\in{\rm Nature}}p_{\phi(i)}.$

For $a\in{\rm Nature}$, we get the meet of both sides with $p_{\phi(a)}$. This
results in

$\displaystyle\bigl{(}\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{\phi(i)}\bigr{)}\sqcap p_{\phi(a)}$
$\displaystyle=\bigl{(}\bigsqcup_{i\in N}p_{\phi(j)}\bigr{)}\sqcap
p_{\phi(a)}.$ We apply lattice absorbtion and distribution to get
$\displaystyle\bigsqcup_{i\in
N}\bigl{(}p_{\phi(a)}\sqcap\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{\phi(j)}\bigr{)}$ $\displaystyle=p_{\phi(a)}.$

Since $p_{\phi(a)}$ is join prime, there must be a $i\in{\rm Nature}$ with
$p_{\phi(a)}\leq
p_{\phi(a)}\sqcap\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{\phi(j)}$. Then, per lattice rules,
$p_{\phi(a)}\leq\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{\phi(j)}\leq p_{\phi(b)}$ for any $b\geq i$. Then we choose $b\geq i$
with $b>a$, and get $p_{\phi(a)}\leq p_{\phi(b)}$ with $\phi(a)\leq\phi(b)$.
This concludes the proof.

######  Proof A.10 (Proof of Proposition 3.9, Backward Direction).

We now construct a WSTS that accepts the same language as $\mathit{U}$. We
claim that $\mathit{V}=(\mathsf{FJP}(Q),\sqsubseteq,I,\Sigma,\gamma,G)$ is a
WSTS with $\mathit{L}(\mathit{V})=\mathit{L}(\mathit{U})$, where
$\mathsf{FJP}(Q)=\\{X\subseteq\mathsf{JP}(Q)\mid X\text{ finite}\\}$, and

$\displaystyle X\sqsubseteq Y$ $\displaystyle\text{ iff }\bigsqcup
X\leq\bigsqcup Y$ $\displaystyle I$
$\displaystyle=\\{X\in\mathsf{FJP}(Q)\mid\bigsqcup X\leq y\\}$ $\displaystyle
G$ $\displaystyle=\\{X\in\mathsf{FJP}(Q)\mid\bigsqcup X\in F\\}$
$\displaystyle\gamma(X,a)$ $\displaystyle=\\{Y\in\mathsf{FJP}(Q)\mid\bigsqcup
Y\leq\delta(\bigsqcup X,a)\\}\ .$

We first show that $\mathit{V}$ is a WSTS. Per Lemma A.8, we know that
$(\mathsf{JP}(Q),\leq)$ is a WQO. The order $(\mathsf{FJP}(Q),\sqsubseteq)$ is
isomorphic to $\subseteq$ on the downward closed finite subsets of
$\mathsf{JP}(Q)$. It is well known that this is also WQO [28]. We need to show
upward-compatibility. First, we show that $G$ is upward closed. Let $X\in G$
and $X\sqsubseteq Y$. Then, $\bigsqcup X\leq\bigsqcup Y$ and $\bigsqcup X\in
F$. Since $F$ is upward-closed, $\bigsqcup Y\in G$ as well. So $Y\in G$. For
the transitions, let $X\sqsubseteq Y$ and $X^{\prime}\in\gamma(X,a)$. Then,
$\bigsqcup X^{\prime}\leq\delta(\bigsqcup X,a)$. Since $X\sqsubseteq Y$, then
$\bigsqcup X\leq\bigsqcup Y$. Per upward-compatibility of $\mathit{U}$ and
determinicity, we have $\delta(\bigsqcup X,a)\leq\delta(\bigsqcup Y,a)$.
Combining this with the previous inequality we get $\bigsqcup
X^{\prime}\leq\delta(\bigsqcup Y,a)$. Therefore $X^{\prime}\in\gamma(Y,a)$.

We now proceed with the proof of
$\mathit{L}(\mathit{U})=\mathit{L}(\mathit{V})$ under two assumptions. First,
(i) for all $w\in\Sigma^{*}$ and $X_{0},X_{1}\in\gamma(I,w)$, we assume
$X_{0}\cup X_{1}\in\gamma(I,w)$. Second, (ii) for all $w\in\Sigma^{*}$, we
assume $\bigsqcup\\{\bigsqcup X\mid X\in\gamma(I,w)\\}=\delta(y,w)$. We will
prove these assumptions once we have shown
$\mathit{L}(\mathit{U})=\mathit{L}(\mathit{V})$. Towards showing the forward
inclusion, let $w\in\mathit{L}(\mathit{U})$. Then $\delta(y,w)\cap
F\neq\emptyset$. Since CTS are deterministic, $\delta(y,w)\in F$. Per
assumption (ii), we have $\bigsqcup\\{\bigsqcup X\mid
X\in\gamma(I,w)\\}=\delta(y,w)\in F$. By finite acceptance in $\mathit{U}$,
there must be $X_{0},\ldots,X_{k}\in\gamma(I,w)$ with $\bigsqcup\\{\bigsqcup
X_{i}\mid i\leq k\\}=\bigsqcup\bigcup_{i\leq k}X_{i}\in F$. We apply
assumption (i) and get $\bigcup_{i\leq k}X_{i}\in\gamma(I,w)$. Thus
$\bigcup_{i\leq k}X_{i}\in G$ as well. Then $\gamma(I,w)\cap G\neq\emptyset$.
This means $w\in\mathit{L}(\mathit{V})$. Towards showing the backward
inclusion, let $w\in\mathit{L}(\mathit{V})$. Then, $\gamma(I,w)\cap
G\neq\emptyset$. There must be some $X\in\gamma(I,w)$ with $X\in G$ and thus
$\bigsqcup X\in F$. We show that $\delta(y,w)\in F$, which implies
$w\in\mathit{L}(\mathit{U})$. We apply assumption (ii) and get
$\delta(y,w)=\bigsqcup\\{\bigsqcup Y\mid Y\in\gamma(I,w)\\}\geq\bigsqcup X\in
F$. Since $F$ is upward closed, we observe $\delta(y,w)\in F$.

Now, we show our assumptions. We proceed by assumption (i) and prove it by
induction on $|w|$. For the base case we have $w=\varepsilon$. Let
$X_{0},X_{1}\in\gamma(I,\varepsilon)=I$. Then $\bigsqcup X_{0},\bigsqcup
X_{1}\leq y$. So we have $\bigsqcup X_{0}\cup X_{1}\leq y$ as well. Per
definition of $I$, $X_{0}\cup X_{1}\in I$ holds. For the inductive case, we
handle $w=v.a\in\Sigma^{*}$. Let $X_{0},X_{1}\in\gamma(I,v.a)$. Then, there
are $Y_{0},Y_{1}\in\gamma(I,v)$ with
$(X_{0},a,Y_{0}),(X_{1},a,Y_{1})\in\gamma$. We also apply the induction
hypothesis and get $Y_{0}\cup Y_{1}\in\gamma(I,v)$. By definition, we have
$\bigsqcup X_{i}\leq\delta(\bigsqcup Y_{i},a)$ for $i\in\\{0,1\\}$. So,
$\bigsqcup(X_{0}\cup X_{1})=\bigsqcup X_{0}\sqcup\bigsqcup
X_{1}\leq\delta(\bigsqcup Y_{0},a)\sqcup\delta(\bigsqcup Y_{1},a)$. Per Scott
continuity, $\delta(\bigsqcup Y_{0},a)\sqcup\delta(\bigsqcup
Y_{1},a)=\delta(\bigsqcup Y_{0}\sqcup\bigsqcup
Y_{1},a)=\delta(\bigsqcup(Y_{0}\cup Y_{1}),a)$. Combining these inequalities
with the definition of $\gamma$, we get $X_{0}\cup X_{1}\in\gamma(Y_{0}\cup
Y_{1},a)$. Since $Y_{0}\cup Y_{1}\in\gamma(I,v)$, we have $X_{0}\cup
X_{1}\in\gamma(I,v.a)$ as well.

Now we prove assumption (ii) by induction on $|w|$. For the base case, we have
$w=\varepsilon$. Then, $p=\bigsqcup\\{\bigsqcup X\mid
X\in\gamma(I,\varepsilon)\\}=\bigsqcup\\{\bigsqcup X\mid X\in I\\}$. Since
$\bigsqcup X\leq y$ for all $X\in I$, we also have $p\leq y$. Now let
$y=\bigsqcup_{i\in A}s_{i}$ with $\\{s_{i}\mid i\in
A\\}\subseteq\mathsf{JP}(Q)$, per Lemma A.6. Then, $s_{i}\leq y$ and thus
$\\{s_{i}\\}\in I$ for all $i\in A$. The join $p=\bigsqcup\\{\bigsqcup X\mid
X\in I\\}$, includes $\bigsqcup_{i\in A}s_{i}$, so we have $p\geq y$ and thus
$p=y$. For the inductive case, let $w=v.a$. We write
$\delta(I,v.a)=\delta(\delta(I,v),a)$. We apply the induction hypothesis and
get $\delta(I,v)=\bigsqcup\\{\bigsqcup X\mid X\in\gamma(I,w)\\}$. Then,
$\delta(\delta(I,v),a)=\delta(\bigsqcup\\{\bigsqcup X\mid
X\in\gamma(I,w)\\},a)$. Under the assumption $\delta(\bigsqcup
X,a)=\bigsqcup\\{\bigsqcup Y\mid Y\in\gamma(Y,a)\\}$, which we will show
shortly, we observe:

$\displaystyle\delta(\bigsqcup\\{\bigsqcup X\mid X\in\gamma(I,w)\\},a)$
$\displaystyle=\bigsqcup\\{\delta(\bigsqcup X,a)\mid X\in\gamma(I,w)\\}$
$\displaystyle=\bigsqcup\\{\bigsqcup\\{\bigsqcup Y\mid Y\in\gamma(X,a)\\}\mid
X\in\gamma(I,v)\\}$ $\displaystyle=\bigsqcup\\{\bigsqcup Y\mid
Y\in\gamma(I,v.a)\\}.$

To prove our assumption $\delta(\bigsqcup X,a)=\bigsqcup\\{\bigsqcup Y\mid
Y\in\gamma(Y,a)\\}$, we derive

$\displaystyle\bigsqcup\\{\bigsqcup Y\mid Y\in\gamma(X,a)\\}$
$\displaystyle\leq\delta(\bigsqcup X,a)$
$\displaystyle=\bigsqcup\\{s\in\mathsf{JP}(Q)\mid
s\leq\delta(X,a)\\}\leq\bigsqcup\\{\bigsqcup Y\mid Y\in\gamma(X,a)\\}.$

The initial inequality is by the definition of $\gamma(X,a)$. It consists of
$Y\in\mathsf{FJP}(Q)$ where $\bigsqcup Y\leq\delta(X,a)$. Therefore, the join
is also smaller. The equality that follows it acquires the join of
$\mathsf{JP}(Q)$ elements that expresses $\delta(\bigsqcup X,a)$, guaranteed
per Lemma A.6. The final inequality follows from the observation
$\\{s\\}\in\gamma(X,a)$ for all $s\in\mathsf{JP}(Q)$ with $s\leq\delta(X,a)$.

#### Details on Lemma 3.11.

We now show that CTS are closed under product construction. Let
$\mathit{U}=(Q,\leq,I,\Sigma,\delta,F)$ and
$\mathit{V}=(P,\sqsubseteq,I,\Sigma,\gamma,G)$ be CTS. We show that
$\mathit{U}\times\mathit{V}$ is a CTS.

######  Proof A.11 (Proof of Lemma 3.11).

We start by showing that the product order $(Q\times P,\leq_{\times})$ is a
converging lattice. Usual lattice properties carry over, with the join
$\bigsqcup_{i\in K}(p_{i},q_{i})=(\bigsqcup_{i\in K}p_{i},\bigsqcup_{i\in
K}q_{i})$ and the meet
$\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{i\in
K}(p_{i},q_{i})=(\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{i\in
K}p_{i},\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{i\in
K}q_{i})$. The symbols $\sqcup$ and $\sqcap$ refer to respective operations in
$(Q,\leq)$ when used on elements from $Q$, and to those in $(P,\sqsubseteq)$
when used on elements from $P$. Let $[(p_{i},q_{i})]_{i\in{\rm Nature}}\in
Q\times P$ be a sequence. Then, since $(Q,\leq)$ is a converging lattice,
there is a subsequence $[p_{\phi(i)}]_{i\in{\rm Nature}}$ that converges in
$(Q,\leq)$. We also apply this to the other side, and acquire a subsequence
$[q_{\phi(\psi(i))}]_{i\in{\rm Nature}}$ of $[q_{\phi(i)}]_{i\in{\rm Nature}}$
that converges in $(P,\sqsubseteq)$. Subsequences of converging sequences also
converge. Then, $[p_{\phi(\psi(i))}]_{i\in{\rm Nature}}$ also converges. We
get the below equalities. The second equality is acquired by the convergence
of component sequences.

$\displaystyle\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}(p_{\phi(\psi(j))},q_{\phi(\psi(j))})$ $\displaystyle=(\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{\phi(\psi(j))},\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}q_{\phi(\psi(j))})$ $\displaystyle=(\bigsqcup_{i\in{\rm
Nature}}p_{\phi(\psi(i))},\bigsqcup_{i\in{\rm
Nature}}q_{\phi(\psi(i))})=\bigsqcup_{i\in{\rm Nature}}(p_{i},q_{i})$

We now show Scott continuity. Let $\bigsqcup_{i\in K}(p_{i},q_{i})\in Q\times
P$. The Scott continuity follows from the continuity of the individual
components. Transition relations in the product $\mathit{U}\times\mathit{V}$
is expressed by the symbol $\delta_{\times}$.

$\displaystyle\delta_{\times}(\bigsqcup_{i\in K}(p_{i},q_{i}),a)$
$\displaystyle=(\delta_{\times}((\bigsqcup_{i\in K}p_{i},\bigsqcup_{i\in
K}q_{i}),a)=(\delta(\bigsqcup_{i\in K}p_{i},a),\gamma(\bigsqcup_{i\in
K}q_{i},a))$ $\displaystyle=(\bigsqcup_{i\in K}\delta(p_{i},a),\bigsqcup_{i\in
K}\gamma(q_{i},a))=\bigsqcup_{i\in K}(\delta(p_{i},a),\gamma(q_{i},a))$
$\displaystyle=\bigsqcup_{i\in K}\delta_{\times}((p_{i},q_{i}),a)$

We conclude the proof by the finite acceptance. Let $\bigsqcup_{i\in
K}(p_{i},q_{i})=(\bigsqcup_{i\in K}p_{i},\bigsqcup_{i\in K}q_{i})\in F\times
G$. Then $\bigsqcup_{i\in K}p_{i}\in F$ and $\bigsqcup_{i\in K}q_{i}\in G$. By
finite acceptance of $\mathit{U}$ and $\mathit{V}$, there must be finite
$K^{\prime},L^{\prime}\subseteq K$ with $\bigsqcup_{i\in K^{\prime}}p_{i}\in
F$ and $\bigsqcup_{i\in L^{\prime}}q_{i}\in G$. Then, $\bigsqcup_{i\in
K^{\prime}\cup L^{\prime}}p_{i}\in F$ and $\bigsqcup_{i\in K^{\prime}\cup
L^{\prime}}q_{i}\in G$ by upward-compatibility. Therefore, $(\bigsqcup_{i\in
K^{\prime}\cup L^{\prime}}p_{i},\bigsqcup_{i\in K^{\prime}\cup
L^{\prime}}q_{i})\in F\times G$. This is equal to $\bigsqcup_{i\in
K^{\prime}\cup L^{\prime}}(p_{i},q_{i})\in F\times G$. The set $K^{\prime}\cup
L^{\prime}$ is also finite, which concludes the proof.

#### Details on Lemma 3.13:

The result $S\subseteq\mathit{cl}(S)$ is clear, since any sequence where every
element is equal to $p\in Q$ converges to $p$. We show
$\mathit{cl}(S)=\mathit{cl}(\mathit{cl}(S))=\mathord{\downarrow}\mathit{cl}(S)$
below.

######  Proof A.12 (Proof of Lemma 3.13).

We proceed by showing $\mathit{cl}(S)=\mathord{\downarrow}\mathit{cl}(S)$. Let
$p\in\mathit{cl}(S)$ and $q\in Q$ with $q\leq p$. Since $p\in\mathit{cl}(S)$,
there is a converging sequence $[p_{i}]_{i\in{\rm Nature}}\in S$ with
$\bigsqcup_{i\in{\rm Nature}}p_{i}=p$. Note that $S$ is downward closed and
$p_{i}\sqcap q\leq p_{i}$, so for all $i\in{\rm Nature}$, we get $p_{i}\sqcap
q\in S$ for all $i\in{\rm Nature}$. We now show that $[p_{i}\sqcap
q]_{i\in{\rm Nature}}\in S$ converges to $q$ and therefore
$q\in\mathit{cl}(S)$. We apply a meet with $q$ on both sides and get

$\displaystyle\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{j}$ $\displaystyle=\bigsqcup_{i\in{\rm Nature}}p_{i}=p$
$\displaystyle\bigl{(}\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{j}\bigr{)}\sqcap q$ $\displaystyle=\bigl{(}\bigsqcup_{i\in{\rm
Nature}}p_{i}\bigr{)}\sqcap q=p\sqcap q=q$ $\displaystyle\bigsqcup_{i\in{\rm
Nature}}\bigl{(}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}p_{j}\sqcap q\bigr{)}$ $\displaystyle=\bigsqcup_{i\in{\rm
Nature}}\bigl{(}p_{i}\sqcap q\bigr{)}=q.$

Finally, we show $\mathit{cl}(S)=\mathit{cl}(\mathit{cl}(S))$. Here, we need
the countability of $Q$, or in particular, of $\mathsf{JP}(Q)$. It is clear
that $\mathit{cl}(S)\subseteq\mathit{cl}(\mathit{cl}(S))$ by an argument
similar to $S\subseteq\mathit{cl}(S)$. To see
$\mathit{cl}(\mathit{cl}(S))\subseteq\mathit{cl}(S)$, let
$p\in\mathit{cl}(\mathit{cl}(S))$. Then, there is a converging
$[p_{i}]_{i\in{\rm Nature}}\in\mathit{cl}(S)$. Since $p_{i}\in\mathit{cl}(S)$,
there is a converging sequence $[p_{i,j}]_{j\in{\rm Nature}}\in S$. We apply
join prime decomposition by Lemma A.6. We acquire $p=\bigsqcup_{i\in I}s_{i}$
for some $\\{s_{i}\mid i\in I\\}\subseteq\mathsf{JP}(Q)$. Since $Q$ is
countable, then so is $\mathsf{JP}(Q)$. Wlog. we exchange the index set $I$
with ${\rm Nature}$ and write $p=\bigsqcup_{i\in{\rm Nature}}s_{i}$.

By induction, we construct a sequence $[q_{i}]_{i\in{\rm Nature}}\in S$ where
for all $i\in{\rm Nature}$, $\bigsqcup_{j\leq i}s_{j}\leq q_{i}$ holds. As an
inductive invariant, we require that the finite segment
$q_{0},...,q_{n-1}\in\\{p_{i,j}\mid i,j\in{\rm Nature}\\}$ has (i) for all
$i<n$, $\bigsqcup_{j\leq i}q_{j}\leq p_{i}$, (ii) there is $\\{r_{i,j}\mid
i,j\in{\rm Nature}\\}\subseteq\\{p_{i,j}\mid i,j\in{\rm Nature}\\}$ with
$[r_{k,j}]_{j\in{\rm Nature}}$ converging to some $r_{k}$, where
$[r_{i}]_{i\in{\rm Nature}}$ converges to $p$, (iii) $(\bigsqcup_{k\leq
n-1}s_{k})\leq r_{i,j}$ for all $i,j\in{\rm Nature}$.

We consider $n=0$ as the base case, where $r_{i,j}=p_{i,j}$ and the empty
sequence satisfy all of the requirements. For the inductive case, let
$q_{0},\ldots,q_{n-1}$ be a sequence that satisfies (i), (ii), and (iii) with
$\\{r_{i,j}\mid i,j\in{\rm Nature}\\}$ being the sequence of sequences from
(ii) and (iii). Note that $[r_{i,j}]_{j\in{\rm Nature}}$ converge to some
$r_{i}$ for each $i\in{\rm Nature}$, where $[r_{i}]_{i\in{\rm Nature}}$
converges to $p$. We now find a $q_{n}\in\\{r_{i,j}\mid i,j\in{\rm Nature}\\}$
with $\bigsqcup_{i\leq n}s_{i}\leq q_{n}$, along with $\\{r_{i,j}^{\prime}\mid
i,j\in{\rm Nature}\\}\subseteq\\{r_{i,j}\mid i,j\in{\rm
Nature}\\}\subseteq\\{p_{i,j}\mid i,j\in{\rm Nature}\\}$ that satisfies (ii)
and (iii). We have $s_{n}\leq p=\bigsqcup_{i\in{\rm Nature}}\bigsqcup_{j\geq
i}r_{j}$ since $[r_{i}]_{i\in{\rm Nature}}$ converges to $p$. By join
primeness, we have an $i\in{\rm Nature}$ with
$s_{n}\leq\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{k\geq
i}r_{k}$. Then, for all $k\geq i$, $s_{n}\leq r_{k}$. Let $k\geq i$. Per
convergence of $[r_{k,j}]_{j\in{\rm Nature}}$ we have
$s_{n}\leq\bigsqcup_{j\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{l\in{\rm
Nature}}r_{j,l}$. Join primeness again gives
$s_{n}\leq\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{l\geq
j_{k}}r_{k,l}$ for some $j_{k}\in{\rm Nature}$. Then, for all $k\geq i$, and
$l\geq j_{k}$, we have $s_{n}\leq r_{k,l}$. Since $\bigsqcup_{m\leq
n-1}s_{m}\leq r_{k,l}$ for all such $k$ and $l$, we also have
$\bigsqcup_{m\leq n}s_{m}\leq r_{k,l}$. Then, in order to get a set that
satisfies (iii), we can let $r_{a,b}^{\prime}=r_{k,j_{k}+b}$, where $k=i+a$.
To see that (ii) is also satisfied, consider that infinite subsequences of
convergent sequences also converge to the same state. Then,
$[r_{a,b}^{\prime}]_{b\in{\rm Nature}}$ converges to $r_{i+a}=r_{a}^{\prime}$,
and $[r_{a}^{\prime}]_{a\in{\rm Nature}}$ converges to $p$. We choose
$q_{n+1}=r_{0,0}^{\prime}\geq\bigsqcup_{m\leq n}s_{m}$. This satisfies (i) and
concludes the inductive case.

We claim that the infinite sequence $[q_{i}]_{i\in{\rm Nature}}$ converges to
$p=\bigsqcup_{i\in{\rm Nature}}s_{i}$. First, observe that
$\bigsqcup_{i\in{\rm Nature}}q_{i}\leq p$. This is because
$[p_{i,j}]_{j\in{\rm Nature}}$ converges to $p_{i}$ for all $i\in{\rm
Nature}$, and $[p_{i}]_{i\in{\rm Nature}}$ converges to $p$. Then,
$p=\bigsqcup_{i,j\in{\rm Nature}}p_{i,j}$ where we have $\\{q_{i}\mid i\in{\rm
Nature}\\}\subseteq\\{p_{i,j}\mid i,j\in{\rm Nature}\\}$. We now show that
$p\leq\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}q_{j}$. This is sufficient for showing $\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}q_{j}=\bigsqcup_{i\in{\rm Nature}}q_{j}=p$, because $\bigsqcup_{i\in{\rm
Nature}}q_{i}\geq\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}q_{j}$ always holds. The latter fact follows from
$q_{i}\leq\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}q_{j}$ for all $i\in{\rm Nature}$. By applying the properties of
$[q_{i}]_{i\in{\rm Nature}}$ we get

$\displaystyle\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}q_{j}\geq\bigsqcup_{i\in{\rm
Nature}}\mathop{\mathchoice{\rotatebox[origin={c}]{180.0}{$\displaystyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\textstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle\bigsqcup$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle\bigsqcup$}}}_{j\geq
i}\bigsqcup_{k\leq j}s_{k}=\bigsqcup_{i\in{\rm Nature}}\bigsqcup_{k\leq
i}s_{k}=\bigsqcup_{i\in{\rm Nature}}s_{i}=p.$

For the first inequality, we employ $\bigsqcup_{k\leq j}s_{j}\leq q_{j}$ for
all $j\in{\rm Nature}$. For the following equality, we observe that
$\bigsqcup_{k\leq i}s_{i}$ is the smallest element in the meet. Then, we
reorganize the joins. This results in the join of $\mathsf{JP}(Q)$ elements
that represent $p$.

##  Appendix B Proofs Missing From Section 4

#### Details on Lemma 4.5.

We show the upward-compatibility of $\mathit{U}_{R}$. For states $x,y\in R$
with $x\leq_{R}y$, letter $b$, and $x$-successor $z\in\delta(x,b)$, we show
there is a $y$-successor $z^{\prime}\in\delta(y,b)$ with
$z\leq_{R}z^{\prime}$. During the proof, we let $x=(c,r)$ and
$y=(c^{\prime},r^{\prime})$.

######  Proof B.1 (Proof of Lemma 4.5).

Since $x\leq_{R}y$, we have $r\leq c^{\prime}$ or ($c=c^{\prime}$ and $r\leq
r^{\prime}$). We do a case distinction along the letters.

#### Case $a$.

Then $\delta((c,r),a)={(c+1,r+1)}$ and
$\delta((c^{\prime},r^{\prime}),a)={(c^{\prime}+1,r^{\prime}+1)}$. If $r\leq
r^{\prime}$ and $c=c^{\prime}$, then $r+1\leq r^{\prime}+1$ and
$c+1=c^{\prime}+1$. If $r\leq c^{\prime}$, then $r+1\leq c^{\prime}+1$.

#### Case $\bar{a}$.

If $c=0$, there is no transition from $(c,r)$. So consider $c>0$. The
transition is now allowed, and we see $\delta((c,r),\bar{a})={(c-1,r-1)}$. If
$c=c^{\prime}$, we also have $c^{\prime}>0$. This also holds if $r\leq
c^{\prime}$, since $r>c>0$. Then,
$\delta((c^{\prime},r^{\prime}),\bar{a})={(c^{\prime}-1,r^{\prime}-1)}$. The
argument for $(c-1,r-1)\leq_{R}(c^{\prime}-1,r^{\prime}-1)$ is like in the
previous case.

#### Case $\mathit{zero}$.

Transitions labeled $\mathit{zero}$ are not activated from row or column $1$.
Therefore, we can assume $c\neq 1$ and $r>1$. Let $c^{\prime}=0$. Assume
$c=c^{\prime}=0$ and $r\leq r^{\prime}$. Then we have
$\delta((c,r),\mathit{zero})={(0,r-1)}$ and
$\delta((c^{\prime},r^{\prime}),\mathit{zero})={(0,r^{\prime}-1)}$, with
$r\leq r^{\prime}$. Therefore $(0,r-1)\leq_{R}(0,r^{\prime}-1)$ as well. The
case $r\leq c^{\prime}$ can not happen as $r>1$ per definition of $R$. Let
$c=0$ and assume $c<c^{\prime}$, since $c^{\prime}=0$ has already been
covered. Then, $\delta((c,r),\mathit{zero})={(0,r-1)}$ and
$\delta((c^{\prime},r^{\prime}),\mathit{zero})={(0,c^{\prime}-1)}$. Since
$c\neq c^{\prime}$, $r\leq c^{\prime}$ must hold, and so
$(0,r-1)\leq_{R}(0,c^{\prime}-1)$. Finally, let $c,c^{\prime}>0$. Note that
$c\neq 1$ and $c,c^{\prime}>0$, necessarily gives $c,c^{\prime}\geq 2$. Then,
the $\mathit{zero}$ transition is activated from both of $(c,r)$ and
$(c^{\prime},r^{\prime})$. So we get $\delta((c,r),\mathit{zero})={(0,c-1)}$
and $\delta((c^{\prime},r^{\prime}),\mathit{zero})={(0,c^{\prime}-1)}$. Let
$c=c^{\prime}$ and $r\leq r^{\prime}$. Then we have
$(0,c-1)=(0,c^{\prime}-1)$, satisfying the condition. Let $r\leq c^{\prime}$.
Then, we have $c<r\leq c^{\prime}$ and therefore
$(0,c-1)\leq_{R}(0,c^{\prime}-1)$.

##  Appendix C Proofs Missing From Section 5

#### Details on Lemma 5.1.

Let $\mathit{U}=(Q,\leq,I,\delta,F)$ and
${\mathit{U}}^{\mathit{rev}}=(Q,\leq,F,\delta^{rev},\mathord{\downarrow}I)$.
We recall the definition

${\delta}^{\mathit{rev}}=\\{(p,a,q)\mid(q,a,p^{\prime})\in\delta,p\leq
p^{\prime}\\}.$

We now show
${\mathit{L}(\mathit{U})}^{\mathit{rev}}=\mathit{L}({\mathit{U}}^{\mathit{rev}})$.

######  Proof C.1 (Proof of Lemma 5.1).

We first show that ${\mathit{U}}^{\mathit{rev}}$ is downward-compatible. The
final states, $\mathord{\downarrow}I$, are downward-closed by definition. To
show that the condition on transitions is also satisfied, let $p,q\in Q$ and
$a\in\Sigma$ with $p\leq q$, $(q,a,q^{\prime})\in{\delta}^{\mathit{rev}}$. Per
definition, there must be a $r\geq q$ with $(q^{\prime},a,r)\in\delta$. Then,
since $p\leq q\leq r$, we also have
$(p,a,q^{\prime})\in{\delta}^{\mathit{rev}}$. This concludes the proof of
upward-compatibility. We do a case distinction along the letters.

Now we show
${\mathit{L}(\mathit{U})}^{\mathit{rev}}=\mathit{L}({\mathit{U}}^{\mathit{rev}})$.
First, we make an assumption that we prove later:
$\mathord{\downarrow}\delta(X,w)\cap Y\neq\emptyset$ if and only if
$\mathord{\uparrow}{\delta}^{\mathit{rev}}(Y,{w}^{\mathit{rev}})\cap
X\neq\emptyset$ for all $X,Y\subseteq Q$ and $w\in\Sigma^{*}$. Now we prove
$\mathit{L}({\mathit{U}}^{\mathit{rev}})={\mathit{L}(\mathit{U})}^{\mathit{rev}}$.
Let $w\in{\mathit{L}(\mathit{U})}^{\mathit{rev}}$. Then
$\delta(I,{w}^{\mathit{rev}})\cap F\neq\emptyset$. We see
$\mathord{\uparrow}{\delta}^{\mathit{rev}}(F,w)\cap I\neq\emptyset$ and thus
${\delta}^{\mathit{rev}}(F,w)\cap\mathord{\downarrow}I\neq\emptyset$. So
$w\in\mathit{L}({\mathit{U}}^{\mathit{rev}})$. Now let
$w\in\mathit{L}({\mathit{U}}^{\mathit{rev}})$. Then
${\delta}^{\mathit{rev}}(F,w)\cap\mathord{\downarrow}I\neq\emptyset$. We get
$\mathord{\downarrow}\delta(\mathord{\downarrow}I,{w}^{\mathit{rev}})\cap
F\neq\emptyset$. Since $F$ is upward-closed, then
$\delta(\mathord{\downarrow}I,{w}^{\mathit{rev}})\cap F\neq\emptyset$. This
means that there must be $p\in I$ with $p^{\prime}\leq p$,
$q^{\prime}\in\delta(p^{\prime},{w}^{\mathit{rev}})$, and $q^{\prime}\in F$.
By standard induction on word length, we see that there must be a
$q\in\delta(p,{w}^{\mathit{rev}})$ with $q^{\prime}\leq q$. Since $F$ is
upward-closed, $q\in F$ and thus
${w}^{\mathit{rev}}\in\mathit{L}(\mathit{U})$. Therefore
$w\in{\mathit{L}(\mathit{U})}^{\mathit{rev}}$.

Finally we prove our assumption by induction on $|w|$. The base case is
$w={w}^{\mathit{rev}}=\varepsilon$. Let $X,Y\subseteq Q$. For the forward
direction, we have
$\mathord{\downarrow}\delta(X,\varepsilon)=\mathord{\downarrow}X$ and
$\mathord{\uparrow}{\delta}^{\mathit{rev}}(Y,\varepsilon)=\mathord{\uparrow}Y$.
We get $\mathord{\downarrow}\delta(X,\varepsilon)\cap
Y=\mathord{\downarrow}X\cap Y\neq\emptyset$. This implies
$X\cap\mathord{\uparrow}Y=\mathord{\uparrow}\delta(Y,\varepsilon)\cap
X\neq\emptyset$. The backward direction is handled similarly.

For the inductive case, let $w\in\Sigma^{*}$ with $w=a.v=u.b$ for some
$a,b\in\Sigma$ and $X,Y\subseteq Q$. To prove the forward direction, assume
$\mathord{\downarrow}\delta(X,a.v)\cap Y\neq\emptyset$. This is the same as
$\mathord{\downarrow}\delta(\delta(X,a),v)\cap Y\neq\emptyset$. Induction
hypothesis, tells us
$\mathord{\uparrow}{\delta}^{\mathit{rev}}(Y,{v}^{\mathit{rev}})\cap\delta(X,a)\neq\emptyset$.
So, there is $p\in X$, $(p,a,q)\in\delta$, along with a
$q^{\prime}\in{\delta}^{\mathit{rev}}(Y,{v}^{\mathit{rev}})$ with
$q^{\prime}\leq q$. By definition of ${\delta}^{\mathit{rev}}$, we also
observe $(q^{\prime},a,p)\in{\delta}^{\mathit{rev}}$. Since we know
$\mathord{\uparrow}{\delta}^{\mathit{rev}}(Y,{v}^{\mathit{rev}}.a)=\mathord{\uparrow}{\delta}^{\mathit{rev}}({\delta}^{\mathit{rev}}(Y,{v}^{\mathit{rev}}),a)$,
$q^{\prime}\in{\delta}^{\mathit{rev}}(Y,{v}^{\mathit{rev}})$, and
$(q^{\prime},a,p)\in{\delta}^{\mathit{rev}}$, we see
$p\in{\delta}^{\mathit{rev}}({\delta}^{\mathit{rev}}(Y,{v}^{\mathit{rev}}),a)$.
We also had $p\in X$, so
$\mathord{\uparrow}{\delta}^{\mathit{rev}}(Y,{v}^{\mathit{rev}}.a)\cap
X\neq\emptyset$.

To prove the backward direction, assume
$\mathord{\uparrow}{\delta}^{\mathit{rev}}(Y,b.{u}^{\mathit{rev}})\cap
X\neq\emptyset$. This is the same as
$\mathord{\uparrow}{\delta}^{\mathit{rev}}({\delta}^{\mathit{rev}}(Y,b),{u}^{\mathit{rev}})\cap
X\neq\emptyset$. Applying the induction hypothesis we observe
$\mathord{\downarrow}\delta(X,u)\cap{\delta}^{\mathit{rev}}(Y,b)\neq\emptyset$.
Therefore, there must be $p\in Y$, $(p,b,q)\in{\delta}^{\mathit{rev}}$, and a
$q^{\prime}\in\delta(X,u)$ with $q\leq q^{\prime}$. We show
$p\in\mathord{\downarrow}\delta(X,u.b)$. Because
$(p,b,q)\in{\delta}^{\mathit{rev}}$, there must be a $p^{\prime}\geq p$ with
$(q,b,p^{\prime})\in\delta$ per definition of ${\delta}^{\mathit{rev}}$. Here,
we use upwards compatibility. Since $q^{\prime}\geq q$, there must be a
$p^{\prime\prime}\geq p^{\prime}$ and
$(q^{\prime},b,p^{\prime\prime})\in\delta$. Recall that
$q^{\prime}\in\delta(X,u)$. Then,
$p^{\prime\prime}\in\mathord{\downarrow}\delta(\delta(X,u),b)=\mathord{\downarrow}\delta(X,u.b)$.
Because $p\leq p^{\prime}\leq p^{\prime\prime}$, we get
$p\in\mathord{\downarrow}\delta(X,u.b)$. We already have $p\in Y$, so
$\mathord{\downarrow}\delta(X,u.b)\cap Y\neq\emptyset$.

#### Details on Lemma 5.2.

Let $\mathit{U}=(Q,\leq,I,\Sigma,\delta,F)$ be a deterministic ULTS. We show
that $\overline{\mathit{U}}=(Q,\leq,I,\Sigma,\delta,\overline{F})$ is a
deterministic DLTS with
$\overline{\mathit{L}(\mathit{U})}=\mathit{L}(\overline{\mathit{U}})$.

######  Proof C.2 (Proof of Lemma 5.2).

That $\overline{\mathit{U}}$ accepts the complement language is due to Rabin
and Scott. To see that $\geq$ is a simulation, consider $p_{1},q_{1},q_{2}\in
Q$, and $a\in\Sigma$ with $p_{1}\leq q_{1}$ and $q_{2}\in\delta(q_{1},a)$. By
determinism, there is $p_{2}\in\delta(p_{1},a)$. As $\leq$ is a simulation, we
obtain $q_{3}\in\delta(q_{1},a)$ with $p_{2}\leq q_{3}$. By determinism,
$q_{3}=q_{2}$ has to hold.

#### Details on Lemma 5.4.

Let
${\mathit{U}_{R}}^{\mathit{rev}}=(R,\leq,R,\Sigma,{\delta}^{\mathit{rev}},\mathord{\downarrow}I)$.
We claim that $R$ and $\delta(p,a)$ are represented by one minimal state, for
all $p\in R$ and $a\in\Sigma$.

######  Proof C.3 (Proof of Lemma 5.4).

It is easy to see that $\mathord{\uparrow}\\{(0,1)\\}=R$. For any $(c,r)\in
R$, either $c=0$, in which case $r\geq 1$, or $c>0$, in which case $c\geq 1$.
For ${\delta}^{\mathit{rev}}$, we do a case distinction along the letters. We
recall the definition ${\delta}^{\mathit{rev}}(p,a)=\\{q\in R\mid
p^{\prime}\in\delta(q,a),p\leq p^{\prime}\\}$. We use the fact that
$|\delta(q,a)|=1$ for all $q\in Q$ and $a\in\Sigma$ without explicitly
mentioning it.

#### Case $\mathit{zero}$:

We claim ${\delta}^{\mathit{rev}}((c,r),\mathit{zero})=\emptyset$ if $c>0$,
and
${\delta}^{\mathit{rev}}((0,r),\mathit{zero})=\mathord{\uparrow}\\{(0,r+1)\\}$.
The former is easy to see. Transitions labeled $\mathit{zero}$ only result in
elements in column $0$, none of which dominate an element in other columns.
Now we show the latter case. For the direction
$\mathord{\uparrow}\\{(0,r+1)\\}\subseteq{\delta}^{\mathit{rev}}((0,r),\mathit{zero})$,
let $(c^{\prime},r^{\prime})\geq_{R}(0,r+1)$. We have $c^{\prime}=0$ and
$r^{\prime}\geq r+1$, or $1\leq r+1\leq c^{\prime}$. If $c^{\prime}=0$ and
$r^{\prime}\geq r+1$, we have
$\delta((c^{\prime},r^{\prime}),\mathit{zero})=(0,r^{\prime}-1)\geq_{R}(0,r)$.
So $(c^{\prime},r^{\prime})\in{\delta}^{\mathit{rev}}((0,r),\mathit{zero})$.
If $1\leq r+1\leq c^{\prime}$ holds, then
$\delta((c^{\prime},r^{\prime}),\mathit{zero})=(0,c^{\prime}-1)\geq_{R}(0,r)$,
so $(c^{\prime},r^{\prime})\in{\delta}^{\mathit{rev}}((0,r),\mathit{zero})$ as
well. For the direction
${\delta}^{\mathit{rev}}((0,r),\mathit{zero})\subseteq\mathord{\uparrow}\\{(0,r+1)\\}$,
let $(c^{\prime},r^{\prime})\in{\delta}^{\mathit{rev}}((0,r),\mathit{zero})$.
Then,
$\delta((c^{\prime},r^{\prime}),\mathit{zero})=(0,c^{\prime}-1)\geq_{R}(0,r)$.
We deduce $c^{\prime}-1\geq r$ and $c^{\prime}\geq r+1$. Then,
$(c^{\prime},r^{\prime})\in\mathord{\uparrow}\\{(0,r+1)\\}$.

#### Case $a$:

We claim ${\delta}^{\mathit{rev}}((c,r),a)=\mathord{\uparrow}\\{(c-1,r-1)\\}$
in the case of $c>0$, and
${\delta}^{\mathit{rev}}((0,r),a)=\mathord{\uparrow}\\{(r-1,r)\\}$. Note that
since $r\geq 1$ is guaranteed by $R$, $r-1\geq 0$ holds.

We start with the former case. To see the inclusion
$\mathord{\uparrow}\\{(c-1,r-1)\\}\subseteq{\delta}^{\mathit{rev}}((c,r),a)$,
let $(c^{\prime},r^{\prime})\geq_{R}(c-1,r-1)$. Then, $c^{\prime}=c-1$ and
$r^{\prime}\geq r-1$, or $c^{\prime}\geq r-1$. We have
$\delta((c^{\prime},r^{\prime}),a)=(c^{\prime}+1,r^{\prime}+1)$. In the first
case we observe $c^{\prime}+1=c$ and $r^{\prime}+1\geq r$, so
$(c^{\prime}+1,r^{\prime}+1)\geq_{R}(c,r)$. In the second case, we observe
$c^{\prime}+1\geq r$, so again $(c^{\prime}+1,r^{\prime}+1)\geq_{R}(c,r)$.
Then, $(c^{\prime},r^{\prime})\in{\delta}^{\mathit{rev}}((c,r),a)$. For the
inclusion
${\delta}^{\mathit{rev}}((c,r),a)\subseteq\mathord{\uparrow}\\{(c-1,r-1)\\}$,
let $(c^{\prime},r^{\prime})\in{\delta}^{\mathit{rev}}((c,r),a)$. Then,
$\delta((c^{\prime},r^{\prime}),a)=(c^{\prime}+1,r^{\prime}+1)\geq_{R}(c,r)$.
So, $c^{\prime}+1=c$ and $r^{\prime}+1\geq r$, or $c^{\prime}+1\geq r$. Then,
$c^{\prime}=c-1$ and $r^{\prime}\geq r-1$ or $c^{\prime}\geq r-1$, meaning
$(c^{\prime},r^{\prime})\geq_{R}(c-1,r-1)$.

Now we handle the latter case. For the inclusion
$\mathord{\uparrow}\\{(r-1,r)\\}\subseteq{\delta}^{\mathit{rev}}((0,r),a)$,
let $(c^{\prime},r^{\prime})\geq_{R}(r-1,r)$. Then, $c^{\prime}=r-1$ and
$r^{\prime}\geq r$, or $c^{\prime}\geq r$. In any case, $c^{\prime}+1\geq r$.
We have $\delta((c^{\prime},r^{\prime}),a)=(c^{\prime}+1,r^{\prime}+1)$. Since
$c^{\prime}+1\geq r$, $(c^{\prime}+1,r^{\prime}+1)\geq_{R}(0,r)$. For the
inclusion
${\delta}^{\mathit{rev}}((0,r),a)\subseteq\mathord{\uparrow}\\{(r-1,r)\\}$,
let $(c^{\prime},r^{\prime})\in{\delta}^{\mathit{rev}}((0,r),a)$. Then we have
$\delta((c^{\prime},r^{\prime}),a)=(c^{\prime}+1,r^{\prime}+1)\geq_{R}(0,r)$.
Since $c^{\prime}\geq 0$, we have $c^{\prime}+1\neq 0$. So $c^{\prime}+1\geq
r$ must hold. We argue that this implies
$(c^{\prime},r^{\prime})\geq_{R}(r-1,r)$. If $c^{\prime}+1>r$, then
$c^{\prime}\geq r$, so $(c^{\prime},r^{\prime})\geq_{R}(r-1,r)$. If
$c^{\prime}+1=r$, then we have $r^{\prime}>c^{\prime}=r-1$ and thus
$r^{\prime}\geq r$. So $(c^{\prime},r^{\prime})\geq_{R}(r-1,r)$ as well.

#### Case $\bar{a}$:

We claim
${\delta}^{\mathit{rev}}((c,r),\bar{a})=\mathord{\uparrow}\\{(c+1,r+1)\\}$.
Toward the inclusion
$\mathord{\uparrow}\\{(c+1,r+1)\\}\subseteq{\delta}^{\mathit{rev}}((c,r),\bar{a})$,
let $(c^{\prime},r^{\prime})\geq_{R}(c+1,r+1)$. Then, $c^{\prime}=c+1$ and
$r^{\prime}\geq r+1$, or $c^{\prime}\geq r+1$. We have
$\delta((c^{\prime},r^{\prime}),\bar{a})=(c^{\prime}-1,r^{\prime}-1)$. If the
first condition holds, we have $c^{\prime}=c+1$ and $r^{\prime}\geq r+1$ so
$c^{\prime}-1=c$ and $r^{\prime}-1\geq r$. Therefore
$(c^{\prime}-1,r^{\prime}-1)\geq_{R}(c,r)$. If the second condition holds, we
have $c^{\prime}\geq r+1$ and $c^{\prime}-1\geq r$. So,
$(c^{\prime}-1,r^{\prime}-1)\geq_{R}(c,r)$ as well. This implies
$(c^{\prime},r^{\prime})\in{\delta}^{\mathit{rev}}((c,r),\bar{a})$. Towards
the inclusion
${\delta}^{\mathit{rev}}((c,r),\bar{a})\subseteq\mathord{\uparrow}\\{(c+1,r+1)\\}$,
let $(c^{\prime},r^{\prime})\in{\delta}^{\mathit{rev}}((c,r),\bar{a})$. The
$\bar{a}$ transitions are only active from columns greater than $0$, so we can
say
$\delta((c^{\prime},r^{\prime}),\bar{a})=(c^{\prime}-1,r^{\prime}-1)\geq_{R}(c,r)$.
This implies $c^{\prime}-1=c$ and $r^{\prime}-1\geq r$, or $c^{\prime}-1\geq
r$. So, we see $c^{\prime}=c+1$ and $r^{\prime}\geq r+1$, or $c^{\prime}\geq
r+1$. Therefore, $(c^{\prime},r^{\prime})\geq_{R}(c+1,r+1)$. This concludes
the proof.

#### Details on Lemma 5.8.

For $K=T.\\#.{\overline{T}}^{\mathit{rev}}$, we prove that we have
$K\in\mathit{L}(\text{WSTS})$, $K\not\in\mathit{L}(\text{detWSTS})$, and
$K\not\in\mathit{L}(\text{detDWSTS})$.

######  Proof C.4 (Proof of Lemma 5.8).

Since ${\overline{T}}^{\mathit{rev}},T\in\mathit{L}(\text{WSTS})$, and
$\mathit{L}(\text{WSTS})$ is closed under concatenation [24, Theorem 2], we
get $T.\\#.{\overline{T}}^{\mathit{rev}}\in\mathit{L}(\text{WSTS})$. We only
show that $K\not\in\mathit{L}(\text{detWSTS})$, as the proof of
${K}^{\mathit{rev}}\not\in\mathit{L}(\text{detDWSTS})$ is similar. Suppose
that $K\in\mathit{L}(\text{detWSTS})$. Then, there is a detWSTS
$\mathit{U}=(Q,\leq,y,\Sigma,\delta,F)$ with $\mathit{L}(\mathit{U})=K$. Let
$v\in{\overline{T}}^{\mathit{rev}}$. This is guaranteed to exist, since $T$ is
neither empty nor universal, per $T\not\in\mathit{L}(\text{detWSTS})$. Let
$\mathit{U}^{\prime}=(Q,\leq,y,\Sigma,\delta,G)$ with $G=\\{p\in
Q\mid\delta(p,\\#.v)\in F\\}$. We claim that $\mathit{U}^{\prime}$ is a
detWSTS with $\mathit{L}(\mathit{U}^{\prime})=T$, which contradicts
Proposition 4.8. First we show that $\mathit{U}^{\prime}$ is indeed a detWSTS.
Since we only modified the final states, we only need to verify that $G$ is
upward-closed. Let $p\in G$ and $p\leq q$. By the definition of $G$, we get
$\delta(p,\\#.v)\in F$. By standard induction on word length, the simulation
property delivers $\delta(q,\\#.v)\geq\delta(p,\\#.v)$. Since $F$ is upward-
closed and $\delta(p,\\#.v)\in F$, we have $\delta(q,\\#.v)\in F$ and thus
$q\in G$.

Now we show $\mathit{L}(\mathit{U}^{\prime})=T$. To see
$\mathit{L}(T)\subseteq\mathit{L}(\mathit{U}^{\prime})$, let $w\in T$. Then,
$\delta(y,w.\\#.v)\in F$ since $w.\\#.v\in K$. We have
$\delta(y,w.\\#.v)=\delta(\delta(y,w),\\#v)\in F$, so $\delta(y,w)\in G$. So
$w\in\mathit{L}(\mathit{U}^{\prime})$. To see
$\mathit{L}(\mathit{U}^{\prime})\subseteq T$, let
$w\in\mathit{L}(\mathit{U}^{\prime})$. Then $\delta(y,w)\in G$. This implies
$\delta(\delta(y,w),\\#.v)=\delta(y,w.\\#.v)\in F$. Then $w.\\#.v\in K$.
Neither words in $T$, nor words in ${\overline{T}}^{\mathit{rev}}$ contain
$\\#$. This is because $\overline{T}$ refers to the complement of $T$ with
respect to $(\Sigma\setminus\\{\\#\\})^{*}$. Therefore, words in $K$ contain
exactly one $\\#$. So, for $w.\\#.v\in K$ to hold, $w\in T$ and
$v\in{\overline{T}}^{\mathit{rev}}$ must also hold. This concludes the proof.