# On the Separability Problem of VASS Reachability Languages

Eren Keskin  TU Braunschweig<EMAIL_ADDRESS>and  Roland Meyer  TU
Braunschweig<EMAIL_ADDRESS>
###### Abstract.

We show that the regular separability problem of VASS reachability languages
is decidable and $\mathbb{F}_{\omega}$-complete. At the heart of our decision
procedure are doubly-marked graph transition sequences, a new proof object
that tracks a suitable product of the VASS we wish to separate. We give a
decomposition algorithm for DMGTS that not only achieves perfectness as known
from MGTS, but also a new property called faithfulness. Faithfulness allows us
to construct, from a regular separator for the $\mathbb{Z}$-versions of the
VASS, a regular separator for the $\mathbb{N}$-versions. Behind faithfulness
is the insight that, for separability, it is sufficient to track the counters
of one VASS modulo a large number that is determined by the decomposition.

##  1\. Introduction

Regular separability problems for the languages of infinite-state systems are
recently gaining momentum [16, 3, 7, 4, 8, 5, 10, 1, 14, 15]. These problems
take as input two infinite-state systems with languages $L_{1}$ and $L_{2}$,
and ask whether $L_{1}\mid L_{2}$ holds, whether there is a regular language
$R$ that separates the two in the sense that $L_{1}\subseteq R$ and $R\cap
L_{2}=\emptyset$. What makes regular separability problems interesting is that
they do not seem to admit a reduction to established problems like emptiness.
Instead, the decision procedure has to analyze the gap between $L_{1}$ and
$L_{2}$, and judge whether it is large enough to be described by a regular
language.

Despite this challenge, there is a pleasant number of positive results on
regular separability. It has been shown that disjoint WSTS languages are
always separated by a regular language [8, 14]. For disjoint VASS coverability
languages, matching upper and lower bounds on the size of least separators
have been found [15]. For Parikh automata [3] and Büchi VASS coverability
languages [1], regular separability has been shown to be decidable.

Unfortunately, for the main model in this field, namely VASS reachability
languages, the search has only brought partial results. This includes the
decidability of the regular separability problem for the reachability
languages of one-dimensional VASS [7], for $\mathbb{Z}$-VASS reachability
languages [3], for the commutative closure of VASS reachability languages [4],
and for VASS reachability languages from any of the aforementioned classes
[10]. The study has also led to important new techniques. With the transducer
trick, one can reduce the regular separability problem to a variant where only
one language is taken as input and the second is fixed [3, 10]. For this
variant, the basic separator approach tries to determine a limited set of
regular languages so that, if separability holds, then a finite combination of
these languages will serve as a separator [10]. The techniques turned out
widely applicable [10, 15, 1], and the transducer trick will also play a
central role in our work. Related to regular separability is the separability
of VASS reachability sets [4]. A landmark result in this context shows that
VASS reachability sets admit Presburger-definable invariants [20], which
resulted in a new algorithm for solving VASS reachability [21]. To sum up,
despite more than a decade of efforts, the decidability of regular
separability for VASS reachability languages is still open.

We solve the open problem and show that regular separability for VASS
reachability languages is decidable and $\mathbf{F}_{\omega}$-complete. The
problem is primitive recursive if the dimension of the input VASS is fixed.
The class $\mathbf{F}_{\omega}$ contains the problems that can be solved with
Ackermannian time and space [28, 29], and the master problem is VASS
reachability. The hardness of VASS reachability has been established only
recently [22, 9, 19]. The decidability is a classic result [25, 17, 18], with
[27] an early attempt, and based on the algorithms proposed in these works,
the upper bound has been brought down from $\mathbf{F}_{\omega^{3}}$ [23] over
$\mathbf{F}_{\omega^{2}}$ [29] to $\mathbf{F}_{\omega}$ [24]. The algorithms
reduce the VASS reachability problem to the reachability problem in
$\mathbb{Z}$-VASS, using an iterative decomposition that creates potentially
many and potentially large $\mathbb{Z}$-VASS. We will follow the same
strategy, and reduce the regular separability problem of VASS reachability
languages to the regular separability problem of $\mathbb{Z}$-VASS
reachability languages, also with a decomposition. The latter problem has been
shown to be decidable in [3]. For the precise upper bound, we rely on an
analysis inspired by [24].

While this is the overall strategy, it takes new ingredients to make it work
that go beyond the toolkit of VASS reachability. To explain them, we refer to
the input as the subject VASS. The second is the Dyck VASS, and can be fixed
with the transducer trick [3, 10].

#### Ingredients

We define doubly-marked graph transition sequences as a new proof object. A
DMGTS $\mathcal{W}$ simultaneously track both, the subject VASS and the Dyck
VASS, like a product construction would. Unlike a product, however, a DMGTS
defines two languages $L_{\mathsf{sj}}(\mathcal{W})$ and
$L_{\mathsf{dy}}(\mathcal{W})$, and the goal is to understand the separability
of the two. To this end, we define a decomposition algorithm for DMGTS that is
inspired by Lambert’s decomposition [18]. What is new is that our
decomposition not only computes one set of perfect DMGTS, but also another set
of DMGTS for which separability is guaranteed to hold. The idea is that our
decomposition does not treat the languages as symmetric, but only tries to
preserve the subject language. If now, as the result of a decomposition step,
the Dyck language becomes empty, then separability will hold and there is no
need to decompose further.

DMGTS have a new property called faithfulness. Faithfulness says that it is
sufficient to track the Dyck language modulo a large number that is determined
in the course of the decomposition. To explain what it means to be sufficient,
note that DMGTS define acceptance not only by reaching a final counter
valuation from an initial one, but require the run to also reach intermediate
valuations. Faithfulness says that if we can reach these intermediate
valuations modulo a large number, then we can reach them precisely. Unlike
perfectness, faithfulness is not established by the decomposition, but it is
preserved as an invariant. The idea why faithfulness holds is this. The
decomposition only introduces intermediate valuations if a counter variable is
bounded. If we then track the counter modulo this bound, then we do not lose
information. For this argument to hold, it is crucial that the input DMGTS is
already faithful.

When the decomposition terminates, it returns a finite set of faithful and
perfect DMGTS (and the second set discussed above). The last ingredient is a
separability transfer result: if the DMGTS $\mathcal{W}$ is faithful, then
$L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})\mid
L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$ implies
$L_{\mathsf{sj}}(\mathcal{W})\mid L_{\mathsf{dy}}(\mathcal{W})$; if it is
perfect, the reverse holds. Behind the first implication is a result that
shows how to turn every separator for the $\mathbb{Z}$-approximations of the
languages into a separator for the languages of interest. Faithfulness is
crucial here. It tells us to intersect the given separator with a regular
language that tracks the Dyck counters modulo the large number determined by
the decomposition. The second implication says that if the
$\mathbb{Z}$-approximations are not separable, then this carries over to the
original languages. Behind this is an application of Lambert’s pumping lemma
[18], and the fact that both languages share the same DMGTS.

#### Overview

After an introduction to VASS, reachability languages, and regular
separability, we discuss Lambert’s decision procedure for VASS reachability in
Section 4. It contains a number of concepts that we build on, including MGTS,
characteristic equations, and perfectness. DMGTS and faithfulness are defined
in Section 5. Our decision procedure for regular separability is given in
Section 6. In Section 7, we prove the separability transfer result. The DMGTS
decomposition can be found in Section 8. Details missing in the main text can
be found in the appendix.

##  2\. VASS

A vector addition system with states $\mathcal{U}=(V,\Sigma,I,E)$ consists of
a finite set of nodes $V$, a finite alphabet $\Sigma$, a finite set of
counters $I$, and a finite set of edges $E\subseteq V\times\mathit{Up}\times
V$. We call $\mathit{Up}=\Sigma_{\varepsilon}\times\mathbb{Z}^{I}$ with
$\Sigma_{\varepsilon}=\Sigma\cup\\{\varepsilon\\}$ the set of updates.

We introduce some notation. For sequences $\sigma\in A^{*}$ over a set $A$, we
use $|{\sigma}|$ for the length and $\sigma[i]$ for the $i$-th component. We
use the distinguished indices $\mathsf{first}$ and $\mathsf{last}$ to access
the first resp. last component. When we have a function
$f:A\rightarrow\mathbb{P}(X)$ into a powerset and $B\subseteq A$, we may use
$f(B)$ for $\bigcup_{b\in B}f(b)$.

We will not only work with VASS but also with $\mathbb{Z}$-VASS. To define the
semantics of both models in one go, let $J\subseteq I$ be a subset of the
counters. A $J$-counter valuation
$c\in\mathbb{N}^{J}\times\mathbb{Z}^{I\setminus J}$ gives a non-negative value
to the $J$-counters. A $J$-configuration is a pair $(v,c)$ consisting of a
node $v\in V$ and a $J$-counter valuation $c$. A $J$-run is a sequence
$\rho=(v_{0},c_{0})e_{0}(v_{1},c_{1})\ldots(v_{l},c_{l})$ of
$J$-configurations and edges where for all $i<l$ we have
$e_{i}=(v_{i},a_{i},x_{i},v_{i+1})$ with $x_{i}=c_{i+1}-c_{i}$. We write
$\mathsf{Runs}_{J}(\mathcal{U})$ for the set of all $J$-runs in $\mathcal{U}$.
We also use $\mathsf{Runs}_{\mathbb{N}}(\mathcal{U})$ if $J$ contains all
counters, and $\mathsf{Runs}_{\mathbb{Z}}(\mathcal{U})$ if $J$ is empty. Note
that the configurations in a run are already determined by the initial counter
valuation and the sequence of edges. We may therefore also give a run as
$\rho=c.\sigma$ with $\sigma\in E^{*}$. We may also emphasize the initial and
final configurations and give a run as
$\rho=(v,c).\sigma.(v^{\prime},c^{\prime})$. We use
$\lambda(\rho)\in\Sigma^{*}$ for the sequence of letters on the run. Two runs
are equivalent, $\rho_{1}\approx\rho_{2}$, if they only differ in the nodes
they visit. We use $\Delta(e)\in\mathbb{Z}^{I}$ for the counter update done by
an edge, and $\Delta(\rho)$ for the counter update done by a run. A Parikh
vector $\psi\in\mathbb{N}^{E}$ associates with each edge an occurrence count,
and we define $\Delta(\psi)=\sum_{e\in E}\psi[e]\cdot\Delta(e)$. Note that
$\Delta(\rho)=\Delta(\psi(\rho))$, where $\psi(\rho)$ is the Parikh vector
induced by $\rho$.

We define accepting runs with generalized initial and final configurations.
Let $\mathbb{N}_{\omega}=\mathbb{N}\cup\\{\omega\\}$ and
$\mathbb{Z}_{\omega}=\mathbb{Z}\cup\\{\omega\\}$ extend the natural numbers
and the integers by a top element. We lift this to counter valuations and call
$c\in\mathbb{N}_{\omega}^{J}\times\mathbb{Z}_{\omega}^{I\setminus J}$ a
generalized $J$-counter valuation. We write $\Omega(c)$ for the set of
counters $i$ with $c(i)=\omega$. We call $(v_{,}c)$ a generalized
$J$-configuration if $c$ is a generalized $J$-counter valuation. We define
acceptance parametric in a preorder $\sqsubseteq\
\subseteq\mathbb{Z}_{\omega}\times\mathbb{Z}_{\omega}$. We lift the preorder
to generalized counter valuations by a componentwise comparison. We also lift
it to generalized configurations by $(v_{1},c_{1})\sqsubseteq(v_{2},c_{2})$,
if $v_{1}=v_{2}$ and $c_{1}\sqsubseteq c_{2}$. An important instance is the
specialization preorder $\leq_{\omega}\
\subseteq\mathbb{Z}_{\omega}\times\mathbb{Z}_{\omega}$, which is defined by
$k\leq_{\omega}k$ and $k\leq_{\omega}\omega$ for all
$k\in\mathbb{Z}_{\omega}$.

An initalized VASS
$\mathcal{V}=(\mathcal{U},(v_{\mathsf{in}},c_{\mathsf{in}}),(v_{\mathsf{out}},c_{\mathsf{out}}))$
enriches a VASS $\mathcal{U}$ with generalized $\mathbb{N}$-configurations
$(v_{\mathsf{in}},c_{\mathsf{in}})$ and $(v_{\mathsf{out}},c_{\mathsf{out}})$
that we call initial and final. We speak of an extremal configuration if it is
initial or final. The runs of $\mathcal{V}$ are the runs of $\mathcal{U}$.
Such a run is $\sqsubseteq$-accepting, if
$\rho[\mathsf{first}]\sqsubseteq(v_{\mathsf{in}},c_{\mathsf{in}})$ and
$\rho[\mathsf{last}]\sqsubseteq(v_{\mathsf{out}},c_{\mathsf{out}})$, the first
configuration is smaller than the initial configuration in the given preorder,
and the last configuration is smaller than the final configuration. We use
$\mathsf{Acc}_{J,\sqsubseteq}(\mathcal{V})$ for the set of all $J$-runs in
$\mathcal{V}$ that are $\sqsubseteq$-accepting. We denote the size of an
initialized VASS by $|{\mathcal{V}}|$. We measure the size in binary, but this
does not matter for the large complexity classes we are concerned with.

With an initialized VASS, we associate the language of all words that label an
$\leq_{\omega}$-accepting run:

$\displaystyle
L_{J}(\mathcal{V})\;\;=\;\;\\{\lambda(\rho)\mid\rho\in\mathsf{Acc}_{J,\leq_{\omega}}(\mathcal{V})\\}\
.$

We use $L_{\mathbb{N}}(\mathcal{V})$ and $L_{\mathbb{Z}}(\mathcal{V})$ if
every counter resp. no counter has to stay non-negative. The former are the
VASS reachability languages and the latter the $\mathbb{Z}$-VASS reachability
languages.

##  3\. Regular Separability

We study the regular separability of VASS reachability languages. Languages
$L_{1},L_{2}\subseteq\Sigma^{*}$ are _separable by a regular language_ ,
denoted by $L_{1}\mid L_{2}$, if there is a regular language
$S\subseteq\Sigma^{*}$ that satisfies $L_{1}\subseteq S$ and $S\cap
L_{2}=\emptyset$. The language $S$ is usually called the separator, and the
regular separability problem asks whether a separator exists for given
languages. In the definition of the decision problem, we again make the domain
of counter values a parameter:

> $\mathbb{X}$-REGSEP
> Given: Initialized VASS $\mathcal{V}_{1}$ and $\mathcal{V}_{2}$ over
> $\Sigma$.
> Problem: Does $L_{\mathbb{X}}(\mathcal{V}_{1})\mid
> L_{\mathbb{X}}(\mathcal{V}_{2})$ hold?

Our main result is the decidability of regular separability for the
reachability languages of ordinary VASS.

###### Theorem 3.1.

$\mathbb{N}$-REGSEP is decidable and $\mathbf{F}_{\omega}$-complete. We can
effectively compute a separator in this time and space bound.

Recall that $\mathbf{F}_{\omega}$ is the class of problems that can be solved
with Ackermannian time and space [28]. It is closed under further calls to
primitive recursive functions [28, Lemma 4.6], and these functions are also
used as reductions to define hardness. Our lower bound for regular
separability is by a reduction from the reachability problem in
$\mathbb{N}$-VASS, whose $\mathbf{F}_{\omega}$-hardness is a recent
achievement [9, 22, 19]. It even holds if we promise the input languages to be
disjoint and the only separator candidate is $\emptyset$. The techniques are
standard and can be found in the appendix.

For the upper bound, we use the transducer trick [3, 10] and reduce
$\mathbb{N}$-REGSEP to a separability problem that only takes one reachability
language as input. The second language is fixed to the Dyck language $D_{n}$,
where $n$ is the number of counters in the second VASS. The Dyck language is
accepted by the initialized VASS
$(\mathcal{D}_{n},(v,\mathbf{0}),(v,\mathbf{0}))$ with
$\mathcal{D}_{n}=(\\{v\\},\Sigma_{n},\mathsf{dy},E)$. The alphabet is
$\Sigma_{n}=\\{a_{i},\bar{a}_{i}\mid 1\leq i\leq n\\}$, the counters
$\mathsf{dy}=\\{1,\ldots,n\\}$, and the edges are
$E=\\{(v,(a_{i},e_{i}),v),(v,(\bar{a}_{i},-e_{i}),v)\mid 1\leq i\leq n\\}$,
where $e_{i}$ is the $i$-th unit vector. This means we increment counter $i$
when seeing $a_{i}$, and decrement $i$ upon $\bar{a}_{i}$. We call a VASS that
sticks with this link between letters and counter updates _Dyck visible_. Note
that the VASS only has one state, and we also speak of a _VAS_.

###### Lemma 3.2.

Let $\mathcal{U}$ and $\mathcal{V}$ be initialized VASS over $\Sigma$, and let
$\mathcal{V}$ have $n$ counters. We can compute in elementary time from
$\mathcal{V}$ a transducer $T$ so that
$\mathit{L}(\mathcal{U})\mid\mathit{L}(\mathcal{V})$ if and only if
$T^{-1}(\mathit{L}(\mathcal{U}))\mid D_{n}$.

VASS are effectively closed under inverse transductions.

###### Lemma 3.3.

Let $\mathcal{U}$ be an initialized VASS over $\Sigma$ and let $T$ be a
transducer from $\Sigma_{n}$ to $\Sigma$. We can compute in time elementary in
the size of $\mathcal{U}$ and $T$ a VASS $\mathcal{U}^{\prime}$ so that
$\mathit{L}(\mathcal{U}^{\prime})=T^{-1}(\mathit{L}(\mathcal{U}))$.

With the aforementioned closure of $\mathbf{F}_{\omega}$ under primitive
recursive functions, Theorem 3.1 is a consequence of the following result.

###### Proposition 3.4.

Let $\mathcal{U}$ be an initialized VASS over $\Sigma_{n}$. Then
$\mathit{L}(\mathcal{U})\mid D_{n}$ is decidable and we can compute a
separator in $\mathbf{F}_{\omega}$.

The rest of the paper is devoted to proving Proposition 3.4. Our algorithm is
based on the decision procedure for VASS reachability, whose details we recall
in a moment. A second ingredient is the decidability of regular separability
for $\mathbb{Z}$-VASS. This is a result we can use in black-box fashion, when
it is formulated as follows.

###### Theorem 3.5 ([3]).

$\mathbb{Z}$-REGSEP is decidable and a regular separator can be computed with
elementary resources.

##  4\. VASS Reachability

We recall Lambert’s decision procedure for VASS reachability [18], with the
recent additions due to Leroux and Schmitz [24]. The purpose is to introduce
concepts that we need later.

###  4.1. Overview

The VASS reachability problem takes as input an initialized VASS $\mathcal{V}$
and asks whether
$\mathsf{Acc}_{\mathbb{N},\leq_{\omega}}(\mathcal{V})\neq\emptyset$. The
decision procedure is an abstraction-refinement algorithm that computes a
sequence

$\displaystyle\mathsf{Acc}_{\mathbb{Z},\leq_{\omega}}(S_{0})\supseteq\mathsf{Acc}_{\mathbb{Z},\leq_{\omega}}(S_{1})\supseteq\ldots\supseteq\mathsf{Acc}_{\mathbb{N},\leq_{\omega}}(\mathcal{V})\
.$

Each over-approximation $S_{i}$ is a finite set of $\mathbb{Z}$-VASS
$\mathcal{W}$ and, as agreed, we use
$\mathsf{Acc}_{\mathbb{Z},\leq_{\omega}}(S_{i})$ for $\bigcup_{\mathcal{W}\in
S_{i}}\mathsf{Acc}_{\mathbb{Z},\leq_{\omega}}(\mathcal{W})$. Details on the
shape of $\mathcal{W}$ will follow in a moment.

At each step, the algorithm picks an element $\mathcal{W}\in S_{i}$ and checks
reachability. If reachability does not hold,
$\mathsf{Acc}_{\mathbb{Z},\leq_{\omega}}(\mathcal{W})=\emptyset$, then the
element will not be considered in the future,
$S_{i+1}=S_{i}\setminus\\{\mathcal{W}\\}$. If reachability holds, the
algorithm checks whether $\mathcal{W}$ is perfect, a property that we discuss
below. If so, the algorithm concludes that the $\mathbb{Z}$-run it has just
found can be turned into an $\mathbb{N}$-run, and terminates with the verdict
_reachable_. If $\mathcal{W}$ is not perfect, there is a guarantee that
$\mathcal{W}$ can be refined. Following Leroux and Schmitz [23], the
refinement is called KLMST decomposition after the inventors Kosaraju [17],
Lambert [18], Mayr [25], as well as Sacerdote and Tenney [27]. The
decomposition computes from $\mathcal{W}$ a new and again finite set
$S(\mathcal{W})$ of $\mathbb{Z}$-VASS that replace $\mathcal{W}$ in the
approximation, meaning we have $S_{i+1}=(S_{i}\setminus\\{\mathcal{W}\\})\cup
S(\mathcal{W})$. The decomposition guarantees
$\mathsf{Acc}_{\mathbb{N},\leq_{\omega}}(\mathcal{W})=\mathsf{Acc}_{\mathbb{N},\leq_{\omega}}(S(\mathcal{W}))$
so that we do not lose $\mathbb{N}$-runs but remain over-approximate. If
$S_{i}$ is found to be empty, the algorithm terminates with the verdict
_unreachable_.

What makes the algorithm terminate is a progress guarantee: each
$\mathbb{Z}$-VASS in the KLMST decomposition $S(\mathcal{W})$ is guaranteed to
be strictly smaller than $\mathcal{W}$ in a well-founded order. Since
$S(\mathcal{W})$ is finite, König’s lemma shows termination of the overall
algorithm.

We elaborate on the $\mathbb{Z}$-VASS used in the over-approximation. There
are two standard techniques to over-approximate reachability in VASS:
characteristic equations [6, 12] and coverablity graphs [13]. The
characteristic equations can track counter values precisely, but they cannot
guarantee that intermediate values remain non-negative. Coverability graphs
are the opposite, they can guarantee that intermediate values remain non-
negative, but they cannot track counter values precisely. The decision
procedure combines the two. The $\mathbb{Z}$-VASS are decorated by generalized
$\mathbb{N}$-counter valuations, like coverability graphs. If a decoration is
$\omega$, and thus not precise enough for reachability, that counter is
treated as a $\mathbb{Z}$-counter and handled by the characteristic equations.

For this combination to solve reachability, we have to be able to transfer the
non-negativity guarantee given by coverability graphs to the characteristic
equations. Behind the non-negativity guarantee given by coverability graphs is
a translation: if we have a run in the coverability graph, we obtain an
$\mathbb{N}$-run in the underlying VASS by repeating intermediate transition
sequences in order to pump counter values arbitrarily high. By transferring
the guarantee, we mean that also the characteristic equations should admit
this pumping behavior: the counter as well as the repetition count for the
edges on the pumping sequences should be unbounded in the solution space of
the characteristic equations. If this is the case, the coverability graph is
called perfect.

It is easy to check unboundedness in the solution space, and therefore also
perfectness: we just have to find a solution to the homogeneous variant of the
characteristic equations where the variable is positive. More precisely, the
characteristic equations will have the shape $Ax=b\wedge x\geq 0$. The
solutions $s$ can have arbitrarily high values $s[i]$ if and only if
$Ay=0\wedge y\geq 0$ has a solution $s^{\prime}$ with $s^{\prime}[i]>0$. To
see that homogeneous solutions are necessary, assume there are solutions with
arbitrarily high values for a variable. The well-quasi order of
$\mathbb{N}^{k}$ will give us comparable solutions that we can subtract to
solve the homogenous equations.

The KLMST decomposition comes in when perfectness fails, but the
$\omega$-decorations and pumping sequences do not coincide with the
unboundedness in the solution space. For example, the decoration may suggest
the counter value $\omega$, but the counter is bounded in the solution space.
Then the counter can only take finitely many values in runs that solve
reachability. The decomposition now replaces the $\omega$-entry by each of
these values. The result is a potentially large but finite set of new
$\mathbb{Z}$-VASS. The analysis also informs us about transitions that can
only be taken a bounded number of times in the solution space, but that lie on
loops in the coverability graph. To improve the precision, one unwinds the
coverability graph so that the bounded transitions lie on an acyclic path.
This is the second form of decomposition. The last decomposition has to do
with the fact that we need pumping sequences that justify the existence of the
$\omega$-entries. We make the ideas formal.

###  4.2. MGTS

The $\mathbb{Z}$-VASS used for the over-approximation are so-called _marked
graph transition sequences (MGTS)_ that are defined as follows:

$\displaystyle\mathcal{W}\;\;::=\;\;G\;\;\mid\;\;\mathcal{W}_{1}.\mathit{up}.\mathcal{W}_{2}\
.$

An MGTS is an interleaving of precovering graphs $G$ and updates
$\mathit{up}$. Precovering graphs are initialized VASS of a form we define in
a moment. In an MGTS, all precovering graphs share the same alphabet and the
same set of counters $I$, but the sets of nodes are pairwise disjoint.

A _precovering graph_ $G=(\mathcal{V},\varphi)$ is an initialized VASS
$\mathcal{V}$ that is decorated by a consistent assignment $\varphi$. The VASS
should be strongly connected and satisfy
$\mathcal{V}.v_{\mathsf{in}}=\mathcal{V}.v_{\mathsf{out}}$, called the root of
$G$ and denoted by $v_{\mathsf{root}}$. Let $V=\mathcal{V}.V$ be the nodes,
$E=\mathcal{V}.E$ the edges, and $I=\mathcal{V}.I$ the counters in
$\mathcal{V}$. An assignment $\varphi:V\to\mathbb{N}_{\omega}^{I}$ of
generalized counter valuations to nodes is _consistent_ , if there is a set of
counters $J\subseteq I$ so that for all nodes $v\in V$ we have
$\varphi(v)[j]\in\mathbb{N}$ if and only if $j\in J$, we have
$\varphi(v_{\mathsf{root}})[J]=c_{\mathsf{in}}[J]=c_{\mathsf{out}}[J]$, and
$\Delta(\mathit{up})[J]=\varphi(w)[J]-\varphi(v)[J]$ for all
$(v,\mathit{up},w)\in E$. The consistent assignment is the decoration from
above. Consistency means all nodes agree on the set of counters $J$ that are
decorated by $\mathbb{N}$-values. The remaining counters are decorated by
$\omega$ and we use $\Omega(G)=I\setminus J$ to refer to them. For the
counters in $J$, the decoration of the root has to coincide with the initial
and the final valuations. This means the initial and final valuations may only
have less $\omega$-entries. The decoration tracks the updates performed by the
edges.

A counter $i$ may be decorated by $\omega$ in the precovering graph but have a
concrete initial value, $i\in\Omega$ with
$\Omega=\Omega(G)\setminus\Omega(c_{\mathsf{in}})$. Then it should be possible
to pump this counter in the precovering graph to arbitrarily high values while
going from the root back to the root. Pumping means the loop starts in a
counter valuation $c_{1}$ that respects the concrete initial values and ends
in a valuation $c_{2}$ that is strictly larger in the counters from $\Omega$.
For the counters in $\Omega(c_{\mathsf{in}})$, there is no requirement and the
loop may reduce their values. The remaining counters are tracked by the
decoration and every loop will leave their valuation unchanged. We use
$c_{1}<^{\Omega}c_{2}$ for $c_{1}(i)<c_{2}(i)$ for all $i\in\Omega$. That
pumping should be possible means the following set of _covering sequences_
should be non-empty:

$\displaystyle\mathsf{CS}_{\mathsf{up}}(G)=\;\\{\sigma\in$ $\displaystyle\
E^{*}\mid\exists
c_{1},c_{2}\in\mathbb{N}^{I}.c_{1}\leq_{\omega}c_{\mathsf{in}}\wedge
c_{1}<^{\Omega}c_{2}$
$\displaystyle\qquad\wedge(v_{\mathsf{root}},c_{1}).\sigma.(v_{\mathsf{root}},c_{2})\in\mathsf{Runs}_{\mathbb{N}}(G)\\}\
.$

We also need to pump down counters $i$ that are decorated $\omega$ in the
precovering graph but receive a concrete value in the final configuration,
$i\in\Omega$ with $\Omega=\Omega(G)\setminus\Omega(c_{\mathsf{out}})$. We
reuse the above definition and define

$\displaystyle\mathsf{CS}_{\mathsf{down}}(G)\;\;=\;\;{\mathsf{CS}_{\mathsf{up}}({G}^{\mathit{rev}})}^{\mathit{rev}}\
.$

The reverse of a run is defined as expected,
${(\rho_{1}.\rho_{2})}^{\mathit{rev}}={\rho_{2}}^{\mathit{rev}}.{\rho_{1}}^{\mathit{rev}}$.
The reverse of a single edge is ${(v,a,x,w)}^{\mathit{rev}}=(w,a,-x,v)$,
meaning we increment where we have decremented before, and vice versa. The
reverse runs stem from a reversal of the precovering graph,
${G}^{\mathit{rev}}=(({\mathcal{U}}^{\mathit{rev}},(v_{\mathsf{root}},c_{\mathsf{out}}),(v_{\mathsf{root}},c_{\mathsf{in}})),\varphi)$.
Note that the initial and final configurations have changed their roles. The
reversal of the underlying counter system
${\mathcal{U}}^{\mathit{rev}}=(V,\Sigma,I,\\{{e}^{\mathit{rev}}\mid e\in
E\\})$ simply reverses the edges. Hence, the two reversals in the definition
have no effect on the counter updates but just identify the down-pumping runs
that end in $c_{\mathsf{out}}$ from arbitrarily high values in the
$\Omega$-counters.

The emptiness of $\mathsf{CS}_{\mathsf{up}}(G)$ and
$\mathsf{CS}_{\mathsf{down}}(G)$ can be checked using (two different)
unboundedness checks [13, 11], which will also provide covering sequences if
the sets are non-empty.

In our development, it will be helpful to understand MGTS $\mathcal{W}$ as
initalized VASS. We simply turn the intermediate updates into edges that
connect the final node in one precovering graph with the initial node of the
next. We write $\mathcal{W}.V$ for the set of all nodes in precovering graphs
of $\mathcal{W}$, and similar for the alphabet, the counters, and the edges.
We write $\mathcal{W}.v_{\mathsf{in}}$ for
$\mathcal{W}[\mathsf{first}].v_{\mathsf{in}}$, and
$\mathcal{W}.v_{\mathsf{out}}$ for
$\mathcal{W}[\mathsf{last}].v_{\mathsf{out}}$. We use $|{\mathcal{W}}|$ for
the size. The initial and final configurations of each precovering graph count
towards the size.

Seeing MGTS as VASS, we can use $\mathsf{Acc}_{J,\sqsubseteq}(\mathcal{W})$ to
refer to the accepting runs. MGTS also have their own notion of _intermediate
acceptance_ , where the runs not only have to meet the overall initial and
final configurations, but the initial and final configurations of every
precovering graph. Since we transition through a sequence of precovering
graphs, we also speak of entry and exit rather than initial and final
configurations. We say that a $J$-run $\rho\in\mathsf{Runs}_{J}(\mathcal{W})$
is $\sqsubseteq$-intermediate accepting, if for every precovering graph $G$ in
$\mathcal{W}$ that is traversed by the infix $\rho_{G}$ of $\rho$, we have
$\rho_{G}[\mathsf{first}]\sqsubseteq(v_{\mathsf{root}},c_{\mathsf{in}})$ and
$\rho_{G}[\mathsf{last}]\sqsubseteq(v_{\mathsf{root}},c_{\mathsf{out}})$.
Here, $(v_{\mathsf{root}},c_{\mathsf{in}})$ and
$(v_{\mathsf{root}},c_{\mathsf{out}})$ are the entry and exit configurations
of $G$. We use $\mathsf{IAcc}_{J,\sqsubseteq}(\mathcal{W})$ for the set of all
$\sqsubseteq$-intermediate accepting $J$-runs in $\mathcal{W}$.

###  4.3. Characteristic Equations

The characteristic equations for MGTS are

$\displaystyle\mathsf{Char}(G)$
$\displaystyle\;\;=\;\;\mathsf{RunsEq}(G)\wedge\mathsf{IAccEq}(G,\leq_{\omega})$
$\displaystyle\mathsf{Char}(G.\mathit{up}.\mathcal{W})$
$\displaystyle\;\;=\;\;\mathsf{Char}(G)\wedge\mathsf{Char}(\mathcal{W})$
$\displaystyle\hskip 19.91684pt\wedge
x[G,\mathsf{out}]+\Delta(\mathit{up})-x[\mathcal{W}[\mathsf{first}],\mathsf{in}]=\mathbf{0}\
.$

For each precovering graph $G$ and each counter $i$ in the MGTS, we introduce
the variables $x[G,\mathsf{in},i]$ and $x[G,\mathsf{out},i]$. The idea is that
the vectors
$x[G,\mathsf{in}]=(x[G,\mathsf{in},1],\ldots,x[G,\mathsf{in},|{I}|])$ and
$x[G,\mathsf{out}]$ describe the counter valuations upon entering respectively
exiting the precovering graph. The last system of equations says that the
counter valuation when entering the first precovering graph in $\mathcal{W}$
is the valuation when leaving $G$ plus the counter update
$\Delta(\mathit{up})$. We also have a variable $x[e]$ for every edge in a
precovering graph, which counts how often the edge is taken in a run.

The system of equations $\mathsf{RunsEq}(G)$ captures the runs through the
precovering graph $G$. It consists of the Kirchhoff equations, the marking
equations, and equations that require non-negative values for the edge
variables. The Kirchhoff equations express the fact that a run must enter and
exit every node the same number of times. Since precovering graphs are
strongly connected, this means the edge vector can be turned into a path
provided every single edge is taken at least once. Perfectness will make sure
this is the case. The marking equations say that the counter valuation after
the run is the initial counter valuation plus the updates performed by the
edges. The reader may note that we would only have to track the values for
counters in $\Omega(G)$, but this would clutter the presentation. Let $V=G.V$,
$E=G.E$, and $E^{\mathsf{to}}(v)$ and $E^{\mathsf{from}}(v)$ denote the edges
leading to and originating from node $v$. We have

$\mathsf{RunsEq}(G)$: $\displaystyle\sum_{e\in
E^{\mathsf{to}}(v)}x[e]-\sum_{e\in E^{\mathsf{from}}(v)}x[e]$
$\displaystyle=0\quad\text{for all }v\in V$ $\displaystyle
x[G,\mathsf{in}]+\Delta(x[E])-x[G,\mathsf{out}]$ $\displaystyle=\mathbf{0}$
$\displaystyle x[e]$ $\displaystyle\geq 0\quad\text{for all }e\in E\ .$

The system $\mathsf{IAccEq}(G,\sqsubseteq)$ formulates
$\sqsubseteq$-intermediate acceptance. It says that the initial counter
valuation held by $x[G,\mathsf{in}]$ should be smaller than the initial
counter valuation $G.c_{\mathsf{in}}$ wrt. $\sqsubseteq$, and the final
counter valuation $x[G,\mathsf{out}]$ should be smaller than
$G.c_{\mathsf{out}}$. Moreover, both valuations should be non-negative. We
define

$\mathsf{IAccEq}(G,\sqsubseteq)$: $\displaystyle\mathbf{0}\leq
x[G,\mathsf{in}]$ $\displaystyle\sqsubseteq G.c_{\mathsf{in}}$
$\displaystyle\mathbf{0}\leq x[G,\mathsf{out}]$ $\displaystyle\sqsubseteq
G.c_{\mathsf{out}}\ .$

As explained above, to judge whether a variable is unbounded in the solution
space of $\mathsf{Char}(\mathcal{W})$, we need a homogeneous variant of the
characteristic equations. Since most equations are already homogeneous, all we
have to do is replace the concrete values in $\mathsf{IAccEq}(G,\sqsubseteq)$
by zero. We thus define $\mathbf{0}_{\mathsf{in}}\in\\{0,\omega\\}^{I}$ by
$\mathbf{0}_{\mathsf{in}}[i]=\omega$ if and only if
$c_{\mathsf{in}}[i]=\omega$ for all $i\in I$, and similar for
$\mathbf{0}_{\mathsf{out}}$. With this,

$\mathsf{HomIAccEq}(G,\sqsubseteq)$: $\displaystyle\mathbf{0}\leq
x[G,\mathsf{in}]$ $\displaystyle\sqsubseteq\mathbf{0}_{\mathsf{in}}$
$\displaystyle\mathbf{0}\leq x[G,\mathsf{out}]$
$\displaystyle\sqsubseteq\mathbf{0}_{\mathsf{out}}\ .$

A support solution of $\mathsf{Char}(\mathcal{W})$ is a vector
$s\in\mathbb{Z}^{\mathcal{W}}$ that satisfies the homogeneous characteristic
equations. The support $\mathsf{supp}(\mathsf{Char}(\mathcal{W}))$ consists of
all (counter and edge) variables $x[c]$ for which there is a support solution
$s$ with $s[c]\geq 1$. We call $s$ a full support solution, if it gives a
positive value to all variables in the support, $s[c]\geq 1$ for all
$x[c]\in\mathsf{supp}(\mathsf{Char}(\mathcal{W}))$. Since support solutions
are stable under addition, we have the following result.

###### Lemma 4.1.

There always is a full support solution of $\mathsf{Char}(\mathcal{W})$.

###  4.4. Perfectness and Reachability

When it comes to reachability, an $\leq_{\omega}$-intermediate accepting
$\mathbb{N}$-run in an MGTS $\mathcal{W}$ immediately yields a solution of the
characteristic equations $\mathsf{Char}(\mathcal{W})$. Lambert’s important
insight is that also the reverse holds [18]: a solution to the characteristic
equations yields an $\leq_{\omega}$-intermediate accepting $\mathbb{N}$-run.
What is remarkable is that the characteristic equations cannot guarantee non-
negativity of the valuations attained within precovering graphs. Instead,
Lambert achieves non-negativity by pumping covering sequences. His result
needs the hypothesis that covering sequences exist and, moreover, the
characteristic equations admit the pumping. This is captured by the notion of
perfectness. The MGTS $\mathcal{W}$ is _perfect_ , if for every precovering
graph $G$ in $\mathcal{W}$,

  * (i)

$\mathsf{CS}_{\mathsf{up}}(G)\neq\emptyset\neq\mathsf{CS}_{\mathsf{down}}(G)$,
and

  * (ii)

$\mathsf{supp}(\mathsf{Char}(\mathcal{W}))$ justifies the unboundedness in
$G$.

It remains to define what it means to justify the unboundedness. We make the
definition slightly more general so that we can reuse it later. Let $G$ have
counters $I$, edges $E$, initial valuation $c_{\mathsf{in}}$, and final
valuation $c_{\mathsf{out}}$. Let $J\subseteq I$ be a subset of the counters.
We say that $\mathsf{supp}(\mathsf{Char}(\mathcal{W}))$ _justifies the
unboundedness of $J$ in $G$_, if

$\displaystyle x[G,\mathsf{in},j]$
$\displaystyle\in\mathsf{supp}(\mathsf{Char}(\mathcal{W}))\text{ for all $j\in
J$ with $c_{\mathsf{in}}[j]=\omega$}$ $\displaystyle x[G,\mathsf{out},j]$
$\displaystyle\in\mathsf{supp}(\mathsf{Char}(\mathcal{W}))\text{ for all $j\in
J$ with $c_{\mathsf{out}}[j]=\omega$}$ $\displaystyle x[e]$
$\displaystyle\in\mathsf{supp}(\mathsf{Char}(\mathcal{W}))\text{ for all $e\in
E$}\ .$

If $J=I$, we say _$\mathsf{supp}(\mathsf{Char}(\mathcal{W}))$ justifies the
unboundedness in $G$_.

Perfectness of $\mathcal{W}$ is sufficient to construct an $\mathbb{N}$-run
from a solution to the characteristic equations:

$\displaystyle\mathsf{IAcc}_{\mathbb{N},\leq_{\omega}}(\mathcal{W})\neq\emptyset\qquad$
$\displaystyle\text{iff}\qquad\mathsf{IAcc}_{\mathbb{Z},\leq_{\omega}}(\mathcal{W})\neq\emptyset$
$\displaystyle\text{iff}\qquad\mathsf{Char}(\mathcal{W})\text{ is feasible}\
.$

The implication from right to left is Lambert’s famous iteration lemma [18,
Lemma 4.1]. As the key arguments will reappear in our solution to regular
separability, we explain them before stating the result. For simplicity,
assume there is only one precovering graph $G$ whose initial and final
valuations are concrete, $c_{\mathsf{in}},c_{\mathsf{out}}\in\mathbb{N}^{I}$.
Let $s_{\mathit{h}}$ be a full support solution that exists by Lemma 4.1. Let
$s_{\mathit{c}}$ be a solution to the characteristic equations that exists by
feasibility. Then $s_{\mathit{h}}+s_{\mathit{c}}=s$ solves the characteristic
equations and satisfies $s[e]\geq 1$ for every edge. As the solution contains
every edge, we can turn it into a path $\rho$ with $\psi(\rho)=s$.
Unfortunately, the path may not be an $\mathbb{N}$-run, because the
$\omega$-decorated counters may become negative. By perfectness, however,
there is a covering sequence $u\in\mathsf{CS}_{\mathsf{up}}(G)$ that produces
a positive value on all $\omega$-decorated counters (recall that the initial
valuation is concrete). The idea is to repeat $u$ to enable $\rho$.

Unfortunately, we cannot repeat $u$ in isolation, otherwise we may end up with
a run that no longer solves reachability. The way out is to work with
repetitions of the support solution. We also have to involve a sequence
$v\in\mathsf{CS}_{\mathsf{down}}(G)$ for reasons that will become clear in a
moment. Select $m\in\mathbb{N}$ so that

(1) $\displaystyle m\cdot s_{\mathit{h}}[E]-\psi(u)-\psi(v)\geq\mathbf{1}\ .$

The condition says that $m$ copies of the support solution contain enough
transitions to fit in $u$, $v$, and another cycle $w$. We can form $w$ because
we still have every edge at least once. The idea is to embed $\rho$ into a
repetition $u^{k}.\rho.w^{k}.v^{k}$. We first have a sequence that increases
the counter values and in the end a sequence that decreases them. Since $u$
and $v$ are $\mathbb{N}$-runs, we know they are executable once we have their
initial valuations.

Unfortunately, we do not even know that $u.w.v$ forms an $\mathbb{N}$-run. The
word $w$ may have a negative effect on the $\omega$-decorated counters. This
is where $v$ comes in. We know that $u.w.v$ has a zero effect on the
$\omega$-decorated counters by the shape of the homogeneous characteristic
equations. Moreover, we know that $v$ has a strictly negative effect on these
counters by the definition of $\mathsf{CS}_{\mathsf{down}}(G)$. Then $u.w$
must have a strictly positive effect on the $\omega$-decorated counters. This
means there is $k\in\mathbb{N}$ so that $u^{k}.w^{k}.v^{k}$ is an
$\mathbb{N}$-run. We can choose $k$ large enough for $u^{k}.\rho.w^{k}.v^{k}$
to form an $\mathbb{N}$-run.

It is also helpful to consider the case where $c_{\mathsf{out}}[i]=\omega\neq
c_{\mathsf{in}}[i]$, meaning the precovering graph has to provide arbitrarily
large values for counter $i$. By perfectness, we know that
$x[G,\mathsf{out},i]$ is in the support. In the above discussion, this means
$u.w.v$ will have a strictly positive effect on this counter.

To lift the argumentation from precovering graphs to composed MGTS, we have to
deal with $\omega$-entries in the initial valuation of a precovering graph. An
$\omega$-entry means the covering sequence may have a negative impact on the
counter. To be able to execute the sequence, we let the precovering graphs
which are placed earlier in the MGTS produce a high enough value on the
counter as follows. By perfectness, the variable for the $\omega$-decorated
counter is in the support. This means we can scale the support solution
$s_{\mathit{h}}$ by a factor $m\in\mathbb{N}$ that not only achieves Condition
(1) from above, but also satisfies the following: for all precovering graphs
$G$ in $\mathcal{W}$ with $\omega$-decorated counter $i$,
$u\in\mathsf{CS}_{\mathsf{up}}(G)$ and $v\in\mathsf{CS}_{\mathsf{down}}(G)$,
we have

(2) $\displaystyle m\cdot s_{\mathit{h}}[G,\mathsf{in},i]+\Delta(u)\geq
1\;\text{and}\;m\cdot s_{\mathit{h}}[G,\mathsf{out},i]-\Delta(v)\geq 1\ .$

The following is a slightly strengthened variant of Lambert’s iteration lemma
that makes explicit the universal quantification over the cycles that can be
iterated. This gives us freedom for our construction in Section 7. Despite the
stronger formulation, the correctness of the lemma still follows from the
proof in [18].

###### Lemma 4.2 (Lambert’s Iteration Lemma, Lemma 4.1 in [18]).

Let $\mathcal{W}$ be a perfect MGTS. For every $G_{i}$ in $\mathcal{W}$, let
$u_{i}\in\mathsf{CS}_{\mathsf{up}}(G_{i})$ and
$v_{i}\in\mathsf{CS}_{\mathsf{down}}(G_{i})$. Let $s_{\mathit{c}}$ solve
$\mathsf{Char}(\mathcal{W})$. We can compute

  * •

a support solution $s_{\mathit{h}}$ satisfying (1) and (2) for every $G_{i}$,

  * •

for every $G_{i}$, cycles $\rho_{i}$ and $w_{i}$ originating in the root,

  * •

so that $s_{\mathit{h}}[E_{i}]=\psi(u_{i})+\psi(w_{i})+\psi(v_{i})$,

  * •

and $s_{\mathit{c}}[E]=\sum_{G_{i}\in\mathcal{W}}\psi(\rho_{i})$.

Moreover, for every $s_{\mathit{c}}$, $s_{\mathit{h}}$, and $(u_{i}$,
$\rho_{i}$, $w_{i}$, $v_{i})_{G_{i}\in\mathcal{W}}$ that satisfy the above
conditions, there is $k_{0}\in\mathbb{N}$ so that for all $k\in\mathbb{N}$
with $k_{0}\leq k$

$\displaystyle
c.u_{0}^{k}\rho_{0}w_{0}^{k}v_{0}^{k}\mathit{up}_{1}\ldots\mathit{up}_{\mathsf{last}}u_{\mathsf{last}}^{k}\rho_{\mathsf{last}}w_{\mathsf{last}}^{k}v_{\mathsf{last}}^{k}$
$\displaystyle\in\mathsf{IAcc}_{\mathbb{N},\leq_{\omega}}(\mathcal{W})\ .$

###  4.5. Decomposition

Our decision procedure for regular separability will modify the KLMST
decomposition. We therefore omit the details here and only discuss the well-
founded relation. To achieve the $\mathbf{F}_{\omega}$ upper bound, we cannot
work with the well-founded relation from [18], but rely on recent ideas from
[24]. We assign each MGTS with $d$ counters a rank in $\mathbb{N}^{d+1}$, and
define the well-founded relation $<_{\mathsf{rnk}}$ to compare the ranks
lexicographically. The rank of an MGTS $\mathcal{W}$ is defined inductively.
For a precovering graph, $\mathsf{rank}(G)$ is a vector with a single non-zero
entry, and this entry holds information about the size of $G$. The entry
itself is related to the dimension of a vector space $\mathsf{V}(G)$ that is
associated with the precovering graph. This is the space spanned by the cycle
effects:

$\displaystyle\mathsf{V}(G)=\mathsf{span}(\\{\Delta(\rho)\mid\rho=(v,c)\ldots(v,c^{\prime})\in\mathsf{Runs}_{\mathbb{Z}}(G)\\})\
.$

Assume $\mathsf{V}(G)$ is $i$-dimensional. We define
$\mathsf{rank}(G)[d-i]=|{G.E}|+|{\Omega(G.c_{\mathsf{in}})}|+|{\Omega(G.\varphi)}|+|{\Omega(G.c_{\mathsf{out}})}|$
and $\mathsf{rank}(G)[j]=0$ for $j\neq d-i$. The inductive case is
$\mathsf{rank}(\mathcal{W}_{1}.\mathit{up}.\mathcal{W}_{2})=\mathsf{rank}(\mathcal{W}_{1})+\mathsf{rank}(\mathcal{W}_{2})$.

The definition allows us to unwind a precovering graph into an MGTS with a
number of precovering graphs. If the cycle spaces of the new precovering
graphs have a smaller dimension, then this makes their non-zero entry in the
rank move to the right. As a consequence, the well-founded order decreases,
even though the new MGTS may have more edges in total.

##  5\. DMGTS

We introduce _doubly-marked graph transition sequences (DMGTS)_ as the data
structure behind our decision procedure for regular separability. Recall that
the goal is to separate the language of a subject VASS from the Dyck language.
The idea of DMGTS is to simultanteously track both languages, very much like
an MGTS for the intersection would. The coupling, however, is not as tight as
in the case of intersection. Instead, the notion of perfectness and the
decomposition focus on the language of the subject VASS, and only consider the
Dyck language as a barrier to which the subject language cannot be extended.

A DMGTS $\mathcal{W}=(\mathcal{S},\mu)$ consists of an MGTS $\mathcal{S}$ and
a natural number $\mu\geq 1$. The counters in $\mathcal{S}$ form a disjoint
union $\mathsf{sj}\uplus\mathsf{dy}$ between the counters $\mathsf{sj}$ in the
subject VASS and the counters $\mathsf{dy}$ in the VASS accepting the Dyck
language. We use $\mathsf{sd}$ to refer to the counters from either side,
$\mathsf{sj}$ or $\mathsf{dy}$. The idea is this: when we project the runs in
$\mathcal{S}$ to $\mathsf{sj}$, we obtain behavior of the subject VASS, and
when we project the runs to $\mathsf{dy}$, we obtain the effect that this
behavior has on the Dyck language. To achieve this, we expect that the
counters in $\mathsf{dy}$ are updated in a visible way, meaning a letter
$a_{i}$ leads to an increment of the $i$-th Dyck-counter, and $\bar{a}_{i}$
leads to a decrement. We lift the well-founded relation from MGTS to DMGTS and
define $(\mathcal{S}_{1},\mu_{1})<_{\mathsf{rnk}}(\mathcal{S}_{2},\mu_{2})$ by
$\mathcal{S}_{1}<_{\mathsf{rnk}}\mathcal{S}_{2}$. The size is
$|{\mathcal{W}}|=|{\mathcal{S}}|+|{\mu}|$, where $|{\mu}|$ is the length of
the binary representation. We call $\mathcal{W}$ _zero-reaching_ , if
$\mathcal{W}.c_{\mathsf{in}}[\mathsf{dy}]=\mathbf{0}=\mathcal{W}.c_{\mathsf{out}}[\mathsf{dy}]$.

When it comes to regular separability, we only track the Dyck language in an
approximate way, namely by acceptance modulo $\mu$, and so the number $\mu$ in
the definition of DMGTS is the precision of this approximation. The central
new notion will then be faithfulness: if we have an $\mathbb{N}$-run where we
only know that the Dyck-side is accepting modulo $\mu$, then we are sure the
Dyck-side is already accepting in the normal sense. This will allow us to
construct a regular separator in Section 7. To formulate acceptance modulo
$\mu$, we define the _modulo $\mu$ specialization order_
$\sqsubseteq_{\omega}^{\mu}\
\subseteq\mathbb{Z}_{\omega}\times\mathbb{Z}_{\omega}$ by
$i\sqsubseteq_{\omega}^{\mu}j$, if $j=\omega$ or $i\equiv j$ mod $\mu$. We
extend it to counter valuations and to configurations as we have done for the
specialization order. Given a preorder $\sqsubseteq$ on configurations, we use
$\sqsubseteq\\![\mathsf{sd}]$ for the restriction of the preorder that only
compares the counters in $\mathsf{sd}$, but does not constrain the remaining
counters.

Since DMGTS are MGTS, the definitions of runs, acceptance, and intermediate
acceptance carry over. To account for the fact that a DMGTS is meant to
represent two languages, one for the Dyck-side and one for the VASS-side, we
add the following abbreviations:

$\displaystyle\mathsf{(I)Acc}_{\mathsf{dy}}(\mathcal{W})\;\;$
$\displaystyle=\;\;\
\mathsf{(I)Acc}_{\mathsf{dy},\leq_{\omega}\\![\mathsf{dy}]}(\mathcal{W})$
$\displaystyle\mathsf{(I)Acc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})\;\;$
$\displaystyle=\;\;\
\mathsf{(I)Acc}_{\mathbb{Z},\leq_{\omega}\\![\mathsf{dy}]}(\mathcal{W})$
$\displaystyle\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{W})\;\;$
$\displaystyle=\;\;\
\mathsf{IAcc}_{\mathsf{sj},\leq_{\omega}\\![\mathsf{sj}]}(\mathcal{W})\;\cap\;\mathsf{IAcc}_{\mathsf{dy},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{W})\
$ $\displaystyle\mathsf{IAcc}_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})\;\;$
$\displaystyle=\;\;\
\mathsf{IAcc}_{\mathbb{Z},\leq_{\omega}\\![\mathsf{sj}]}(\mathcal{W})\;\cap\;\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{W})\
.$

A run is (intermediate) accepting for the Dyck-side, if the counters in the
set $\mathsf{dy}$ remain non-negative and on these counters the run is
(intermediate) accepting in the normal sense, expressed as
$\leq_{\omega}\\![\mathsf{dy}]$. A run is intermediate accepting on the VASS-
side, if the same holds for the counters in $\mathsf{sj}$ and, moreover, the
Dyck-side is accepting modulo $\mu$. The purpose of the intersection is to
limit the words the subject VASS may produce before violating separability.
This will become clear in Section 7. We also introduce
$\mathbb{Z}$-relaxations of these notions. With acceptance in place, we define
the languages

$\displaystyle L_{\mathsf{sd}}(\mathcal{W})\;\;$
$\displaystyle=\;\;\\{\lambda(\rho)\mid\rho\in\mathsf{IAcc}_{\mathsf{sd}}(\mathcal{W})\\}$
$\displaystyle L_{\mathbb{Z},\mathsf{sd}}(\mathcal{W})\;\;$
$\displaystyle=\;\;\\{\lambda_{\\#}(\rho)\mid\rho\in\mathsf{IAcc}_{\mathbb{Z},\mathsf{sd}}(\mathcal{W})\\}\
.$

By $\lambda_{\\#}$, we denote the function that extracts the edge labels
except that it replaces the label $\lambda(\mathit{up})$ of every update
between precovering graphs by $(\lambda(\mathit{up}),\\#)$. This will allow us
to uniquely identify the current precovering graph in a run. The following is
immediate.

###### Lemma 5.1.

If $\mathcal{W}$ is zero-reaching, we have
$L_{\mathsf{dy}}(\mathcal{W})\subseteq D_{n}$. One can construct a
$\mathbb{Z}$-VASS that accepts the language
$L_{\mathbb{Z},\mathsf{sd}}(\mathcal{W})$.

We also define characteristic equations for each side that mimic the notions
of acceptance we have just defined:

$\displaystyle\mathsf{Char}_{\mathsf{dy}}(G,\mu)$
$\displaystyle\;\;=\;\;\mathsf{RunsEq}(G)\wedge\mathsf{IAccEq}(G,\leq_{\omega}\\![\mathsf{dy}])$
$\displaystyle\mathsf{Char}_{\mathsf{sj}}(G,\mu)$
$\displaystyle\;\;=\;\;\mathsf{RunsEq}(G)\wedge\mathsf{IAccEq}(G,\leq_{\omega}\\![\mathsf{sj}])$
$\displaystyle\hskip
62.59596pt\wedge\mathsf{IAccEq}(G,\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}])$
$\displaystyle\mathsf{Char}_{\mathsf{sd}}(G.\mathit{up}.\mathcal{W},\mu)$
$\displaystyle\;\;=\;\;\mathsf{Char}_{\mathsf{sd}}(G,\mu)\wedge\mathsf{Char}_{\mathsf{sd}}(\mathcal{W},\mu)$
$\displaystyle\hskip 5.69046pt\wedge
x[G,\mathsf{out}]+\Delta(\mathit{up})-x[\mathcal{W}[\mathsf{first}],\mathsf{in}]=\mathbf{0}\
.$

We also define the support
$\mathsf{supp}(\mathsf{Char}_{\mathsf{sd}}(\mathcal{W}))$. As in the case of
reachability, we first define homogeneous variants of the above systems by
replacing concrete values in $\mathsf{IAccEq}(G,\sqsubseteq)$ with zero. Then
we collect the variables that receive a positive value in a solution to the
homogeneous characteristic equations.

The central new notion for regular separability is faithfulness. A DMGTS
$\mathcal{W}$ is _faithful_ , if it is zero-reaching and

(3) $\displaystyle\mathsf{Acc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})\ \cap\
\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{W})\quad\subseteq\quad\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})\
.$

The definition considers runs that take the Dyck counters from zero to zero.
That the initial and final valuations are precisely zero and not just zero
modulo $\mu$ is by the intersection with
$\mathsf{Acc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$. Faithfulness now says
that, for the intermediate precovering graphs in the underlying MGTS, there is
no difference between acceptance modulo $\mu$ and ordinary acceptance. Indeed,
the reverse inclusion is readily checked (but will not be needed).

A DMGTS $\mathcal{W}$ is _perfect_ , if it is faithful and for every
precovering graph $G$ in $\mathcal{W}$, for every
$\mathsf{sd}\in\\{\mathsf{sj},\mathsf{dy}\\}$,

  * •

$\mathsf{CS}_{\mathsf{up}}(G)\neq\emptyset\neq\mathsf{CS}_{\mathsf{down}}(G)\neq\emptyset$
and

  * •

$\mathsf{supp}(\mathsf{Char}_{\mathsf{sd}}(\mathcal{W}))$ justifies the
unboundedness of $\mathsf{sd}$ in $G$.

Note that the edge variables are in the support of both, the VASS-side and the
Dyck-side.

##  6\. Deciding Regular Separability

Our decision procedure for regular separability decomposes the DMGTS
$\mathcal{W}$ of interest until the regular separability
$L_{\mathsf{sj}}(\mathcal{W})\mid D_{n}$ reduces to the regular separability
of the $\mathbb{Z}$-VASS approximations
$L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})\mid
L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$. The latter problem can be solved
with the algorithm from [3], as stated in Theorem 3.5 above. Behind our
decision procedure are two key results. The first says that we can decompose
faithful DMTGS into two finite sets of DMTGS.

###### Lemma 6.1.

We can decompose a faithful DMTGS $\mathcal{W}$ in
$\mathbf{F}_{|{\mathsf{sj}\cup\mathsf{dy}}|+4}$ into two finite sets
$\mathsf{Perf}$ and $\mathsf{Fin}$ of DMTGS, where all
$\mathcal{S}\in\mathsf{Perf}$ are perfect, all $\mathcal{T}\in\mathsf{Fin}$
satisfy $L_{\mathsf{sj}}(\mathcal{T})\mid D_{n}$, and

$\displaystyle L_{\mathsf{sj}}(\mathcal{W})\quad=\quad
L_{\mathsf{sj}}(\mathsf{Perf}\cup\mathsf{Fin})\ .$

The second is a transfer result, saying that separability can be checked on
the $\mathbb{Z}$-approximations as soon as we have perfectness.

###### Lemma 6.2.

If $\mathcal{W}$ is faithful, then
$L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})\mid
L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$ implies
$L_{\mathsf{sj}}(\mathcal{W})\mid D_{n}$. If $\mathcal{W}$ is perfect, also
the reverse holds.

Since perfect DMGTS are faithful, the following is a consequence.

###### Corollary 6.3.

Let $\mathcal{W}$ be perfect. Then $L_{\mathsf{sj}}(\mathcal{W})\mid D_{n}$ if
and only if $L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})\mid
L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$.

These insights allow us to decide regular separability.

###### Proof of Proposition 3.4.

To ease the notation, we assume the subject VASS is actually a VAS,
$\mathcal{U}=((\\{v\\},\Sigma_{n},\mathsf{sj},E),(v,c_{1}),(v,c_{2}))$. It is
well-known that any VASS can be turned into a VAS with the same language by
introducing auxiliary counters for the states. One can also adapt our
procedure to directly work with VASS. We first check
$\mathit{L}(\mathcal{U})\cap D_{n}=\emptyset$. If the intersection is non-
empty, our decision procedure returns inseparable. If it is empty, we
construct an initial DMGTS $\mathcal{W}$ with
$\mathit{L}(\mathcal{U})=L_{\mathsf{sj}}(\mathcal{W})$. Checking
$\mathit{L}(\mathcal{U})\mid D_{n}$ then amounts to checking
$L_{\mathsf{sj}}(\mathcal{W})\mid D_{n}$.

We define $\mathcal{W}=(G,\mu)$ with $\mu=1$. The precovering graph $G$ uses
the underlying VASS
$\mathcal{V}=(\\{v_{\mathsf{root}}\\},\Sigma_{n},\mathsf{sj}\uplus\mathsf{dy},E^{\prime})$.
It has a single node and both sets of counters. The set of edges $E^{\prime}$
contains a loop $(v_{\mathsf{root}},a,(x,y),v_{\mathsf{root}})$ for every
$(v,a,x,v)\in E$. The vector $y$ modifies the counters in $\mathsf{dy}$ as
required by Dyck visibility. The precovering graph is
$G=(\mathcal{V},(v_{\mathsf{root}},(c_{1},\mathbf{0})),(v_{\mathsf{root}},(c_{2},\mathbf{0})),\varphi)$.
The root node is decorated by $\omega$, expressed as
$\varphi=\mathbb{N}^{\emptyset}$. The initial and final valuations expect the
counters in $\mathsf{sj}$ to behave like in $\mathcal{U}$, and the counters in
$\mathsf{dy}$ to go from zero to zero. For
$L_{\mathsf{sj}}(\mathcal{W})=\mathit{L}(\mathcal{U})$, note that the modulo
$\mu=1$ constraints that $L_{\mathsf{sj}}(\mathcal{W})$ imposes on the Dyck-
side do not mean a restriction.

To decide $L_{\mathsf{sj}}(\mathcal{W})\mid D_{n}$, we invoke Lemma 6.1. The
required faithfulness of $\mathcal{W}$ is trivial: the extremal valuations are
zero on $\mathsf{dy}$, and since there are no intermediate precovering graphs,
we have
$\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})=\mathsf{Acc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$.
The lemma yields finite sets of DMGTS $\mathsf{Perf}$ and $\mathsf{Fin}$ with
$L_{\mathsf{sj}}(\mathcal{W})=L_{\mathsf{sj}}(\mathsf{Perf})\cup
L_{\mathsf{sj}}(\mathsf{Fin})$. It moreover guarantees
$L_{\mathsf{sj}}(\mathcal{T})\mid D_{n}$ for all $\mathcal{T}\in\mathsf{Fin}$.
To decide $L_{\mathsf{sj}}(\mathcal{W})\mid D_{n}$, it thus remains to check
$L_{\mathsf{sj}}(\mathcal{S})\mid D_{n}$ for all
$\mathcal{S}\in\mathsf{Perf}$. If all checks succeed, our decision procedure
returns separable, and if one check fails, it returns inseparable. Since the
DMGTS in $\mathsf{Perf}$ are perfect, we can apply Corollary 6.3. We compute
$\mathbb{Z}$-VASS for the languages $L_{\mathbb{Z},\mathsf{sd}}(\mathcal{S})$
using Lemma 5.1, and check $L_{\mathbb{Z},\mathsf{sj}}(\mathcal{S})\mid
L_{\mathbb{Z},\mathsf{dy}}(\mathcal{S})$ with the algorithm from [3] that is
behind Theorem 3.5.

The decomposition of the DMGTS takes resources
$\mathbf{F}_{|{\mathsf{sj}\cup\mathsf{dy}}|+4}$, followed by an elementary
separability check. By [28, Lemma 4.6], this yields an $\mathbf{F}_{\omega}$
upper bound. ∎

##  7\. Separability Transfer

We prove the separability transfer result in Lemma 6.2.

###  7.1. Regular Separator

For the direction from left to right, we show that every regular separator for
the $\mathbb{Z}$-approximations $L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})$ and
$L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$ can be turned into a regular
separator for $L_{\mathsf{sj}}(\mathcal{W})$ and $D_{n}$. Faithfulness and
modulo reasoning will play an important role.

Let $\mathcal{B}^{\\#}$ separate $L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})$ and
$L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$. We write $\mathcal{B}$ for the NFA
that results from $\mathcal{B}^{\\#}$ by replacing transition labels $(a,\\#)$
with $a$. Our plan is to use $\mathcal{B}$ as a separator for
$L_{\mathsf{sj}}(\mathcal{W})$ and $D_{n}$. For this to work,
$\mathcal{B}^{\\#}$ should be _precise_ as follows:

(4) $\displaystyle\mathit{L}(\mathcal{B}^{\\#})\ \cap\ D_{n}^{\\#}\ \subseteq\
L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})\ .$

Preciseness says that the language of $\mathcal{B}^{\\#}$ is so small that it
cannot intersect the Dyck language without already intersecting
$L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$. The language $D_{n}^{\\#}$ offers
$a$ and $(a,\\#)$ whenever $D_{n}$ has letter $a$. The following is immediate.

###### Lemma 7.1.

If the NFA $\mathcal{B}^{\\#}$ separates
$L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})$ and
$L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$ and is precise, then $\mathcal{B}$
separates $L_{\mathsf{sj}}(\mathcal{W})$ and $D_{n}$.

Our main finding is the following lemma, where the product captures language
intersection,
$\mathit{L}(\mathcal{B}^{\\#}\times\mathcal{A}^{\\#})=\mathit{L}(\mathcal{B}^{\\#})\cap\mathit{L}(\mathcal{A}^{\\#})$.

###### Lemma 7.2.

Let $\mathcal{W}$ be faithful. Every separator $\mathcal{B}^{\\#}$ of
$L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})$ and
$L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$ can be turned into a precise
separator $\mathcal{B}^{\\#}\times\mathcal{A}^{\\#}$. The NFA
$\mathcal{A}^{\\#}$ is independent of $\mathcal{B}^{\\#}$.

A first failure of preciseness may be due to the fact that $\mathcal{B}^{\\#}$
accepts words that do not label a run through $\mathcal{W}$. To overcome the
problem, we understand $\mathcal{W}$ as an NFA
$\mathcal{B}^{\\#}({\mathcal{W}})$, and use this as $\mathcal{A}^{\\#}$ in the
lemma. If $\mathcal{B}^{\\#}({\mathcal{W}})$ accepts a word from
$D_{n}^{\\#}$, then the word labels a run through $\mathcal{W}$ that takes the
Dyck-counters from zero to zero. The latter holds, because the word is in the
Dyck-language and $\mathcal{W}$ is Dyck-visible. Since $\mathcal{W}$ is
faithful, the initial and final configurations are zero on $\mathsf{dy}$, and
so the run belongs to $\mathsf{Acc}_{\mathsf{dy}}(\mathcal{W})$.
Unfortunately, this does not suffice for preciseness.

The problem is that $L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$ is not defined
via $\mathsf{Acc}_{\mathsf{dy}}(\mathcal{W})$, but via intermediate acceptance
$\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$. This means the run not
only has to reach zero on the Dyck-counters, but it also has to reach certain
values at the entries and exits of the intermediate precovering graphs in
$\mathcal{W}$. This is where the Inclusion (3) in the definition of
faithfulness comes in. It suggests we should define the NFA
$\mathcal{A}^{\\#}$ so that it (i) follows $\mathcal{W}$ like
$\mathcal{B}^{\\#}({\mathcal{W}})$ does, (ii) maintains the counters modulo
the number $\mu$ given by $\mathcal{W}$, and (iii) checks intermediate
acceptance. If then $\mathcal{A}^{\\#}$ accepts a word from the Dyck-language,
we have a run in $\mathsf{Acc}_{\mathsf{dy}}(\mathcal{W})$ as before, but
moreover we know that the run belongs to
$\mathsf{IAcc}_{\mathsf{dy},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{W})$.
Faithfulness shows that the run is in
$\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$.

To be a separator, $\mathit{L}(\mathcal{B}^{\\#}\times\mathcal{A}^{\\#})$ has
to cover $L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})$. This holds, because
$L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})$ is not only defined via ordinary
acceptance on the counters in $\mathsf{sj}$, but also via modulo $\mu$
acceptance on $\mathsf{dy}$. The purpose of the constraint
$\mathsf{Acc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{W})$
in the definition of $\mathsf{Acc}_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})$ is
thus to support the above restriction of a given separator. The disjointness
$\mathit{L}(\mathcal{B}^{\\#}\times\mathcal{A}^{\\#})\cap
L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})=\emptyset$ is by the fact that
$\mathcal{B}^{\\#}$ is a separator. This justifies the product construction
$\mathcal{B}^{\\#}\times\mathcal{A}^{\\#}$ in the sense that
$\mathcal{A}^{\\#}$ alone may not be a separator.

It remains to define the NFA $\mathcal{A}^{\\#}$ that satisfies (i) to (iii)
above:

$\displaystyle\mathcal{A}^{\\#}=(Q\times[0,\mu-1]^{d},\Sigma_{n}\times\\{\varepsilon,\\#\\},\delta,$
$\displaystyle((G_{\mathsf{first}},\mathsf{in}),{(c_{1},\mathbf{0})}\mathop{\text{
mod }}{\mu}),$
$\displaystyle((G_{\mathsf{last}},\mathsf{out}),{(c_{2},\mathbf{0})}\mathop{\text{
mod }}{\mu}))\ .$

The set $Q$ contains states $(G,\mathsf{in})$ and $(G,\mathsf{out})$ for every
precovering graph $G$ im $\mathcal{W}$, and moreover all nodes in
$\mathcal{W}$. For every transition $(v,a,y,w)$ in a precovering graph of
$\mathcal{W}$ and for every counter valuation $x\in[0,\mu-1]^{d}$, we have

$\displaystyle(v,x)\xrightarrow{a}(w,{x+y}\mathop{\text{ mod
}}{\mu})\in\delta\ .$

We also have transitions that enter and exit a precovering graph $G$, or move
from $G$ to $G^{\prime}$ via the update $\mathit{up}$:

$\displaystyle((G,\mathsf{in}),x)\xrightarrow{\varepsilon}$
$\displaystyle(G.v_{\mathsf{root}},x)\in\delta,\hskip 24.18501pt\text{ if
}x\sqsubseteq_{\omega}^{\mu}G.c_{\mathsf{in}}$
$\displaystyle(G.v_{\mathsf{root}},x)\xrightarrow{\varepsilon}$
$\displaystyle((G,\mathsf{out}),x)\in\delta,\hskip 19.91684pt\text{ if
}x\sqsubseteq_{\omega}^{\mu}G.c_{\mathsf{out}}$
$\displaystyle((G,\mathsf{out}),x)\xrightarrow{(\lambda(\mathit{up}),\\#)}$
$\displaystyle((G^{\prime},\mathsf{in}),{x+\Delta(\mathit{up})}\mathop{\text{
mod }}{\mu})\in\delta\ .$

It is worth noting that this construction could have been done without the
$\\#$ symbol. The symbol only plays a role for the reverse implication in
Lemma 6.2 that we show next.

###  7.2. Inseparability

We prove the missing direction of Lemma 6.2, formulated as follows.

###### Lemma 7.3.

Consider a perfect DMGTS $\mathcal{W}$ that satisfies
$L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})\not{\mid}L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$.
Then also $L_{\mathsf{sj}}(\mathcal{W})\not{\mid}D_{n}$ holds.

The proof needs a classic definition [2]. A DFA $\mathcal{A}$ over $\Sigma$
induces the equivalence $\sim_{\mathcal{A}}\
\subseteq\Sigma^{*}\times\Sigma^{*}$ defined by $w\sim_{\mathcal{A}}v$, if for
all states $p,q$ in $\mathcal{A}$, we have
$p\mathop{\raisebox{-1.70709pt}{$\xrightarrow{w}$}}q$ if and only if
$p\mathop{\raisebox{-1.70709pt}{$\xrightarrow{v}$}}q$. The equivalence says
that the words lead to the same state changes in $\mathcal{A}$.

To prove Lemma 7.3, we reason towards a contradiction, and assume there is a
DFA $\mathcal{A}$ that separates $L_{\mathsf{sj}}(\mathcal{W})$ from $D_{n}$.
We use the premise
$L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})\not{\mid}L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$
and Lambert’s iteration lemma to construct words $o_{\mathsf{sj}}\in
L_{\mathsf{sj}}(\mathcal{W})$ and $o_{\mathsf{dy}}\in
L_{\mathsf{dy}}(\mathcal{W})$ with
$o_{\mathsf{sj}}\sim_{\mathcal{A}}o_{\mathsf{dy}}$. Then $\mathcal{A}$ must
accept or reject both words. If $\mathcal{A}$ accepts $o_{\mathsf{dy}}$, we
have a contradiction to $\mathit{L}(\mathcal{A})\cap D_{n}=\emptyset$ due to
Lemma 5.1. If $\mathcal{A}$ does not accept $o_{\mathsf{sj}}$, we have a
contradiction to
$L_{\mathsf{sj}}(\mathcal{W})\subseteq\mathit{L}(\mathcal{A})$. This concludes
the proof.

To construct $o_{\mathsf{sj}}$ and $o_{\mathsf{dy}}$, we use the following
lemma. Here, we need the $\\#$ symbols in the definition of
$L_{\mathbb{Z},\mathsf{sd}}(\mathcal{W})$.

###### Lemma 7.4.

Consider a DFA $\mathcal{A}$ such that for all pairs of words
$w_{0}(a_{1},\\#)\ldots w_{k}\in L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})$ and
$v_{0}(a_{1},\\#)\ldots v_{k}\in L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$
there is $i\leq k$ with $w_{i}\not\sim_{\mathcal{A}}v_{i}$. Then
$L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})\mid
L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$.

###### Proof.

It is well-known that the equivalence $\sim_{\mathcal{A}}$ has finite index
and the equivalence classes $[w]_{\sim_{\mathcal{A}}}$ are regular languages
[2]. Then the following is a finite union of regular languages:

$\displaystyle S\quad=\quad\bigcup_{w_{0}(a_{1},\\#)\ldots w_{k}\in
L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})}[w_{0}]_{\sim_{\mathcal{A}}}(a_{1},\\#)\ldots[w_{k}]_{\sim_{\mathcal{A}}}\
.$

We show that the regular language $S$ separates
$L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})$ and
$L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$. The inclusion
$L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})\subseteq S$ is immediate. Assume
there is $v\in S\cap L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$. Then
$v=v_{0}(a_{1},\\#)\ldots v_{k}\in L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$
and there is $w_{0}(a_{1},\\#)\ldots w_{k}\in
L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})$ so that
$v_{i}\sim_{\mathcal{A}}w_{i}$ for all $i\leq k$. This is the conclusion that
needs the $\\#$ symbols. Without them, the equivalent words may not align with
the precovering graphs. The conclusion contradicts the lemma’s premise, and
$v$ cannot exist. ∎

We proceed with the definition of the words $o_{\mathsf{sj}}$ and
$o_{\mathsf{dy}}$. We apply Lemma 7.4 in contraposition to
$L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})\not{\mid}L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$.
This yields $c_{0}\ldots c_{k}\in L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})$ and
$b_{0}\ldots b_{k}\in L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$ so that for all
$i\leq k$ we have $c_{i}\sim_{\mathcal{A}}b_{i}$. The membership in
$L_{\mathbb{Z},\mathsf{sj}}(\mathcal{W})$ resp.
$L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$ gives us loops $g_{i}$ and $h_{i}$
in every precovering graph $G_{i}$ of $\mathcal{W}$ that start in the root and
are labeled by $c_{i}$ resp. $b_{i}$. Moreover, since the languages are
defined via intermediate acceptance, we know that $\sum_{i\leq k}\psi(g_{i})$
and $\sum_{i\leq k}\psi(h_{i})$ solve
$\mathsf{Char}_{\mathsf{sj}}(\mathcal{W})$ resp.
$\mathsf{Char}_{\mathsf{dy}}(\mathcal{W})$. To sum up, the words given by
Lemma 7.4 provide solutions to the characteristic equations as we need them to
apply Lambert’s pumping lemma.

The perfectness of $\mathcal{W}$ yields covering sequences
$u_{i}^{\prime}\in\mathsf{CS}_{\mathsf{up}}(G_{i})$ and
$v_{i}^{\prime}\in\mathsf{CS}_{\mathsf{down}}(G_{i})$ for all $i\leq k$. We
show how to construct new covering sequences $u_{i}$ and $v_{i}$, as well as
further rooted loops $\mathit{w}_{\mathsf{sj},i}$ and
$\mathit{w}_{\mathsf{dy},i}$ in each precovering graph $G_{i}$ so that the
conditions on the homogeneous solutions formulated by Lambert’s pumping lemma
are met for both, $(u_{i},\mathit{w}_{\mathsf{sj},i},v_{i})_{i\leq k}$ and
$(u_{i},\mathit{w}_{\mathsf{dy},i},v_{i})_{i\leq k}$. In addition, we will
guarantee that
$\lambda(\mathit{w}_{\mathsf{sj},i})\sim_{\mathcal{A}}\lambda(\mathit{w}_{\mathsf{dy},i})$.
Applying Lemma 4.2 twice then yields a common $c\in\mathbb{N}$ so that

$\displaystyle
o_{\mathsf{sj}}=\lambda(u_{0}^{c}g_{0}\mathit{w}_{\mathsf{sj},0}^{c}v_{0}^{c}t_{0}\ldots
t_{k-1}u_{k}^{c}g_{k}\mathit{w}_{\mathsf{sj},k}^{c}v_{k}^{c})$
$\displaystyle\in L_{\mathsf{sj}}(\mathcal{S})$ $\displaystyle
o_{\mathsf{dy}}=\lambda(u_{0}^{c}h_{0}\mathit{w}_{\mathsf{dy},0}^{c}v_{0}^{c}t_{0}\ldots
t_{k-1}u_{k}^{c}h_{k}\mathit{w}_{\mathsf{dy},k}^{c}v_{k}^{c})$
$\displaystyle\in L_{\mathsf{dy}}(\mathcal{S})\ .$

Note that $o_{\mathsf{sj}}\in L_{\mathsf{sj}}(\mathcal{S})$ also requires
$\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{W})$.
This is taken care of by the modulo constraints in
$\mathsf{Char}_{\mathsf{sj}}(\mathcal{W})$.

With this definition, the desired
$o_{\mathsf{sj}}\sim_{\mathcal{A}}o_{\mathsf{dy}}$ is a consequence of
$\lambda(g_{i})\sim_{\mathcal{A}}\lambda(h_{i})$ and
$\lambda(\mathit{w}_{\mathsf{sj},i})\sim_{\mathcal{A}}\lambda(\mathit{w}_{\mathsf{dy},i})$
for all $i\leq k$.

We turn to the construction of $u_{i}$, $v_{i}$, $\mathit{w}_{\mathsf{sj},i}$,
and $\mathit{w}_{\mathsf{dy},i}$. To ease the notation, we fix a precoving
graph $G$ and skip the index $i$. So $u^{\prime}$ and $v^{\prime}$ will be the
pumping sequences for this precovering graph, $E$ will be the edges in this
precovering graph, and $u$, $v$, $\mathit{w}_{\mathsf{sj}}$, and
$\mathit{w}_{\mathsf{dy}}$ are the sequences we want to construct.

With $\mathit{N}$ the number of states in $\mathcal{A}$, we define

(5) $\displaystyle\mathit{w}_{\mathsf{sj}}\ =\
\mathsf{diff}^{\mathit{N}}.\mathsf{rem}\qquad\mathit{w}_{\mathsf{dy}}\ =\
\mathsf{diff}^{\mathit{N}+c\cdot\mathit{N}!}.\mathsf{rem}\ .$

The integer $c\geq 1$ will become clear when we define $\mathsf{rem}$. To see
$\lambda(\mathit{w}_{\mathsf{sj}})\sim_{\mathcal{A}}\lambda(\mathit{w}_{\mathsf{dy}})$,
let $p$ and $q$ be states in $\mathcal{A}$. Since $\mathcal{A}$ is a DFA,
there is a unique run from $p$ on $\lambda(\mathit{w}_{\mathsf{sj}})$.
Consider the part of the run that reads $\lambda(\mathsf{diff}^{\mathit{N}})$.
By the pigeonhole principle, there are $0\leq i<j\leq\mathit{N}$ where the
state after reading $\lambda(\mathsf{diff}^{i})$ and
$\lambda(\mathsf{diff}^{j})$ is the same. This means we can repeat
$\lambda(\mathsf{diff}^{j-i})$ and still arrive at this state. While we repeat
$\mathsf{diff}^{j-i}$ only once in $\mathit{w}_{\mathsf{sj}}$, we repeat it an
additional $c\cdot\mathit{N}!/(j-i)$ times in $\mathit{w}_{\mathsf{dy}}$. The
sole purpose of the factorial $\mathit{N}!$ is to guarantee that this division
by $j-i$ results in an integer: $j-i\leq\mathit{N}$ implies
$\mathit{N}!/(j-i)\in\mathbb{N}$. Since the states reached after
$\lambda(\mathsf{diff}^{\mathit{N}})$ and
$\lambda(\mathsf{diff}^{\mathit{N}+c\cdot\mathit{N}!})$ coincide, we have that
$\lambda(\mathit{w}_{\mathsf{sj}})$ leads from $p$ to $q$ if and only if this
holds for $\lambda(\mathit{w}_{\mathsf{dy}})$.

It remains to construct $u$, $v$, $\mathsf{diff}$, and $\mathsf{rem}$ for each
precovering graph. By Lemma 4.2, we can find full support solutions
$\mathit{s}_{\mathsf{sj}}$ and $\mathit{s}_{\mathsf{dy}}$ that satisfy the
Conditions (1) and (2) wrt. $u^{\prime}$ and $v^{\prime}$. We will not only
construct cycles, but also new support solutions
$\mathit{s}_{\mathsf{sj}}^{*}$ and $\mathit{s}_{\mathsf{dy}}^{*}$. Our
construction is guided by the following equations in Lemma 4.2:

(6) $\displaystyle\psi(u)+\psi(v)+\psi(\mathit{w}_{\mathsf{sj}})\ $
$\displaystyle=\ \mathit{s}_{\mathsf{sj}}^{*}\\![E]$ (7)
$\displaystyle\psi(u)+\psi(v)+\psi(\mathit{w}_{\mathsf{dy}})\ $
$\displaystyle=\ \mathit{s}_{\mathsf{dy}}^{*}\\![E]\ .$

By inserting the shape of $\mathit{w}_{\mathsf{sj}}$ and
$\mathit{w}_{\mathsf{dy}}$ required by Equation (5) and subtracting Equation
(6) from (7), we obtain

(8) $\displaystyle c\cdot\mathit{N}!\cdot\psi(\mathsf{diff})\ =\
(\mathit{s}_{\mathsf{dy}}^{*}-\mathit{s}_{\mathsf{sj}}^{*})[E]\ .$

This leads us to define

(9) $\displaystyle\mathit{s}_{\mathsf{sd}}^{*}\ =\
c\cdot\mathit{N}!\cdot\mathit{s}_{\mathsf{sd}}\ .$

We can now divide Equation (8) by $c\cdot\mathit{N}!$ and obtain

$\displaystyle\mathsf{diff}\ =\
\langle\mathit{s}_{\mathsf{dy}}-\mathit{s}_{\mathsf{sj}}\rangle\ .$

Here, we use $\langle v\rangle$ to turn a Parikh vector $v\geq\mathbf{1}$ into
a cycle. We can assume
$(\mathit{s}_{\mathsf{dy}}-\mathit{s}_{\mathsf{sj}})[E]\geq\mathbf{1}$,
because we could have scaled the support solution for the Dyck-side by an
appropriate factor.

The new support solutions in Equation (9) suggest we should define the new
covering sequences by repetition:

(10) $\displaystyle u\ =\ (u^{\prime})^{c\cdot\mathit{N}!}\qquad\qquad v\ =\
(v^{\prime})^{c\cdot\mathit{N}!}\ .$

We insert the Equations (5), (9), and (10) into (6) and get

$\displaystyle
c\cdot\mathit{N}!\cdot(\psi(u^{\prime})+\psi(v^{\prime}))+\mathit{N}\cdot\psi(\mathsf{diff})+\psi(\mathsf{rem})\
=\ c\cdot\mathit{N}!\cdot\mathit{s}_{\mathsf{sj}}[E]\ .$

This yields the missing

$\displaystyle\mathsf{rem}\ =\ \langle
c\cdot\mathit{N}!\cdot(\mathit{s}_{\mathsf{sj}}\\![E]-\psi(u^{\prime})-\psi(v^{\prime}))-\mathit{N}\cdot\psi(\mathsf{diff})\rangle\
.$

This is the moment we need the factor $c$: it has to be large enough so that
$c\cdot\mathit{N}!\cdot(\mathit{s}_{\mathsf{sj}}\\![E]-\psi(u^{\prime})-\psi(v^{\prime}))-\mathit{N}\cdot\psi(\mathsf{diff})\geq\mathbf{1}$,
and hence the vector can be realized as a cycle. Note that $c$ goes into the
definition of the support solution, which is shared by all precovering graphs.
This means the choice of $c$ not only has to satisfy the inequality for $G$,
but for all precovering graphs.

##  8\. Decomposition

We prove Lemma 6.1 by developing a decomposition algorithm that takes a
faithful DMGTS and returns a finite set of perfect DMGTS and a finite set of
DMGTS for which separability holds. At the heart of the algorithm is a single
decomposition step as follows.

###### Lemma 8.1.

There is a function $\textsf{dec}(-)$, computable with elementary resources,
that expects a faithful but imperfect DMGTS $\mathcal{W}$ with
$\mathsf{sol}(\mathsf{Char}_{\mathsf{sj}}(\mathcal{W}))\neq\emptyset$ and
$\mathsf{sol}(\mathsf{Char}_{\mathsf{dy}}(\mathcal{W}))\neq\emptyset$, and
returns finite sets $X,Y$ of DMGTS so that

  * (a)

for all $\mathcal{W}^{\prime}\in X$ we have faithfulness and
$\mathcal{W}^{\prime}<_{\mathsf{rnk}}\mathcal{W}$,

  * (b)

for all $\mathcal{W}^{\prime}\in Y$ we have
$L_{\mathsf{sj}}(\mathcal{W}^{\prime})\mid D_{n}$, and

  * (c)

$L_{\mathsf{sj}}(\mathcal{W})=L_{\mathsf{sj}}(X\cup Y)$.

Lemma 8.1 readily implies Lemma 6.1.

###### Proof of Lemma 6.1.

We formulate the overall decomposition algorithm and afterwards reason about
its correctness. The input to the decomposition is a faithful DMGTS
$\mathcal{W}$. If $\mathcal{W}$ is perfect, then we return
$\mathsf{Perf}=\\{\mathcal{W}\\},\mathsf{Fin}=\emptyset$. If
$\mathsf{sol}(\mathsf{Char}_{\mathsf{sj}}(\mathcal{W}))=\emptyset$, then we
return $\mathsf{Perf}=\mathsf{Fin}=\emptyset$. If
$\mathsf{sol}(\mathsf{Char}_{\mathsf{dy}}(\mathcal{W}))=\emptyset$, then we
return $\mathsf{Perf}=\emptyset$ and $\mathsf{Fin}=\\{\mathcal{W}\\}$. If
these conditions do not apply, we invoke $\textsf{dec}(-)$ from Lemma 8.1 to
generate sets $X$ and $Y$ of DMGTS with the stated properties. We recursively
call our decomposition algorithm on each DMGTS $\mathcal{S}\in X$, which
returns $\mathsf{Perf}_{\mathcal{S}}$ and $\mathsf{Fin}_{\mathcal{S}}$. We
include all DMGTS from $(\mathsf{Perf}_{\mathcal{S}})_{\mathcal{S}\in X}$ in
$\mathsf{Perf}$, and all DMGTS from
$(\mathsf{Fin}_{\mathcal{S}})_{\mathcal{S}\in X}$ as well as from $Y$ in
$\mathsf{Fin}$.

We reason about correctness with an induction on the height of the call tree.
The tree is finite as every recursive call decreases the well-founded order,
each node has a finite outdegree, and hence König’s lemma applies. For a
perfect DMGTS, there is nothing to do. If
$\mathsf{sol}(\mathsf{Char}_{\mathsf{sj}}(\mathcal{W}))=\emptyset$, then
$L_{\mathsf{sj}}(\mathcal{W})=\emptyset$ follows and we are done. If
$\mathsf{sol}(\mathsf{Char}_{\mathsf{dy}}(\mathcal{W}))=\emptyset$, the set
$Y=\\{\mathcal{W}\\}$ preserves the language. Since
$\mathsf{sol}(\mathsf{Char}_{\mathsf{dy}}(\mathcal{W}))=\emptyset$ implies
$L_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})=\emptyset$, the required separability
holds by the forward direction of Lemma 6.2.

In the induction step, the induction hypothesis and Lemma 8.1 show that for
the DMGTS in $\mathsf{Fin}$ the required separability holds. The induction
hypothesis moreover shows that the DMGTS in $\mathsf{Perf}$ are perfect. We
have
$L_{\mathsf{sj}}(\mathcal{W})=L_{\mathsf{sj}}(\mathsf{Perf}\cup\mathsf{Fin})$,
because $L_{\mathsf{sj}}(\mathcal{W})=L_{\mathsf{sj}}(X\cup Y)$ by Lemma 8.1
and, by the induction hypothesis, our decomposition yields
$L_{\mathsf{sj}}(\mathcal{S})=L_{\mathsf{sj}}(\mathsf{Perf}_{\mathcal{S}}\cup\mathsf{Fin}_{\mathcal{S}})$
for all $\mathcal{S}\in X$.

Perfectness and infeasibility can be checked with time and space elementary in
the size of the input DMGTS [18]. By Lemma 8.1, also
$\textsf{dec}(\mathcal{W})$ is computable with resources elementary in
$|{\mathcal{W}}|$. The well-founded relation $<_{\mathsf{rnk}}$ is defined as
a lexicographic order on $\mathbb{N}^{|{\mathsf{sj}\cup\mathsf{dy}}|+1}$. This
yields an algorithm in $\mathbf{F}_{|{\mathsf{sj}\cup\mathsf{dy}}|+4}$ by the
same argument as [24, Theorem 5.4]. ∎

Lemma 8.1 deals with faithful but imperfect DMGTS. A faithful DMGTS
$\mathcal{W}$ is not perfect if and only if it contains a precovering graph
$G$ for which one of the following conditions holds.

  * (i)

There are $\mathsf{sd}\in\\{\mathsf{sj},\mathsf{dy}\\}$, a counter
$\mathit{j}\in\mathsf{sd}$, and
$c_{\mathsf{io}}\in\\{c_{\mathsf{in}},c_{\mathsf{out}}\\}$ so that
$c_{\mathsf{io}}[\mathit{j}]=\omega$ but
$x[G,\mathsf{io},\mathit{j}]\not\in\mathsf{supp}(\mathsf{Char}_{\mathsf{sd}}(\mathcal{W}))$.

  * (ii)

There are a side $\mathsf{sd}\in\\{\mathsf{sj},\mathsf{dy}\\}$ and an edge
$e\in G.E$ so that
$x[e]\not\in\mathsf{supp}(\mathsf{Char}_{\mathsf{sd}}(\mathcal{W}))$.

  * (iii)

We have $\mathsf{CS}_{\mathsf{up}}(G)=\emptyset$ or
$\mathsf{CS}_{\mathsf{down}}(G)=\emptyset$.

Case (iii) is part of the perfectness definition. The Cases (i) and (ii)
follow from the fact that
$\mathsf{supp}(\mathsf{Char}_{\mathsf{sd}}(\mathcal{W}))$ should capture the
unboundedness of $\mathsf{sd}$ in $\mathcal{W}$. We break down the proof of
Lemma 8.1 into three arguments, one for each of the cases.

###  8.1. Case (i)

Consider a faithful but imperfect DMGTS $\mathcal{W}=(\mathcal{U},\mu)$ that
satisfies
$\mathsf{sol}(\mathsf{Char}_{\mathsf{sj}}(\mathcal{W}))\neq\emptyset\neq\mathsf{sol}(\mathsf{Char}_{\mathsf{dy}}(\mathcal{W}))$.
In Case (i), there is a precovering graph $G$, a side
$\mathsf{sd}\in\\{\mathsf{sj},\mathsf{dy}\\}$, a counter
$\mathit{j}\in\mathsf{sd}$, and a counter valuation
$c_{\mathsf{io}}\in\\{G.c_{\mathsf{in}},G.c_{\mathsf{out}}\\}$ so that
$c_{\mathsf{io}}[\mathit{j}]=\omega$ but
$x[G,\mathsf{io},\mathit{j}]\notin\mathsf{supp}(\mathsf{Char}_{\mathsf{sd}}(\mathcal{W}))$.
If the variable is not in the support, the set of values
$A_{\mathsf{sd}}=\\{s[G,\mathsf{io},\mathit{j}]\mid
s\in\mathsf{sol}(\mathsf{Char}_{\mathsf{sd}}(\mathcal{W}))\\}$ is finite. We
also know $A_{\mathsf{sd}}\neq\emptyset$, because
$\mathsf{sol}(\mathsf{Char}_{\mathsf{sd}}(\mathcal{W}))\neq\emptyset$.
Finally, we have $A_{\mathsf{sd}}\subseteq\mathbb{N}$ by the shape of
$\mathsf{Char}_{\mathsf{sd}}(\mathcal{W})$. We show how to construct
$(X,Y)=\textsf{dec}(\mathcal{W})$ as required by Lemma 8.1.

#### Case $\mathsf{sd}=\mathsf{sj}$

Let $\mathcal{U}_{a}$ be the MGTS that results from $\mathcal{U}$ by changing
the entry or exit value of counter $\mathit{j}$ in $G$ from $\omega$ to
$a\in\mathbb{N}$. We define

$\displaystyle X\ =\ \\{(\mathcal{U}_{a},\mu)\mid a\in
A_{\mathsf{sj}}\\}\qquad\text{and}\qquad Y\ =\ \emptyset\ .$

###### Proof.

We begin with Property (c) in Lemma 8.1. The difference between $\mathcal{W}$
and $\mathcal{W}_{\mathsf{new}}=(\mathcal{U}_{a},\mu)$ is a single entry or
exit value that changes from $\omega$ to $a$. This makes intermediate
acceptance stricter,
$\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{W}_{\mathsf{new}})\subseteq\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{W})$,
and so we have $L_{\mathsf{sj}}(X\cup Y)\subseteq
L_{\mathsf{sj}}(\mathcal{W})$. For the reverse inclusion, we use that every
run $\rho\in\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{W})$ induces a solution to
$\mathsf{Char}_{\mathsf{sj}}(\mathcal{W})$. Then $\rho$ enters or exits the
precovering graph $G$ with a value $a\in A_{\mathsf{sj}}$ on counter
$\mathit{j}$. For Property (b), there is nothing to show as $Y=\emptyset$. For
Property (a), note that we do not modify the edges, nodes, or
$\mathsf{dy}$-valuations when moving from $\mathcal{U}$ to $\mathcal{U}_{a}$.
Hence, the faithfulness of $\mathcal{W}_{\mathsf{new}}=(\mathcal{U}_{a},\mu)$
follows from the faithfulness of $\mathcal{W}$. We reduce the well-founded
order, because we replace say an exit value $\omega$ by a concrete value,
while keeping $G.E$, $\Omega(G)$, and $G.c_{\mathsf{in}}$ unchanged. The
complexity follows from the fact that the set $A_{\mathsf{sj}}$ can be
constructed using resources elementary in the size of $\mathcal{W}$ [18]. ∎

#### Case $\mathsf{sd}=\mathsf{dy}$

The construction uses an equivalence
$\mathcal{S}_{1}\simeq_{\mu}\mathcal{S}_{2}$ on MGTS. It is the least
equivalence that satisfies the following. For precovering graphs, we have
$G_{1}\simeq_{\mu}G_{2}$ if the nodes, the edges, and the root coincide, and
moreover
$G_{1}.c_{\mathsf{io}}[\mathsf{sj}]=G_{2}.c_{\mathsf{io}}[\mathsf{sj}]$ and
$G_{1}.c_{\mathsf{io}}[\mathsf{dy}]\equiv
G_{2}.c_{\mathsf{io}}[\mathsf{dy}]\mathop{\text{ mod }}\mu$, for both,
$\mathsf{io}=\mathsf{in}$ and $\mathsf{io}=\mathsf{out}$. For composed MGTS,
we use

$\displaystyle\mathcal{S}_{1}.\mathit{up}.\mathcal{S}_{2}\simeq_{\mu}\mathcal{S}_{1}^{\prime}.\mathit{up}.\mathcal{S}_{2}^{\prime}\mathcal{S}_{1}\simeq_{\mu}\mathcal{S}_{1}^{\prime}\qquad\mathcal{S}_{2}\simeq_{\mu}\mathcal{S}_{2}^{\prime}\
.$

Equivalent MGTS may only differ in the entry and exit values of Dyck counters,
and these values still have to coincide modulo $\mu$. As a piece of notation,
we use $0\leq\mathcal{S}<c$ with $c\in\mathbb{N}$ to mean
$G^{\prime}.c_{\mathsf{in}}$ and $G^{\prime}.c_{\mathsf{out}}$ only take
values from $[0,c-1]\cup\\{\omega\\}$, for all $G^{\prime}$ in $\mathcal{S}$.

To define $X$ and $Y$, we choose the least value $l$ that is larger than the
maximal value in $A_{\mathsf{dy}}$ and moreover larger than any entry or exit
value in a precovering graph of $\mathcal{U}$. We set
$\mu_{\mathsf{new}}=l\cdot\mu$ and

$\displaystyle Z\ $ $\displaystyle=\
\\{(\mathcal{S},\mu_{\mathsf{new}})\mid\mathcal{S}\simeq_{\mu}\mathcal{U}_{a},\;0\leq
a,\mathcal{S}<\mu_{\mathsf{new}},\;\mathcal{S}.c_{\mathsf{in}}[\mathsf{dy}]=\mathbf{0}\\}$
$\displaystyle X\ $ $\displaystyle=\ \\{(\mathcal{S},\mu_{\mathsf{new}})\in
Z\mid\mathcal{S}.c_{\mathsf{out}}[\mathsf{dy}]=\mathbf{0}\\}$ $\displaystyle
Y\ $ $\displaystyle=\ Z\setminus X\ .$

We discuss three important points before turning to the proof. We deliberately
not only replace $\omega$ by values from $A_{\mathsf{dy}}$, but by all values
$0\leq a<\mu_{\mathsf{new}}$. The reason is that
$L_{\mathsf{sj}}(\mathcal{W})$ also checks intermediate acceptance for the
Dyck counters, but only modulo $\mu$. The set $A_{\mathsf{dy}}$ is constructed
from runs where the Dyck counters reach intermediate values precisely. This
means $A_{\mathsf{dy}}$ may not offer enough values for
$L_{\mathsf{sj}}(\mathcal{W})\subseteq L_{\mathsf{sj}}(X\cup Y)$ to hold.

The definition of $\mu_{\mathsf{new}}$ addresses the main challenge in this
case, namely the faithfulness of the DMGTS
$\mathcal{W}_{\mathsf{new}}=(\mathcal{S},\mu_{\mathsf{new}})\in X$. We have to
show that we reach the value $0\leq a<\mu_{\mathsf{new}}$ that replaces
$\omega$, whenever we reach it modulo $\mu_{\mathsf{new}}$. The idea is this.
The left-hand side of Inclusion (3) will allow us to show that the run belongs
to $\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$. A consequence is
that it reaches $b\in A_{\mathsf{dy}}\subseteq\mathbb{N}$ with
$b<\mu_{\mathsf{new}}$. We thus reach $a$ if we can show $b=a$. We use the
following property of the modulo equivalence.

###### Lemma 8.2.

Consider $\mu_{\mathsf{new}}\in\mathbb{N}$. For all $x,k\in\mathbb{N}$, we
have that $x,k<\mu_{\mathsf{new}}$ and $x\equiv k\mathop{\text{ mod
}}\mu_{\mathsf{new}}$ together imply $x=k$.

The missing $b\equiv a\mathop{\text{ mod }}\mu_{\mathsf{new}}$ is by
$\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu_{\mathsf{new}}}\\![\mathsf{dy}]}(\mathcal{W}_{\mathsf{new}})$,
which is a premise of faithfulness. To sum up, we let $\mu_{\mathsf{new}}$
exceed the counter values that any run (satisfying the premise of
faithfulness) can take (in the moment we use $a$ for $\omega$), and so we do
not lose information by only tracking counter values modulo
$\mu_{\mathsf{new}}$.

The change from $\mu$ to $\mu_{\mathsf{new}}$ brings $\simeq_{\mu}$ to the
definition of $X$ and $Y$. The purpose of the equivalence is to modify the
entry and exit valuations of the Dyck counters in all precovering graphs. To
see the need for a modification, note that such a valuation is a constraint of
the form $x\equiv k\mathop{\text{ mod }}\mu$. Imagine now we multiply $\mu=3$
by $l=4$ and get $\mu_{\mathsf{new}}=12$. Assume $k=2$. To obtain all
solutions to $x\equiv 2\mathop{\text{ mod }}3$, it is not sufficient to
consider $x\equiv 2\mathop{\text{ mod }}12$. We need to join the solutions to
$x\equiv i\mathop{\text{ mod }}12$ for all $i\in\\{2,5,8,11\\}$. The reason
these values $i$ collect all solutions, is the following property.

###### Lemma 8.3.

Let $\mu$ divide $\mu_{\mathsf{new}}$. For all $x,k\in\mathbb{Z}$ with
$x\equiv k\mathop{\text{ mod }}\mu$, there is a $0\leq i<\mu_{\mathsf{new}}$
with $x\equiv i\mathop{\text{ mod }}\mu_{\mathsf{new}}$ and $i\equiv
k\mathop{\text{ mod }}\mu$.

The equivalence $\simeq_{\mu}$ incorporates all and only these choices of $i$.

###### Proof.

We prove Property (c) in Lemma 8.1 and begin with the inclusion
$L_{\mathsf{sj}}(X\cup Y)\subseteq L_{\mathsf{sj}}(\mathcal{W})$. Let
$\mathcal{W}_{\mathsf{new}}=(\mathcal{S},\mu_{\mathsf{new}})\in X\cup Y$. By
definition, $\mathcal{S}\simeq_{\mu}\mathcal{U}_{a}$ for some $0\leq
a<\mu_{\mathsf{new}}$. We argue that

$\displaystyle\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{W}_{\mathsf{new}})\subseteq\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{S},\mu)\subseteq\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{U}_{a},\mu)\subseteq\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{W})\
.$

The first inclusion is by the fact that $\mu$ divides $\mu_{\mathsf{new}}$.
The next uses the fact that $\simeq_{\mu}$ preserves the valuations of the
counters in $\mathsf{sj}$ and the valuations of the counters in $\mathsf{dy}$
modulo $\mu$, and so $\mathsf{IAcc}_{\mathsf{sj}}(-)$ is invariant under this
equivalence. The last inclusion is by the fact that concrete values make
intermediate acceptance stricter.

For the inclusion $L_{\mathsf{sj}}(\mathcal{W})\subseteq L_{\mathsf{sj}}(X\cup
Y)$, consider $\rho\in\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{W})$. As we do not
change the entry and exit valuations for the counters in $\mathsf{sj}$, we
readily have
$\rho\in\mathsf{IAcc}_{\mathsf{sj},\leq_{\omega}\\![\mathsf{sj}]}(\mathcal{W}_{\mathsf{new}})$
for all $\mathcal{W}_{\mathsf{new}}\in X\cup Y$. What remains is to argue that
$\rho\in\mathsf{IAcc}_{\mathsf{dy},\sqsubseteq_{\omega}^{\mu_{\mathsf{new}}}\\![\mathsf{dy}]}(\mathcal{W}_{\mathsf{new}})$
for some $\mathcal{W}_{\mathsf{new}}=(\mathcal{S},\mu_{\mathsf{new}})\in X\cup
Y$. Let $\rho$ enter or leave the precovering graph $G$ of interest with
counter valuation $c$. Let $a\in[0,\mu_{\mathsf{new}}-1]$ be such that
$c[\mathit{j}]\equiv a\mathop{\text{ mod }}\mu_{\mathsf{new}}$, where
$\mathit{j}$ is the counter of interest. By Lemma 8.3, there is
$(\mathcal{S},\mu_{\mathsf{new}})\in X\cup Y$ with
$\mathcal{S}\simeq_{\mu}\mathcal{U}_{a}$ for which the run is intermediate
accepting.

For the separability stated in (b), let
$\mathcal{W}_{\mathsf{new}}=(\mathcal{S},\mu_{\mathsf{new}})\in Y$. The
definition of $Y$ yields
$\mathcal{S}.c_{\mathsf{in}}[\mathsf{dy}]=\mathbf{0}$. Moreover, we know that
$0<\mathcal{S}.c_{\mathsf{out}}[\mathit{j}]<\mu_{\mathsf{new}}$ for all
$\mathit{j}\in\mathsf{dy}$. The final values are concrete, because
$\mathcal{W}$ is zero-reaching by faithfulness. They are bounded by
$\mu_{\mathsf{new}}$ due to $0\leq\mathcal{S}<\mu_{\mathsf{new}}$. They are
different from zero by the definition of $Y$. The analysis of the initial and
final values shows that every
$\rho\in\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{W}_{\mathsf{new}})\subseteq\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu_{\mathsf{new}}}\\![\mathsf{dy}]}(\mathcal{W}_{\mathsf{new}})$
has an effect $c\not\equiv\mathbf{0}\mathop{\text{ mod }}\mu_{\mathsf{new}}$
on the Dyck counters. By Dyck visibility, the word $\lambda(\rho)$ must have
the same effect on $\mathcal{D}_{n}$. Then, a DFA that tracks the Dyck
counters modulo $\mu_{\mathsf{new}}$ and only accepts upon valuations
different from zero modulo $\mu_{\mathsf{new}}$ shows
$L_{\mathsf{sj}}(\mathcal{W}_{\mathsf{new}})\mid D_{n}$.

For Property (a), the argument that the well-founded relation decreases is the
same as in the case $\mathsf{sd}=\mathsf{sj}$. For faithfulness, consider
$\mathcal{W}_{\mathsf{new}}=(\mathcal{S},\mu_{\mathsf{new}})\in X$. It is
zero-reaching by definition. The challenge is to prove Inclusion (3). We
reason as follows:

(11)
$\displaystyle\mathsf{Acc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W}_{\mathsf{new}})\cap\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu_{\mathsf{new}}}\\![\mathsf{dy}]}(\mathcal{W}_{\mathsf{new}})$
$\displaystyle\subseteq\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$
(12)
$\displaystyle\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})\cap\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu_{\mathsf{new}}}\\![\mathsf{dy}]}(\mathcal{W}_{\mathsf{new}})$
$\displaystyle\subseteq\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W}_{\mathsf{new}}).$

Inclusion (11) is a consequence of the Inclusions (13) and (14), which allow
us to invoke the faithfulness of $\mathcal{W}$:

(13)
$\displaystyle\mathsf{Acc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W}_{\mathsf{new}})$
$\displaystyle\subseteq\mathsf{Acc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$
(14)
$\displaystyle\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu_{\mathsf{new}}}\\![\mathsf{dy}]}(\mathcal{W}_{\mathsf{new}})$
$\displaystyle\subseteq\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{W})\
.$

Inclusion (13) holds, as we only change an intermediate valuation from
$\mathcal{W}$ to $\mathcal{W}_{\mathsf{new}}$, and acceptance does not take
the intermediate valuations into account. To see that we only change an
intermediate valuation, note that also $\mathcal{W}$ is zero-reaching by
faithfulness. Inclusion (14) holds with the same argument as Property (c)
above.

For Inclusion (12), let
$\rho\in\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})\cap\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu_{\mathsf{new}}}\\![\mathsf{dy}]}(\mathcal{W}_{\mathsf{new}})$.
Consider the moment the run enters or exits the precovering graph of interest,
and the counter $j$ whose value changes from $\omega$ in $\mathcal{W}$ to
$0\leq a<\mu_{\mathsf{new}}$ in $\mathcal{W}_{\mathsf{new}}$. By the
intermediate acceptance
$\rho\in\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$, the run induces
a solution to $\mathsf{Char}_{\mathsf{dy}}(\mathcal{W})$. The consequence is
that, at this moment in the run, counter $j$ has a value $b\in
A_{\mathsf{dy}}\subseteq\mathbb{N}$. Moreover $b<\mu_{\mathsf{new}}$, because
we chose $l$ larger than all values in $A_{\mathsf{dy}}$. With
$\rho\in\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu_{\mathsf{new}}}\\![\mathsf{dy}]}(\mathcal{W}_{\mathsf{new}})$,
we additionally get $b\equiv a\mathop{\text{ mod }}\mu_{\mathsf{new}}$ . Lemma
8.2 applies and shows $a=b$.

For the remaining precovering graphs, and the precovering graph $G$ but a
counter different from $j$, we show intermediate acceptance as follows. Let
$\mathcal{W}$ carry value $b\in\mathbb{N}$ at the moment of interest. Note
that $b<\mu_{\mathsf{new}}$ by the choice of $l$, namely larger than all
values in $\mathcal{W}$. In
$\mathcal{W}_{\mathsf{new}}=(\mathcal{S},\mu_{\mathsf{new}})$, we find a value
$b^{\prime}$ at this moment. As $0\leq\mathcal{S}<\mu_{\mathsf{new}}$, we know
$0\leq b^{\prime}<\mu_{\mathsf{new}}$. We have
$\rho\in\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})\cap\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu_{\mathsf{new}}}\\![\mathsf{dy}]}(\mathcal{W}_{\mathsf{new}})$.
We are thus sure to reach $b$ and reach $b^{\prime}$ modulo
$\mu_{\mathsf{new}}$. This allows us to conclude $b\equiv
b^{\prime}\mathop{\text{ mod }}\mu_{\mathsf{new}}$ with $0\leq
b,b^{\prime}<\mu_{\mathsf{new}}$. Lemma 8.2 applies and yields the desired
$b=b^{\prime}$.

We analyze the complexity. Every counter in every valuation may be replaced by
$\mu_{\mathsf{new}}=l\cdot\mu$ many values. This limits the number of
generated DMGTS to ${\mu_{\mathsf{new}}}^{|{\mathcal{W}}|}$. The DMGTS have a
maximal size of $\mu_{\mathsf{new}}\cdot|{\mathcal{W}}|$. As we argued in the
case $\mathsf{sd}=\mathsf{sj}$, the value $l$ itself is of size elementary in
$|{\mathcal{W}}|$. We conclude that the whole procedure takes elementary
resources. ∎

###  8.2. Reasoning Locally about Faithfulness

In Case (i), we modified the entry and exit valuations of every precovering
graph in a DMGTS. In the remaining two cases, we will decompose a single
precovering graph, in a way that is independent of the context. We now develop
techniques that allow us to reason locally about the one precovering graph,
and lift the results to the overall DMGTS. The focus is on faithfulness.

An _MGTS context_ is an MGTS in which a distinguished variable $\bullet$
occurs precisely once:

$\displaystyle\mathcal{C}[\bullet]\;\;::=\;\;\bullet\;\;\mid\;\;\mathcal{C}[\bullet].\mathit{up}.\mathcal{W}\;\;\mid\;\;\mathcal{W}.\mathit{up}.\mathcal{C}[\bullet]\
.$

We write $\mathcal{C}[\mathcal{W}]$ for the MGTS that is obtained by replacing
$\bullet$ with the MGTS $\mathcal{W}$. When $\mathcal{W}$ is a DMGTS
$(\mathcal{S},\mu)$, we also write $\mathcal{C}[\mathcal{W}]$ to mean
$(\mathcal{C}[\mathcal{S}],\mu)$. A first observation is that the well-founded
relation is preserved when comparable MGTS and DMGTS are inserted into
contexts, $\mathcal{W}_{1}\preceq\mathcal{W}_{2}$ implies
$\mathcal{C}[\mathcal{W}_{1}]\preceq\mathcal{C}[\mathcal{W}_{2}]$.

With contexts at hand, the remaining cases we will start from
$(\mathcal{C}[G],\mu)$ and decompose $(G,\mu)$ into sets of DMGTS $U$ and $V$.
The sets needed for Lemma 8.1 are then
$X=\mathcal{C}[U]=\\{\mathcal{C}[\mathcal{S}]\mid\mathcal{S}\in U\\}$ resp.
$Y=\mathcal{C}[V]$. We also have $Y=\emptyset$ in one case. To show the
faithfulness of these DMGTS, we use the following arguments.

We define a relation called _consistent specialization_ between DMGTS. We use
an induction on the structure of the underlying MGTS. In the base case,
$(\mathcal{S},\mu)$ is a consistent specialization of $(G,\mu)$ if the
following two conditions hold.

  * (1)

We have $\mathcal{S}.c_{\mathsf{in}}\leq_{\omega}G.c_{\mathsf{in}}$,
$\mathcal{S}.c_{\mathsf{out}}\leq_{\omega}G.c_{\mathsf{out}}$, and for all
runs $\rho\in\mathsf{Runs}_{\mathbb{Z}}(\mathcal{S})$ there is
$\sigma\in\mathsf{Runs}_{\mathbb{Z}}(G)$ with $\sigma\approx\rho$.

  * (2)

For all
$\rho\in\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{S})$
with $\rho[\mathsf{first}][\mathsf{dy}]\leq_{\omega}G.c_{\mathsf{in}}$ and
$\rho[\mathsf{last}][\mathsf{dy}]\leq_{\omega}G.c_{\mathsf{out}}$, we have
$\rho\in\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W})$.

In the inductive step, if $\mathcal{S}_{1}$ is a consistent specialization of
$\mathcal{S}_{2}$, then $\mathcal{C}[\mathcal{S}_{1}]$ is a consistent
specialization of $\mathcal{C}[\mathcal{S}_{2}]$. Note that $\mu$ has to
coincide for DMGTS that are related by consistent specialization.

Condition (1) expects that every run through $\mathcal{S}$ can be mimicked by
$G$. With this, consistent specializations have smaller languages. Together,
Conditions (1) and (2) show that consistent specializations preserve
faithfulness.

###### Lemma 8.4.

Let $\mathcal{W}_{1}$ be a consistent specialization of $\mathcal{W}_{2}$.
Then $L_{\mathsf{sj}}(\mathcal{W}_{1})\subseteq
L_{\mathsf{sj}}(\mathcal{W}_{2})$ holds. Moreover, if $\mathcal{W}_{2}$ is
faithful, so is $\mathcal{W}_{1}$.

We give an intuition as to why the decompositions for the Cases (ii) and (iii)
will guarantee Condition (2). The decompositions unroll the precovering graph
$G$ into DMGTS. The intermediate counter valuations of these DMGTS correspond
to the consistent assignment in $G$. The precovering graph only admits runs
that respects the consistent assignment. As a consequence, every run through
the new DMGTS will satisfy intermediate acceptance.

###  8.3. Case (ii)

This is the case where an edge $e$ belongs to a precovering graph $G$, and
hence can be taken in loops, but the characteristic equations for the DMGTS
$(\mathcal{C}[G],\mu)$ impose an upper bound $l\in\mathbb{N}$ on the number of
times the edge can be taken. The decomposition unrolls $G$ into MGTS where
every copy of $e$ leads to a new precovering graph. The MGTS thus count the
number of times $e$ is taken.

The DMGTS in the set $U$ only admit runs where $e$ is taken at most $l$ times.
As $x[e]$ is not in the support, the precovering graphs we obtain by excluding
$e$ have a smaller dimension, and hence the well-founded preorder decreases.

The DMGTS in $V$ count until $e$ has been taken $l+1$ times, and then admit
all edges while returning to the former root. Any solution to the
characteristic equations can be translated into a solution $s$ for the
characteristic equations of $(G,\mu)$ with $s[e]>l$. When the elements of $V$
are inserted into the context, this makes the characteristic equation
infeasible as the edge count is too high.

Lemma 8.5 lists the guarantees. It is [18, Proposition 3.3] with information
about faithfulness and the DMGTS in $V$ added.

###### Lemma 8.5.

Let $(G,\mu)$ contain the edge $e$, let
$\mathsf{sd}\in\\{\mathsf{sj},\mathsf{dy}\\}$, and let $\mathcal{C}[\bullet]$
be a context with
$x[e]\not\in\mathsf{supp}(\mathsf{Char}_{\mathsf{sd}}(\mathcal{C}[G],\mu))$.
Using resources elementary in $|{(\mathcal{C}[G],\mu)}|$, we can compute sets
$U$ and $V$ of consistent specializations of $(G,\mu)$, where

  * •

for all $\mathcal{S}\in U$, we have $\mathcal{S}<_{\mathsf{rnk}}(G,\mu)$,

  * •

for all $\rho\in\mathsf{IAcc}_{\mathsf{sj}}(G,\mu)$ there is
$\sigma\in\mathsf{IAcc}_{\mathsf{sj}}(U\cup V)$ with $\rho\approx\sigma$,

  * •

for all $\mathcal{T}\in V$, we have that
$\mathsf{Char}_{\mathsf{sd}}(\mathcal{C}[\mathcal{T}])$ is infeasible.

We define the decomposition $(X,Y)=\textsf{dec}(\mathcal{W})$ for the faithful
DMGTS $\mathcal{W}=(\mathcal{C}[G],\mu)$ whose precovering graph $G$ contains
an edge $e$ with
$x[e]\not\in\mathsf{supp}(\mathsf{Char}_{\mathsf{sd}}(\mathcal{W}))$. With
Lemma 8.5, we compute the sets $U$ and $V$. If $\mathsf{sd}=\mathsf{sj}$, we
set $X=\mathcal{C}[U]$ and $Y=\emptyset$. If $\mathsf{sd}=\mathsf{dy}$, we set
$X=\mathcal{C}[U]$ and $Y=\mathcal{C}[V]$. This should be read as follows. If
the subject VASS can only execute the edge a bounded number of times, we use
the usual decomposition and do not create elements in $Y$. If the Dyck-side
can only execute the edge a bounded number of times, we split the runs of the
subject VASS. The set $X$ contains the runs where the edge is bounded. The set
$Y$ contains the runs where the edge may occur more often, and we have the
guarantee to be separable from the Dyck language by Lemma 6.2.

###### Proof.

We prove the properties promised by Lemma 8.1. For (a), we note that not only
the DMGTS in $X$ but also the ones in $Y$ are faithful by Lemmas 8.5 and 8.4.
The well-founded relation decreases by Lemma 8.5. It is stable under forming
contexts as noted above. For (b), if $\mathsf{sd}=\mathsf{sj}$ there is
nothing to do, because $Y=\emptyset$. If $\mathsf{sd}=\mathsf{dy}$, Lemma 8.5
already yields the infeasibility of
$\mathsf{Char}_{\mathsf{dy}}(\mathcal{C}[\mathcal{T}])$ for all
$\mathcal{T}\in V$. With Lemma 6.2, this implies the desired
$L_{\mathsf{sj}}(\mathcal{C}[\mathcal{T}])\mid D_{n}$.

For (c), we have $L_{\mathsf{sj}}(X\cup Y)\subseteq
L_{\mathsf{sj}}(\mathcal{W})$ by Lemmas 8.5 and 8.4. For reverse inclusion,
consider a word $\lambda(\rho)$ with
$\rho\in\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{W})$. As
$\mathcal{W}=(\mathcal{C}[G],\mu)$, we have $\rho=\rho_{0}.\rho_{1}.\rho_{2}$,
where $\rho_{1}$ is the part of the run through $G$. Intermediate acceptance
propagates down to the components of the DMGTS, which yields
$\rho_{1}\in\mathsf{IAcc}_{\mathsf{sj}}(G,\mu)$. By Lemma 8.5, there are
$\mathcal{S}\in U\cup V$ and
$\sigma\in\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{S})$ with
$\rho_{1}\approx\sigma$. The equivalence among runs guarantees that the labels
and counter values coincide, only the visited nodes may differ. Hence, we have
$\rho_{0}.\sigma.\rho_{2}\in\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{C}[\mathcal{S}])$
and
$\lambda(\rho_{0}.\sigma.\rho_{2})=\lambda(\rho_{0}.\rho_{1}.\rho_{2})=\lambda(\rho)$.
If $\mathsf{sd}=\mathsf{dy}$, we are done. If $\mathsf{sd}=\mathsf{sj}$, we
must additionally show $\mathcal{S}\not\in V$, because the MGTS in $V$ are
dropped by the construction. We reason with infeasibility, like we did for
(b). ∎

###  8.4. Case (iii)

This is the case where a precovering graph $G$ does not have a covering
sequence to arbitrarily increase or decrease the values of $\omega$-decorated
counters. As $\mathsf{CS}_{\mathsf{down}}(G)$ is defined via
$\mathsf{CS}_{\mathsf{up}}(G)$, we focus on
$\mathsf{CS}_{\mathsf{up}}(G)=\emptyset$. We follow the construction by Leroux
and Schmitz [24], which employs a Rackoff argument [26], rather than the one
by Lambert [18], which works with coverability graphs [13].

For each $\mathit{j}\in\mathsf{sj}\cup\mathsf{dy}$ that is decorated by
$\omega$ and has $G.c_{\mathsf{in}}[\mathit{j}]\in\mathbb{N}$, we unroll the
precovering graph into a DMGTS that tracks $\mathit{j}$ up to a bound $B$. The
bound $B$ is of size doubly exponential in $|{G}|$. By the same Rackoff
argument as in [24], we conclude that this captures all words in
$L_{\mathsf{sj}}(G)$, because the opposite would imply
$\mathsf{CS}_{\mathsf{up}}(G)\neq\emptyset$. The graph has one peculiarity
compared to [24]. Assume a Dyck counter has not yet exceeded $B$ and becomes
negative. Then we enter a sink node in which we enable all transitions.

The DMGTS in $U$ capture the runs that do not enter the sink and reach
$G.c_{\mathsf{out}}$. Since cycles cannot change counter $\mathit{j}$, the
dimension of the vector space decreases for each precovering graph. This
reduces the well-founded preorder. The details are in the appendix.

The DMGTS in $V$ capture the runs that enter the sink and the runs that end in
a valuation different from $G.c_{\mathsf{out}}$. In both cases, the
characteristic equations for $\mathsf{dy}$ become infeasible. Indeed, when a
Dyck counter becomes negative, the construction forces us to leave a
precovering graph towards the sink. But then we fail to satisfy the non-
negativity requirement for entering the sink.

Lemma 8.6 formalizes the guarantees given by the construction. It is based on
[18, Propositions 3.4 and 3.5].

###### Lemma 8.6.

Let $(G,\mu)$ have $\mathsf{CS}_{\mathsf{up}}(G)=\emptyset$ or
$\mathsf{CS}_{\mathsf{down}}(G)=\emptyset$. Using resources elementary in
$|{(G,\mu)}|$, we can compute sets $U$ and $V$ of consistent specializations
of $(G,\mu)$, where

  * •

for all $\mathcal{S}\in U$, we have $\mathcal{S}<_{\mathsf{rnk}}(G,\mu)$,

  * •

for all $\rho\in\mathsf{IAcc}_{\mathsf{sj}}(G,\mu)$ there is
$\sigma\in\mathsf{IAcc}_{\mathsf{sj}}(U\cup V)$ with $\rho\approx\sigma$,

  * •

for all $\mathcal{T}\in V$, we have that
$\mathsf{Char}_{\mathsf{dy}}(\mathcal{T})$ is infeasible.

We explain the role of the DMGTS in $V$ that enter the sink as a Dyck counter
becomes negative. How can they help with the second property, if the
requirement there is that the Dyck counters stay non-negative? The observation
is that intermediate acceptance modulo $\mu$ satisfies a monotonicity
property: if
$\rho\in\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{T})$
then
$\rho+k\cdot\mu\in\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{T})$.
Here, we use $\rho+k\cdot\mu$ to denote the run obtained from $\rho$ by
raising the values of all counters in all configurations by $k\cdot\mu$ with
$k\in\mathbb{N}$. A consequence of monotonicity is that even though a run
starting from small values has to enter the sink due to a negative counter,
this negativity will disappear in properly scaled runs, and they will still
take the same transitions. The set $V$ makes sure we do not miss the scaled
runs.

We define $(X,Y)=\textsf{dec}(\mathcal{W})$ for
$\mathcal{W}=(\mathcal{C}[G],\mu)$ faithful with
$\mathsf{CS}_{\mathsf{up}}(G)=\emptyset$ or
$\mathsf{CS}_{\mathsf{down}}(G)=\emptyset$. Lemma 8.6 yields sets $U$ and $V$
of consistent specializations. We set $X=\mathcal{C}[U]$ and
$Y=\mathcal{C}[V]$. The requirements of Lemma 8.1 are derived like in Case
(ii).

## References

  * [1] P. Baumann, R. Meyer, and G. Zetzsche.  Regular separability in Büchi VASS.  In STACS, volume 254 of LIPIcs, pages 9:1–9:19, 2023.
  * [2] J. R. Büchi.  On a decision method in restricted second order arithmetic.  In International Congress on Logic, Method, and Philosophy of Science, pages 1–12. Stanford University Press, 1962.
  * [3] L. Clemente, W Czerwiński, S. Lasota, and C. Paperman.  Regular separability of Parikh automata.  In ICALP, volume 80 of LIPIcs, pages 117:1–117:13. Dagstuhl, 2017.
  * [4] L. Clemente, W. Czerwiński, 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.
  * [5] 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.
  * [6] F. G. Commoner, A. W. Holt, S. Even, and A. Pnueli.  Marked directed graphs.  JCSS, 5(5):511–523, 1971.
  * [7] W. Czerwiński and S. Lasota.  Regular separability of one counter automata.  In LICS, pages 1–12. IEEE, 2017.
  * [8] W. Czerwiński, 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.
  * [9] W. Czerwiński and Ł. Orlikowski.  Reachability in vector addition systems is Ackermann-complete.  In FOCS, pages 1229–1240. IEEE, 2021.
  * [10] W. Czerwiński and G. Zetzsche.  An approach to regular separability in vector addition systems.  In LICS, pages 341–354. ACM, 2020.
  * [11] S. Demri.  On selective unboundedness of VASS.  JCSS, 79(5):689–713, 2013.
  * [12] H. J. Genrich and K. Lautenbach.  Synchronisationsgraphen.  Acta Informatica, 2:143–161, 1973.
  * [13] R. M. Karp and R. E. Miller.  Parallel program schemata.  JCSS, 3(2):147–195, 1969.
  * [14] E. Keskin and R. Meyer.  Separability and non-determinizability of WSTS.  In CONCUR, volume 279 of LIPIcs, pages 8:1–8:17. Dagstuhl, 2023.
  * [15] C. Köcher and G. Zetzsche.  Regular separators for VASS coverability languages.  In FSTTCS, volume 284 of LIPIcs, pages 15:1–15:19. Dagstuhl, 2023.
  * [16] E. Kopczynski.  Invisible pushdown languages.  In LICS, pages 867–872. ACM, 2016.
  * [17] S. R. Kosaraju.  Decidability of reachability in vector addition systems (preliminary version).  In STOC, pages 267–281. ACM, 1982.
  * [18] J.-L. Lambert.  A structure to decide reachability in Petri nets.  TCS, 99(1):79–104, 1992.
  * [19] S. Lasota.  Improved Ackermannian lower bound for the Petri nets reachability problem.  In STACS, volume 219 of LIPIcs, pages 46:1–46:15. Dagstuhl, 2022.
  * [20] J. Leroux.  The general vector addition system reachability problem by Presburger inductive invariants.  In LICS, pages 4–13. IEEE, 2009.
  * [21] J. Leroux.  Vector addition system reachability problem: a short self-contained proof.  In POPL, pages 307–316. ACM, 2011.
  * [22] J. Leroux.  The reachability problem for Petri nets is not primitive recursive.  In FOCS, pages 1241–1252. IEEE, 2021.
  * [23] J. Leroux and S. Schmitz.  Demystifying reachability in vector addition systems.  In LICS, pages 56–67. IEEE, 2015.
  * [24] J. Leroux and S. Schmitz.  Reachability in vector addition systems is primitive-recursive in fixed dimension.  In LICS. IEEE, 2019.
  * [25] E. W. Mayr.  An algorithm for the general Petri net reachability problem.  In STOC, pages 238–246. ACM, 1981.
  * [26] C. Rackoff.  The covering and boundedness problems for vector addition systems.  TCS, 6(2):223–231, 1978.
  * [27] G. S. Sacerdote and R. L. Tenney.  The decidability of the reachability problem for vector addition systems (preliminary version).  In STOC, pages 61–76. ACM, 1977.
  * [28] S. Schmitz.  Complexity hierarchies beyond elementary.  ACM TOCT, 8(1):3:1–3:36, 2016.
  * [29] S. Schmitz.  Algorithmic Complexity of Well-Quasi-Orders.  Habilitation à diriger des recherches, ENS-Paris-Saclay, 2017.

##  Appendix A Appendix: DMGTS

###### Proof of Lemma 5.1.

Let $w\in L_{\mathsf{dy}}(\mathcal{W})$. Then there is a run $\rho$ in
$\mathcal{W}$ labeled by $\lambda(\rho)=w$ that remains non-negative and that
is accepting on $\mathsf{dy}$. By the definition of DMGTS, the effects of
letters on the counters in $\mathsf{dy}$ agree with the effects that these
letters have in the VASS $\mathcal{D}_{n}$. This allows us to construct a run
$\rho^{\prime}\in\mathsf{Acc}_{\mathbb{N},\leq_{\omega}}(\mathcal{D}_{n})$
that has the same counter valuations and updates. Hence, we have $w\in D_{n}$.
∎

##  Appendix B Appendix: The Decomposition

In this section, we provide the missing proofs from Section 8, followed by the
analysis the complexity of the algorithm from the proof of Lemma 6.1. We
preface the missing proofs with the adapting the Rackoff-styled observations
in [24] to our needs.

As we mention in the main paper, our decomposition is based on the
decomposition by Leroux et al. in [24]. For this reason, many proofs we
feature are adaptations of the ones in [24]. Because our setting differs from
that of [24] non-trivially, we adapt the proofs to our setting instead of
using them as black-boxes. The biggest difference is this. DMGTS define two
languages, one per counter set $\mathsf{sj}$ and $\mathsf{dy}$, where the
language associated with one side does not track the constraints on the other
side. Additionally, we need the faithfulness invariant, which is not needed in
[24].

###  B.1. Preliminary Proofs

As alluded to, we first show the following observation which is an adaptation
of Lemma A.1 from the appendix of [24]. For a set of counters $J$ our version
of the observation states the following. If we have an integer run, where each
counter (i) exceeds some doubly exponential bound in $C$, the number of
counters $d$, and the largest effect of a transition $l$ along the run and
(ii) remains positive until this happens, then there is an $J$-run that
reaches a value that covers $C$ in all counters $i\in J$. Our version of the
observation differs from the one used in [24, Lemma A.1], in that we allow
counters to become negative after exceeding the bound. We recall the proof

###### Lemma B.1.

Let $G$ be a precovering graph with the largest transition effect $l$, $C\geq
2$, $J\subseteq\mathsf{sj}\cup\mathsf{dy}$, and
$\rho\in\mathsf{Runs}_{\mathbb{Z}}(G)$ with

$\rho=(p_{0},c_{0})e_{0}\ldots e_{k-1}(p_{k},c_{k}).$

If for all $\mathit{j}\in J$, there is an $i\leq k$ with
$c_{i}[\mathit{j}]\geq(|{G.V}|\cdot l\cdot C)^{|{J}|+1!}$, and
$c_{i^{\prime}}[\mathit{j}]\geq 0$ for all $i^{\prime}\leq i$, then there is a
run $\sigma\in\mathsf{Runs}_{J}(G)$ of size at most $(|{G.V}|\cdot l\cdot
C)^{|{J}|+1!}$ where $\sigma[\mathsf{last}]=(p_{k},c)$,
$\sigma[\mathsf{first}]=(p_{0},c_{0})$, and $c[\mathit{j}]\geq C$ for all
$\mathit{j}\in J$.

###### Proof of Lemma B.1.

Let $G$, $J$, $\rho$, and $l$ be defined as stated in the premise of the
lemma, and $\rho$ additionally the shortest run with this property. First, we
define $\alpha_{i}$ for $i\leq|{\mathsf{sj}\cup\mathsf{dy}}|$ inductively. We
define $\alpha_{0}=|{G.V}|$, and
$\alpha_{i}=|{G.V}|\cdot(l\cdot\alpha_{i-1}+C)^{i}+\alpha_{i-1}$ for $i>1$.
Over approximating, we get

$\alpha_{i}\leq|{G.V}|\cdot(l\cdot\alpha_{i-1}\cdot
C)^{i}+\alpha_{i-1}\leq(|{G.V}|\cdot l\cdot\alpha_{i-1}\cdot C)^{i+1}.$

We can apply the inductive definition to get

$\alpha_{i}\leq(|{G.V}|\cdot l\cdot C)^{i+1!}$

Our proof is by induction on $|{J}|$. For the base case, we take
$J=\emptyset$. Then, both the premise and the requirements become trivial.
Since there is a run $\rho$ that starts from $p_{0}$ and ends at $p_{k}$, we
can find a run of size at most $|{G.V}|=\alpha_{0}$ between these nodes.

For the inductive case, let Lemma B.1 hold for all $J^{\prime}\subset J$. The
premise of the lemma gives us $i_{\mathit{j}}\leq k$ for each $\mathit{j}\in
J$ where $c_{i_{\mathit{j}}}[\mathit{j}]\geq\alpha_{|{J}|}\geq
l\cdot\alpha_{|{J}|-1}+C$ and $c_{i^{\prime}}[\mathit{j}]\geq 0$ for all
$i^{\prime}\leq i_{\mathit{j}}$. Wlog. assume $i_{\mathit{j}}$ to be minimal
for each $\mathit{j}\in J$. Let $J^{\prime}$ be the set of counters
$\mathit{j}$ that minimize $i_{\mathit{j}}$. Fix some $\mathit{j}\in
J^{\prime}$. The remainder of the run
$(p_{i_{\mathit{j}}},c_{i_{\mathit{j}}})\ldots(p_{k},c_{k})$ satisfies the
premise of the lemma for $J\setminus J^{\prime}$. Since $i_{\mathit{j}}$ is
minimal and $\rho$ is a $J$-run, we know that for all $\mathit{j}\in J$ and
$i^{\prime}<i_{\mathit{j}}$,
$c_{i^{\prime}}[\mathit{j}]<l\cdot\alpha_{|{J}|-1}+C$. Then, each counter in
$J$ can have at most $l\cdot\alpha_{|{J}|-1}+C$ different values. We have
$i_{\mathit{j}}<|{G.V}|\cdot(l\cdot\alpha_{|{J}|-1}+C)^{|{J}|}$ since $\rho$
is minimal and we could eliminate a loop from $\rho$ if this were to not hold.
Denote the run up to this point as $\rho_{0}$. Observe that the remaining run
$(p_{i_{\mathit{j}}},c_{i_{\mathit{j}}})\ldots(p_{k},c_{k})$ fulfills the
premise of the lemma for the counters $J\setminus J^{\prime}$: for all $n\in
J\setminus J^{\prime}$, we know that there is a $i_{\mathit{j}}<i_{m}\leq k$
where $c_{i_{m}}[m]\geq\alpha_{|{J}|}(C)\geq\alpha_{|{J\setminus
J^{\prime}}|}(C)$ and $c_{i^{\prime}}[m]\geq 0$ for all $i^{\prime}\leq
i_{m}$. Then the induction hypothesis applies to show that there is a
$J\setminus J^{\prime}$-run $\sigma_{1}$ from
$(p_{i_{\mathit{j}}},c_{i_{\mathit{j}}})$ of length at most
$\alpha_{|{J\setminus J^{\prime}}|}(C)$ that reaches $(p_{k},c)$ with
$c[\mathit{j}]\geq C$ for all $m\in J\setminus J^{\prime}$. Let
$\sigma=\ldots(p_{k},c)$ be the run obtained by following up $\rho_{0}$ by
$\sigma_{1}$. We claim that $\sigma$ is a $J$-run with $c[n]\geq C$. This is
already clear for all $n\in J\setminus J^{\prime}$. For $n\in J^{\prime}$, we
observe that $\rho_{0}$ is by definition positive on these counters, and
$c_{i_{n}}[n]\geq l\cdot\alpha_{|{J}|-1}+C\geq l\cdot\alpha_{|{J\setminus
J^{\prime}}|}+C$. Then, since $\sigma$ takes at most $\alpha_{|{J\setminus
J^{\prime}}|}$ transitions, the counter $n$ remains above $C\geq 0$ for all
prefixes of $\sigma_{1}$. This concludes the proof. ∎

We now show Lemma 8.4. We break down its conclusions into two proofs, one for
the implied inclusion and one for the implied faithfulness. In the following
proofs, we write $\mathcal{W}_{0}\leq_{cs}\mathcal{W}_{1}$ mean that
$\mathcal{W}_{0}$ is a consistent specialization of $\mathcal{W}_{1}$. We also
write $(p,c).c$ for a configuration $(p,c)$ to denote the counter valuation of
the configuration.

###### Proof Sketch of Lemma 8.4, Inclusion.

The proof is by structural induction over the proof tree for $\leq_{cs}$. By
this we refer to a tree labeled by pairs of DMGTS
$(\mathcal{W}_{0},\mathcal{W}_{1})$ where (i) the node is a leaf where the
properties (1) and (2) have been applied to show
$\mathcal{W}_{0}\leq_{cs}\mathcal{W}_{1}$ or (ii) the node is not a leaf and
the inductive case is used to show $\mathcal{W}_{0}\leq_{cs}\mathcal{W}_{1}$
by inserting the relation shown in its successor into a context. Our inductive
invariant is stronger than the conclusion of Lemma 8.4: If
$\mathcal{W}_{0}\leq_{cs}\mathcal{W}_{1}$, then for all
$\rho\in\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{W}_{0})$, there is a
$\sigma\in\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{W}_{1})$ with
$\rho\approx\sigma$. Because $\approx$ preserves labels, this clearly implies
the desired inclusion. For the base case, we have $\mathcal{W}_{1}=(G,\mu)$
for some precovering graph $G$, where (1) and (2) hold to show
$\mathcal{W}_{0}\leq_{cs}\mathcal{W}_{1}$. Let
$\rho\in\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{W}_{0})$. We know
$\rho[\mathsf{first}].c[\mathsf{sj}]\leq_{\omega}\mathcal{W}_{0}.c_{\mathsf{in}}[\mathsf{sj}]$,
$\rho[\mathsf{last}].c[\mathsf{sj}]\leq_{\omega}\mathcal{W}_{0}.c_{\mathsf{out}}[\mathsf{sj}]$,
$\rho[\mathsf{first}].c[\mathsf{dy}]\sqsubseteq_{\omega}^{\mu}\mathcal{W}_{0}.c_{\mathsf{in}}[\mathsf{dy}]$,
and
$\rho[\mathsf{last}].c[\mathsf{dy}]\sqsubseteq_{\omega}^{\mu}\mathcal{W}_{0}.c_{\mathsf{out}}[\mathsf{dy}]$.
The second part of (1) tells us that there is a
$\sigma\in\mathsf{Runs}_{\mathbb{Z}}(\mathcal{W}_{1})$ with
$\sigma\approx\rho$. The relation $\approx$ keeps the counter valuations
intact. So positivity on $\mathsf{sj}$ counters is kept, and the constraints
are kept:

$\displaystyle\sigma[\mathsf{first}].c[\mathsf{sj}]$
$\displaystyle\leq_{\omega}\mathcal{W}_{0}.c_{\mathsf{in}}[\mathsf{sj}]\leq_{\omega}\mathcal{W}_{1}.c_{\mathsf{in}}[\mathsf{sj}]$
$\displaystyle\sigma[\mathsf{last}].c[\mathsf{sj}]$
$\displaystyle\leq_{\omega}\mathcal{W}_{0}.c_{\mathsf{out}}[\mathsf{sj}]\leq_{\omega}\mathcal{W}_{1}.c_{\mathsf{out}}[\mathsf{sj}]$
$\displaystyle\sigma[\mathsf{first}].c[\mathsf{dy}]$
$\displaystyle\sqsubseteq_{\omega}^{\mu}\mathcal{W}_{0}.c_{\mathsf{in}}[\mathsf{dy}]\leq_{\omega}\mathcal{W}_{1}.c_{\mathsf{in}}[\mathsf{dy}]$
$\displaystyle\sigma[\mathsf{last}].c[\mathsf{dy}]$
$\displaystyle\sqsubseteq_{\omega}^{\mu}\mathcal{W}_{0}.c_{\mathsf{out}}[\mathsf{dy}]\leq_{\omega}\mathcal{W}_{1}.c_{\mathsf{out}}[\mathsf{dy}]$

At each line, the first inequality follows from
$\rho\in\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{W}_{0})$, and the fact that
$\approx$ keeps the counter valuations intact. The second inequality follows
from the first part of (1) that constraints the valuations of
$\mathcal{S}_{0}$ with respect to $G$. For the inductive case, let
$\mathcal{W}_{i}=\mathcal{C}[\mathcal{W}_{i}^{\prime}]$ for some DMGTS
$\mathcal{W}_{i}^{\prime}$ for each $i\in\\{0,1\\}$, where
$\mathcal{W}_{0}^{\prime}\leq_{cs}\mathcal{W}_{1}^{\prime}$. Let
$\rho\in\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{W}_{0})$. We break this run down
into $\rho=\rho_{0}.\rho_{1}.\rho_{2}$ where $\rho_{1}$ is the part of the run
in $\mathcal{W}_{0}^{\prime}$, and $\rho_{0}.\bullet.\rho_{2}$ the remaining
part in the outer context $\mathcal{C}[\bullet]$. Compositionality of
$\mathsf{IAcc}_{\mathsf{sj}}(-)$ tells us
$\rho_{1}\in\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{W}_{0}^{\prime})$. Using the
induction hypothesis, we get a run
$\sigma_{1}\in\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{W}_{1}^{\prime})$ with
$\sigma_{1}\approx\rho_{1}$. Using compositionality and the fact that
$\mathcal{C}[\bullet]$ is the same between $\mathcal{W}_{0}$ and
$\mathcal{W}_{1}$, we deduce
$\sigma=\rho_{0}.\sigma_{1}.\rho_{2}\in\mathsf{IAcc}_{\mathsf{sj}}(\mathcal{W}_{1})$.
Since $\rho_{1}\approx\sigma_{1}$, it is clear that $\rho_{0}\approx\rho_{1}$.
This concludes the proof. ∎

###### Proof Sketch of Lemma 8.4, Faithfulness.

We do a structural induction similarly to the proof of Lemma 8.4. We maintain
two invariants. If $\mathcal{W}_{0}\leq_{cs}\mathcal{W}_{1}$, then

  * (a)

For all
$\rho\in\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{W}_{0})$,
there is $\sigma\approx\rho$ with
$\sigma\in\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{W}_{1})$.

  * (b)

If $\mathcal{W}_{1}$ is faithful, for all runs
$\rho\in\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{W}_{0})$
with
$\rho[\mathsf{first}].c[\mathsf{dy}]\leq_{\omega}\mathcal{W}_{1}.c_{\mathsf{in}}[\mathsf{dy}]$,
and
$\rho[\mathsf{last}].c[\mathsf{dy}]\leq_{\omega}\mathcal{W}_{1}.c_{\mathsf{out}}[\mathsf{dy}]$,
we have $\rho\in\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W}_{0})$.

We also use the fact that
$\mathcal{W}_{0}.c_{\mathsf{in}}\leq_{\omega}\mathcal{W}_{1}.c_{\mathsf{in}}$
and
$\mathcal{W}_{0}.c_{\mathsf{out}}\leq_{\omega}\mathcal{W}_{1}.c_{\mathsf{in}}$,
which can be shown by standard induction. This fact, applied with (b), shows
the implication from the faithfulness of $\mathcal{W}_{1}$ to the faithfulness
of $\mathcal{W}_{0}$, in Lemma 8.4. For the base case, let
$\mathcal{W}_{1}=(G,\mu)$ for some precovering graph $G$, where (1) and (2)
show $\mathcal{W}_{0}\leq_{cs}\mathcal{W}_{1}$. Let
$\rho\in\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{W}_{0})$.
Because of (1), we know that there is a
$\sigma\in\mathsf{Runs}_{\mathbb{Z}}(G)$ with $\sigma\approx\rho$. Since (1)
tells us that $\mathcal{W}_{0}.c_{\mathsf{in}}$ and
$\mathcal{W}_{0}.c_{\mathsf{out}}$ are stricter than
$\mathcal{W}_{1}.c_{\mathsf{in}}$ and $\mathcal{W}_{1}.c_{\mathsf{out}}$, and
$G$ does not have intermediate valuations,
$\sigma\in\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{W}_{1})$.
This shows (a). Invariant (b) is just (2). This concludes the base case. For
the inductive case, let
$\mathcal{W}_{0}=\mathcal{C}[\mathcal{W}_{0}^{\prime}]$ and
$\mathcal{W}_{1}=\mathcal{C}[\mathcal{W}_{1}^{\prime}]$ with
$\mathcal{W}_{0}^{\prime}\leq_{cs}\mathcal{W}_{1}^{\prime}$. Let
$\rho\in\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{W}_{0})$.
We have $\rho=\rho_{0}.\rho_{1}.\rho_{2}$ where $\rho_{1}$ is the part of the
run in $\mathcal{W}_{0}^{\prime}$, and $\rho_{0}.\bullet.\rho_{2}$ is the part
of the run in the outer context $\mathcal{C}[\bullet]$. For (a), we invoke the
induction hypothesis on $\rho_{1}$ and use compositionality, same as in the
proof of Lemma 8.4, Inclusion. For (b), let $\mathcal{W}_{1}$ be faithful, let
$\rho\in\mathsf{Runs}_{\mathbb{Z}}(\mathcal{W}_{0})$,
$\rho[\mathsf{first}].c[\mathsf{dy}]\leq_{\omega}\mathcal{W}_{1}.c_{\mathsf{in}}[\mathsf{dy}]$,
and
$\rho[\mathsf{last}].c[\mathsf{dy}]\leq_{\omega}\mathcal{W}_{1}.c_{\mathsf{out}}[\mathsf{dy}]$
also hold. By (a) and compositionality, we obtain
$\sigma=\rho_{0}.\sigma_{1}.\rho_{2}\in\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{W}_{1})$
with $\sigma_{1}\approx\rho_{1}$. Since $\approx$ does not change counter
valuations, and $\rho$ already reaches the initial and final valuations of
$\mathcal{W}_{1}$, we know that
$\sigma\in\mathsf{Acc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W}_{1})$. Using the
faithfulness of $\mathcal{W}_{1}$,
$\sigma\in\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{W}_{1})$,
and $\sigma\in\mathsf{Acc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W}_{1})$, we
deduce $\rho\in\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W}_{1})$. This
yields
$\sigma_{1}\in\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W}_{1}^{\prime})$,
which implies
$\rho_{1}[\mathsf{first}].c[\mathsf{dy}]\leq_{\omega}\mathcal{W}_{1}^{\prime}.c_{\mathsf{in}}[\mathsf{dy}]$
and
$\rho_{1}[\mathsf{last}].c[\mathsf{dy}]\leq_{\omega}\mathcal{W}_{1}^{\prime}.c_{\mathsf{out}}[\mathsf{dy}]$
by the properties of $\approx$. We also note that
$\rho\in\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{W}_{0})$
implies
$\rho_{1}\in\mathsf{IAcc}_{\mathbb{Z},\sqsubseteq_{\omega}^{\mu}\\![\mathsf{dy}]}(\mathcal{W}_{0}^{\prime})$.
We use induction hypothesis (b) to get
$\rho_{1}\in\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W}_{0}^{\prime})$.
Since the outer run $\rho_{0}.\bullet.\rho_{2}$ fulfills the remaining
requirements by
$\sigma=\rho_{0}.\sigma_{1}.\rho_{2}\in\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W}_{1})$,
we get
$\rho=\rho_{0}.\rho_{1}.\rho_{2}\in\mathsf{IAcc}_{\mathbb{Z},\mathsf{dy}}(\mathcal{W}_{0})$.
∎

###  B.2. Decomposition Steps

In this section, we prove Lemma 8.5 and Lemma 8.6. They both involve
decomposing a precovering graph $(G,\mu)$ into sets of DMGTS $U$ and $V$ that
track extra information. We do this by enriching the structure of the
precovering graph. To make this enrichment formal and our handling uniform, we
define _observer NFA_. An observer NFA $\mathcal{O}=(Q,I,G.E,\delta,F)$ for
$G$ is an NFA $\mathcal{A}$ that has the edges $G.E$ as its alphabet. We note
that the language of an observer $\mathit{L}(\mathcal{O})\subseteq G.E^{*}$
consist of sequences of edges in $G$. By constructing the product of an
observer and a precovering graph, we get a larger automaton that accepts the
edge sequences of runs based on the information we want to track. We then
decompose this automaton into MGTS, in accordance with the valuations of $G$.

We define the product $G\times\mathcal{O}$ between an observer
$\mathcal{O}=(Q,I,G.E,\delta,F)$ and a precovering graph $G$ to be the
observer $(G.V\times Q,\\{G.v_{\mathsf{root}}\\}\times
I,G.E,\delta_{\times},\\{G.v_{\mathsf{root}}\\}\times F)$, where

$\displaystyle\delta_{\times}=\\{((p_{0},p_{1}),$ $\displaystyle
e,(q_{0},q_{1}))\mid$ $\displaystyle $ $\displaystyle e\in
G.E,e=(p_{0},a,x,q_{0}),(p_{1},e,q_{1})\in\delta\\}.$

Intuitively, $G\times\mathcal{O}$ simulates $\mathcal{O}$ along the edges $G$
can take during a run. We construct MGTS along the runs in
$G\times\mathcal{O}$. Towards this construction, we define the precovering
graphs. For each state $p$ of $\mathcal{O}\times G$, we define the precovering
graph

$\displaystyle G_{p}^{\mathcal{O}}$