Max Planck Institute for Software Systems (MPI-SWS), Germanypbaumann@mpi-
sws.orghttps://orcid.org/0000-0002-9371-0807 TU Braunschweig,
Germanye.keskin@tu-bs.dehttps://orcid.org/0009-0009-5621-6568 TU Braunschweig,
Germanyroland.meyer@tu-bs.dehttps://orcid.org/0000-0001-8495-671X Max Planck
Institute for Software Systems (MPI-SWS), Germanygeorg@mpi-
sws.orghttps://orcid.org/0000-0002-6421-4388 Pascal Baumann, Eren Keskin,
Roland Meyer, and Georg Zetzsche <ccs2012> <concept>
<concept_id>10003752.10003790</concept_id> <concept_desc>Theory of computation
Logic</concept_desc> <concept_significance>500</concept_significance>
</concept> <concept> <concept_id>10003752.10003766</concept_id>
<concept_desc>Theory of computation Formal languages and automata
theory</concept_desc> <concept_significance>500</concept_significance>
</concept> </ccs2012> [500]Theory of computation Logic [500]Theory of
computation Formal languages and automata theory [3cm]eu-erc.pdfFunded by the
European Union (ERC, FINABIS, 101077902). Views and opinions expressed are
however those of the author(s) only and do not necessarily reflect those of
the European Union or the European Research Council Executive Agency. Neither
the European Union nor the granting authority can be held responsible for
them. Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson 4 51st
International Colloquium on Automata, Languages, and Programming (ICALP 2024)
ICALP 2024 ICALP 2024 July 8–12, 2024 Tallinn, Estonia 297 157
o$\IfNoValueTF{#1}{\delta}{\delta_{#1}}$ o$\IfNoValueTF{#1}{\varphi}{\varphi}$

# Separability in Büchi VASS and Singly Non-Linear Systems of Inequalities

Pascal Baumann  Eren Keskin  Roland Meyer  Georg Zetzsche

###### Abstract

The $\omega$-regular separability problem for Büchi VASS coverability
languages has recently been shown to be decidable, but with an
$\mathsf{EXPSPACE}$ lower and a non-primitive recursive upper bound—the exact
complexity remained open. We close this gap and show that the problem is
$\mathsf{EXPSPACE}$-complete. A careful analysis of our complexity bounds
additionally yields a $\mathsf{PSPACE}$ procedure in the case of fixed
dimension $\geq 1$, which matches a pre-established lower bound of
$\mathsf{PSPACE}$ for one dimensional Büchi VASS. Our algorithm is a non-
deterministic search for a witness whose size, as we show, can be suitably
bounded. Part of the procedure is to decide the existence of runs in VASS that
satisfy certain non-linear properties. Therefore, a key technical ingredient
is to analyze a class of systems of inequalities where one variable may occur
in non-linear (polynomial) expressions.

These so-called singly non-linear systems (SNLS) take the form
$\bm{A}(x)\cdot\bm{y}\geq\bm{b}(x)$, where $\bm{A}(x)$ and $\bm{b}(x)$ are a
matrix resp. a vector whose entries are polynomials in $x$, and $\bm{y}$
ranges over vectors in the rationals. Our main contribution on SNLS is an
exponential upper bound on the size of rational solutions to singly non-linear
systems. The proof consists of three steps. First, we give a tailor-made
quantifier elimination to characterize all real solutions to $x$. Second,
using the root separation theorem about the distance of real roots of
polynomials, we show that if a rational solution exists, then there is one
with at most polynomially many bits. Third, we insert the solution for $x$
into the SNLS, making it linear and allowing us to invoke standard solution
bounds from convex geometry.

Finally, we combine the results about SNLS with several techniques from the
area of VASS to devise an $\mathsf{EXPSPACE}$ decision procedure for
$\omega$-regular separability of Büchi VASS.

###### keywords:

Vector addition systems, infinite words, separability, inequalities,
quantifier elimination, rational, polynomials

##  1 Introduction

Vector addition systems with states (VASS) are one of the most popular and
well-studied models of concurrent systems. A $d$-dimensional VASS consists of
finitely many control states and $d$ counters. Transitions between control
states can increment or decrement the $d$ counters, but importantly, one can
only take a transition if the new counter values remain non-negative.

#### Separability problems

In recent years, a strong focus of the research on VASS was on _separability
problems_ [18, 2, 11, 32, 8, 9, 10, 5, 6, 16, 17]. Here, we label the
transitions of the input VASS $\mathcal{V}_{1}$, $\mathcal{V}_{2}$ by letters,
which gives rise to languages $L_{1}$ and $L_{2}$. Then, we ask whether there
exists a language $S$, from some class $\mathcal{S}$ of allowed separators,
such that $L_{1}\subseteq S$ and $L_{2}\cap S=\emptyset$. Here, $\mathcal{S}$
is typically the class of regular languages.

An important motivation for studying separability problems is that separators
can be viewed as certificates for disjointness, and thus the non-existence of
a run in the product of $\mathcal{V}_{1}$ and $\mathcal{V}_{2}$. Such
certificates are crucial for understanding safety verification for infinite-
state systems, where the difficult part is to prove the non-existence of a run
(the existence of a run is usually easy to show). In particular, certificates
for non-existence are often the ingredient that is conceptually hardest to
come by. For example, in the case of reachability in VASS, the KLM
decomposition [27, 19, 20, 23] and Leroux’s Presburger-definable inductive
invariants [22] can be viewed as such certificates. Regular separators could
play a similar role in alternative approaches to reachability.

In addition to understanding certificates, the recent attention on
separability has led to other applications. For example, work on separability
by bounded languages has led to a general framework to address unboundedness
problems for VASS [8]. Moreover, separability results were used in an
algorithm for deciding inclusion between unambiguous VASS [7].

With the recent contribution by Keskin and Meyer [17] (together with earlier
decidability results for subclasses and variants [2, 11, 8, 9, 10, 5, 6]),
proving regular separability decidable for (finite-word) VASS, the
_decidability_ status of regular separability has largely been settled.
However, concerning _complexity_ , regular separability is far from
understood, with few results: So far, the only exact complexity results are
$\mathsf{PSPACE}$-completeness for (succintly represented) one-dimensional
VASS [9], $\mathsf{EXPSPACE}$-completeness for VASS coverability languages
[10], and Ackermann-completeness for VASS reachability languages [17].

#### Büchi VASS

A particularly challenging problem is ($\omega$-)regular separability in Büchi
VASS [2]. In a Büchi VASS $\mathcal{V}$, the language $L(\mathcal{V})$
consists of _infinite words_ induced by runs that visit some final state
infinitely often. As demonstrated by Baumann, Meyer, and Zetzsche [2], Büchi
VASS behave quite differently in terms of regular separability from their
finite-word counterpart, coverability languages of VASS [10]. Nevertheless,
Baumann, Meyer, and Zetzsche proved decidability of regular separability for
Büchi VASS [2]. However, the complexity remained open: Their algorithm
requires at least Ackermannian time (because it constructs Karp-Miller
graphs), and the only known lower bound is $\mathsf{EXPSPACE}$.

#### Challenge: Non-linear constraints

Improving the complexity established in [2] is challenging due to the
characterization of inseparability there: Inseparability is equivalent to the
existence of a constellation of runs, called an _inseparability flower_ , that
must satisfy a _non-linear constraint_ , meaning a constraint that is not
expressible in linear arithmetic (i.e. first-order logic of
$(\mathbb{Z};+,<,0,1)$ or $(\mathbb{Q};+,<,0,1)$). Essentially, such a flower
is a triple $(\alpha,\beta,\gamma)$ of cyclic runs such that (among other
linear inequalities) the counter effect of the combined run
$\alpha\beta\gamma$ is a scalar multiple of the counter effect of just
$\alpha$. In other words, we are looking for runs with effects
$\bm{u},\bm{v}\in\mathbb{Z}^{n}$ such that

$\exists x\in\mathbb{Q}\colon\bm{v}=x\cdot\bm{u}\ .$ (1)

Detecting runs with such constraints is difficult: There are powerful generic
$\mathsf{EXPSPACE}$ algorithms for detecting runs that satisfy unboundedness
conditions [12], linear constraints [1], or variants of computation tree logic
(CTL) [4]. However, condition (1) falls in neither of those categories.

In fact, we are not aware of any algorithmic approach to solving systems of
linear inequalities with constraints of type (1) (let alone inside algorithms
for VASS). There is a result by Gurari & Ibarra [13] showing that integral
feasibility of systems of equalities $\bm{A}\cdot\bm{y}=\bm{b}(x)$ can be
decided in $\mathsf{NP}$, where $\bm{b}(x)$ is a vector containing in each
component a quotient of polynomials in $x$. However, these do not seem to
capture (1): By moving the denominators from $\bm{b}(x)$ to the left-hand
side, one obtains equations where every variable from $\bm{y}$ is multiplied
with the same polynomial over $x$. However, for (1), we need to multiply a
_subset_ of the linear variables (namely, those in $\bm{u}$) with a polynomial
(namely, $x$). The same is true for the logic of _almost linear arithmetic_
due to Weispfenning [33], whose existential fragment is also solvable in
$\mathsf{NP}$. Here, the definable sets are finite unions of solution sets of
Gurari & Ibarra.

Furthermore, it is not even clear how to detect inseparability flowers by
invoking reachability in VASS (even though this would only yield an Ackermann
upper bound): To some extent, algorithms for reachability permit non-linear
constraints—for example, using standard tricks, it is decidable whether one
can reach a configuration with counter values $(m,n)$ such that $n\leq 2^{m}$.
However, the condition in (1) does not even seem to be captured by such
methods.

#### Contribution

Our main result is that regular separability in Büchi VASS is
$\mathsf{EXPSPACE}$-complete, and $\mathsf{PSPACE}$-complete in fixed
dimension $\geq 1$. The key technical ingredient is a method that we expect to
be of independent interest: We develop a procedure for solving systems of
linear inequalities with a single non-linear variable, which we call _singly
non-linear systems of inequalities_ (SNLS). We use our results about SNLS to
show that if an inseparability witness exists, then there is one where all
runs have at most doubly exponential length, yielding an $\mathsf{EXPSPACE}$
procedure. In fixed dimension, we obtain singly exponential bounds, leading to
a $\mathsf{PSPACE}$ procedure.

#### Step I: Singly non-linear systems of inequalities

Intuitively, a singly non-linear system of inequalities (SNLS) is a system of
inequalities that is linear in all but one variable. This means, there is one
variable $x$ that may appear in arbitrary polynomials, but all others can only
occur linearly. More precisely, an SNLS is a system of inequalities of the
form

$\bm{A}(x)\cdot\bm{y}\geq\bm{b}(x),\quad\bm{y}\geq\bm{0}\ ,$ (2)

where $\bm{A}(x)\in\mathbb{Z}[x]^{m\times n}$ is an $m\times n$ matrix over
the ring $\mathbb{Z}[x]$ of integer polynomials in $x$,
$\bm{b}(x)\in\mathbb{Z}[x]^{m}$ is a vector of polynomials from
$\mathbb{Z}[x]$, and $\bm{y}$ ranges over $\mathbb{Q}^{n}$. Notice that here
indeed, $x$ can be freely multiplied with itself and other variables, whereas
the expression on the left-hand side must be linear in each component of
$\bm{y}$.

Our main result about SNLS is that if a system as in (2) has a solution
$(x,\bm{y})\in\mathbb{Q}\times\mathbb{Q}^{n}$, then it has a solution where
all numbers (numerators and denominators) are bounded exponentially in the
description size of $\bm{A}(x)$ and $\bm{b}(x)$, even if numbers in the
description are encoded in binary. This implies in particular that feasibility
of SNLS is in $\mathsf{NP}$.

In the proof, we first show that the set of all $x\in\mathbb{Q}$ for which
there is a solution $(x,\bm{y})$ can be described by a Boolean combination
$\Phi$ of polynomial constraints of the form $p(x)\geq 0$, for polynomials
$p\in\mathbb{Z}[x]$. This amounts to a quantifier elimination procedure for a
class of first-order formulas in the ordered field
$(\mathbb{Q};+,\cdot,<,0,1)$. This is perhaps surprising, since this structure
does not admit quantifier elimination in general [25, Theorem 2].

Let us give a geometric explanation how we arrive at the constraints
$\Phi(x)$: For each choice of $x$, the SNLS
$\bm{A}(x)\cdot\bm{y}\geq\bm{b}(x),\leavevmode\nobreak\ \bm{y}\geq\bm{0}$
defines a polyhedron. It is a standard fact in convex geometry that such a
polyhedron has a point on a minimal face, and moreover this point can be
expressed as the inverse of a submatrix of $\bm{A}(x)$ multiplied with
$\bm{b}(x)$. This expression can then be plugged back into
$\bm{A}(x)\cdot\bm{y}\geq\bm{b}(x)$ to obtain a set of polynomial constraints
on $x$, subject to a particular determinant being non-zero. The latter non-
zero condition can as well be expressed as a polynomial constraint.

We then show that $\Phi$ has a small solution: In one case, a rational root of
one of the polynomials $p$ is a solution—these can be bounded by the _Rational
Root Theorem_. The other case is that the solution $x$ lies strictly between
two roots $r_{1}<r_{2}$ of participating polynomials. But then one can observe
that any rational number between those roots is a solution (if no other root
lies between $r_{1}$ and $r_{2}$). Using the _Root Separation Theorem_
(specifically, Rump’s Bound [28]), which lower-bounds the size of such
intervals $(r_{1},r_{2})$, we can then conclude that such an interval must
contain a rational number with small numerator and denominator.

Once we exhibit a small $x$, we can plug it into
$\bm{A}(x)\cdot\bm{y}\geq\bm{b}(x)$ to obtain a system of linear inequalities.
Then we use standard bounds to obtain a small (i.e. exponential) solution
$\bm{y}\in\mathbb{Q}^{n}$. It should be noted that while our result about SNLS
concerns rational solutions, we apply it in the case where
$\bm{b}(x)\geq\bm{0}$, which means a rational solution can be turned into an
integral solution by multiplying a common denominator.

#### Step II: Rackoff-like bounds

After establishing the solution bound for SNLS, we use this result in the
context of Büchi VASS to show the existence of inseparability witnesses that
are small, i.e. consist of runs that are at most doubly exponential in length.
Here, we use an adaptation of the Rackoff technique [29] similar to the proofs
of Habermehl [14] and Atig & Habermehl [1]. In [1], it is shown that runs
satisfying (restricted) linear inequalities can be detected in
$\mathsf{EXPSPACE}$. For this, they use a Rackoff-style induction to bound the
length of such runs. We devise a similar Rackoff-style induction to work with
SNLS instead of ordinary linear inequalities. Different compared to the
earlier works is the fact that our witnesses contain $\omega$-counters, which
may change when invoking the induction hypothesis. Moreover, we need to use a
result of Demri on selective unboundedness [12, Theorem 4.6] (in
$\mathsf{EXPSPACE}$ in the general case and $\mathsf{PSPACE}$ in fixed
dimension) to check the coverability of our witnesses.

##  2 Preliminaries

#### Büchi VASS

A _Büchi vector addition system with states (Büchi VASS)_ of dimension
$d\in\mathbb{N}$ over an alphabet $\Sigma$ is a tuple
$\mathcal{V}=(Q,q_{0},\Sigma,T,F)$. It consists of a finite set of states $Q$,
an initial state $q_{0}\in Q$, a set of final states $F\subseteq Q$, and a
finite set of transitions $T\subseteq\
Q\times\Sigma^{*}\times\mathbb{Z}^{d}\times Q$. The size of the Büchi VASS is
$|\mathcal{V}|:=|Q|+|F|+\sum_{(q,w,\delta,q^{\prime})\in
T}\big{(}|w|+|\\!|\delta|\\!|_{2}\big{)}$. By $|\\!|\delta|\\!|_{2}$, we mean
the size of the binary encoding of $\delta$. Since we only consider Büchi VASS
in this paper, we often simply call them VASS. If $d=0$, we call $\mathcal{V}$
a _Büchi automaton_.

The semantics of the Büchi VASS is defined over its _configurations_ , which
are elements of $Q\times\mathbb{N}^{d}$. The _initial configuration_ of
$\mathcal{V}$ is $(q_{0},\bm{0})$. We lift the transitions of the Büchi VASS
to a relation over configurations $\rightarrow\ \subseteq\
Q\times\mathbb{N}^{d}\times\Sigma^{*}\times Q\times\mathbb{N}^{d}$ as follows:
$(q,\bm{m})\xrightarrow{w}(q^{\prime},\bm{m}^{\prime})$ if there is
$(q,w,\delta,q^{\prime})\in T$ such that $\bm{m}^{\prime}=\bm{m}+\delta$. A
_run_ of the Büchi VASS is a (possibly infinite) sequence of configurations of
the form
$\sigma=(p_{0},\bm{m}_{0})\xrightarrow{w_{1}}(p_{1},\bm{m}_{1})\xrightarrow{w_{2}}\cdots$.

A run $\sigma$ is _accepting_ if it starts from the initial configuration and
visits final states infinitely often, meaning there are infinitely many
configurations $(q,\bm{m})$ in $\sigma$ with $q\in F$. The run is said to be
_labeled_ by the word $w=w_{0}w_{1}\cdots$ in $\Sigma^{\omega}$. The
_language_ $L(\mathcal{V})$ of the Büchi VASS consists of all infinite words
that label an accepting run.

An infinite-word language $L\subseteq\Sigma^{\omega}$ is called _regular_ if
it is accepted by a Büchi automaton. As we only consider infinite-word
languages, we just call them languages.

#### Arithmetic

Our approach to regular separability in Büchi VASS rests on a result about
solutions to singly non-linear systems of inequalities. This also requires
some terminology.

We define the integers, rationals, polynomials, and matrices together with the
operations we need to perform on them. Let $a\in\mathbb{Z}$ be an integer. Its
size $|\\!|a|\\!|_{2}=|\mathit{bin}(a)|$ is the length of its binary encoding.
We also use $|\\!|a|\\!|_{1}$ to denote the size of the unary encoding. This
is the absolute value plus an extra bit for the sign. A polynomial with
integer coefficients $p\in\mathbb{Z}[x]$ is a sum $\sum_{i=0}^{k}a_{i}x^{i}$
with $a_{0},\ldots,a_{k}\in\mathbb{Z}$ and $a_{k}\neq 0$ if $k>0$. We define
$|\\!|p|\\!|_{1}=\sum_{i=0}^{k}|\\!|a_{i}|\\!|_{1}$ and similar for
$|\\!|p|\\!|_{2}$. The _degree_ of the polynomial is $\deg(p)=k$, its _maximal
coefficient_ is $\operatorname{maxc}(p)=\max_{i\in[0,k]}|\\!|a_{i}|\\!|_{1}$.
Note that $|\\!|p|\\!|_{1}\leq(\deg(p)+1)\cdot\operatorname{maxc}(p)$. A real
number $r\in\mathbb{R}$ with $p(r)=0$ is called a _root_ of the polynomial.
Let $\mathit{S}$ be a set with a size function $|\\!|-|\\!|$ defined on it. We
consider matrices $\bm{A}\in\mathit{S}^{m\times n}$ over $\mathit{S}$, and
define their size $|\\!|\bm{A}|\\!|$ by summing up the sizes of the entries.
We use $\mathit{row}(\bm{A})=m$ and $\mathit{col}(\bm{A})=n$. When
$\mathit{S}=\mathbb{Z}[x]$, we also use $\deg(\bm{A})$ for the highest degree
of a polynomial in $\bm{A}$ and $\operatorname{maxc}(\bm{A})$ for the maximal
coefficient of a polynomial in $\bm{A}$. Pairs
$(s_{1},s_{2})\in\mathit{S}\times\mathit{S}$ form a special case with size
$|\\!|(s_{1},s_{2})|\\!|=|\\!|s_{1}|\\!|+|\\!|s_{2}|\\!|$. In particular, a
rational number $\mathit{t}\in\mathbb{Q}$ is a pair $\mathit{t}=\frac{a}{b}$
of integers $a,b\in\mathbb{Z}$ with
$|\\!|\mathit{t}|\\!|_{1}=|\\!|a|\\!|_{1}+|\\!|b|\\!|_{1}$, and similar for
$|\\!|\mathit{t}|\\!|_{2}$.

We perform addition $a+b$ and multiplication $a\cdot b$ among integers,
rationals, polynomials, and matrices. These operations can be executed in time
polynomial in $|\\!|a|\\!|_{2}+|\\!|b|\\!|_{2}$. The same holds for the
comparison $a\geq b$ among integers and rationals. We also add, multiply, and
compare integers and rationals with $-\infty$ and $\infty$. The definitions
are as expected.

##  3 Main results

A language $\mathit{R}\subseteq\Sigma^{\omega}$ is said to _separate_
languages $\mathit{L}_{1},\mathit{L}_{2}\subseteq\Sigma^{\omega}$, if
$\mathit{L}_{1}\subseteq\mathit{R}$ and
$\mathit{R}\cap\mathit{L}_{2}=\emptyset$. We call $\mathit{L}_{1}$ and
$\mathit{L}_{2}$ _regular separable_ , denoted by
$\mathit{L}_{1}\mathop{|}\mathit{L}_{2}$, if there is a separator $\mathit{R}$
that is a regular language. The problem we address is the _regular
separability problem_ for Büchi VASS:

Given

Two VASS $\mathcal{V}_{1}$ and $\mathcal{V}_{2}$ over some alphabet $\Sigma$.

Question

Does $\mathit{L}(\mathcal{V}_{1})\mathop{|}\mathit{L}(\mathcal{V}_{2})$ hold?

We also consider the variants of this problem where the inputs are of fixed
dimension: For a fixed number $d\in{\rm Nature}\setminus\\{0\\}$, the _$d$
-dimensional regular separability problem_ for Büchi VASS is the same problem
as above, except that the input VASS $\mathcal{V}_{1}$ and $\mathcal{V}_{2}$
are restricted to be of dimension at most $d$. Our first main result is the
following:

######  Theorem 3.1.

The regular separability problem for Büchi VASS is
$\mathsf{EXPSPACE}$-complete. Moreover, the $d$-dimensional regular
separability problem is $\mathsf{PSPACE}$-complete for all $d\geq 1$.

As mentioned above, the proof is based on a small model property for what we
call singly non-linear systems of inequalities. We expect this result to be of
independent interest. Formally, a _singly non-linear system (SNLS)_ is a
system of inequalities of the form

$\displaystyle\bm{A}(x)\cdot\bm{y}\geq\bm{b}(x)\wedge\bm{y}\geq\bm{0}\ .$

Here, $\bm{A}(x)\in\mathbb{Z}[x]^{m\times n}$ is an $m\times n$ matrix over
the set of polynomials with integer coefficients in variable $x$, and
$\bm{b}\in\mathbb{Z}[x]^{m}$ is a vector of polynomials. We also write an SNLS
as $\mathcal{S}=(\bm{A}(x),\bm{b}(x))$, or $\mathcal{S}(x,\bm{y})$ to
emphasize the variables. A _solution_ to $\mathcal{S}$ is a pair
$(\mathit{t},\bm{s})\in\mathbb{Q}\times\mathbb{Q}^{n}$ that satisfies
$\bm{A}(\mathit{t})\cdot\bm{s}\geq\bm{b}(\mathit{t})\wedge\bm{s}\geq\bm{0}$.
If a solution exists, we call the system _feasible_.

Our second main result is a bound on the size of least solutions.

######  Theorem 3.2.

If the SNLS $\mathcal{S}$ is feasible, then it has a solution
$(\mathit{t},\bm{s})$, where all components of $\bm{s}$ have the same
denominator, with
$|\\!|\mathit{t}|\\!|_{1},|\\!|\bm{s}|\\!|_{1}\in(\mathit{col}(\mathcal{S})\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(\deg(\mathcal{S})^{2}\cdot\mathit{row}(\mathcal{S})^{4})}$.

Theorem 3.2 implies that a feasible system $\mathcal{S}$ always has a solution
of size at most singly exponential in $|\\!|\mathcal{S}|\\!|_{1}$. This gives
an upper bound on the complexity of feasibility.

######  Corollary 3.3.

Feasibility of SNLS is in $\mathsf{NP}$.

The reader may have noted that SNLS are more general than the non-linear
systems we are confronted with when checking separability. There are at least
two arguments in support of the generalization. First, non-linearity is not
well-understood, and we believe a class of systems that admits an efficient
algorithm for checking feasibility will find its applications. Second, the
generalization only adds little complexity to the proof or, phrased
differently, the special case already needs most considerations.

#### Organization

The remainder of the paper is organized as follows. In Section 4, we prove
Theorem 3.2 and in Section 5, we show Theorem 3.1.

##  4 Singly Non-Linear Systems

In this section, we prove Theorem 3.2.

#### Some notation

By $\bm{A}(\mathit{t})$ or $\mathit{eval}(\bm{A}(x),\mathit{t})$ we mean the
matrix with rational entries that results from $\bm{A}(x)$ by evaluating all
polynomials at $\mathit{t}$. Let $\bm{A}\in R^{n\times n}$ be a square matrix
over some ring $R$. In our exposition, we will consider matrices over the
rings $\mathbb{Z}$, $\mathbb{Q}$, and $\mathbb{Z}[x]$. We write $\det(\bm{A})$
for the determinant, and recall that if $R$ is a field (such as $\mathbb{Q}$),
then $\bm{A}$ is invertible if and only if $\det(\bm{A})\neq 0$. The
_adjugate_ (also called _classical adjoint_) of $\bm{A}$ is the matrix
$\operatorname{adj}(\bm{A})\in R^{n\times n}$ with
$\operatorname{adj}(\bm{A})[j,i]=(-1)^{i+j}\det(\bm{A}_{ij})$, where
$\bm{A}_{ij}$ is the matrix obtained from $\bm{A}$ by removing the $i$-th row
and the $j$-th column. It is well-known that then
$\bm{A}\cdot\operatorname{adj}(\bm{A})=\det(\bm{A})\cdot\bm{I}$, where
$\bm{I}$ is the identity matrix in dimension $n$. In particular, if $\bm{A}$
is invertible, its inverse can be computed as
$\bm{A}^{-1}=\frac{\operatorname{adj}(\bm{A})}{\det(\bm{A})}$ [21, Chapter
XIII, Prop. 4.16].

In upper bound arguments, we will use the well-known Leibniz formula for
determinants, which says $\det(\bm{A})=\sum_{\sigma\in
S_{n}}\operatorname{sgn}(\sigma)\cdot\prod_{i=1}^{n}\bm{A}[i,\sigma(i)]$ [21,
Chapter XIII, Prop. 4.6]. Here, $S_{n}$ is the set of all permutations of
$[1,n]$ and $\operatorname{sgn}(\sigma)\in\\{-1,1\\}$ is the sign of
$\sigma\in S_{n}$.

#### Bounding solutions

For the proof of Theorem 3.2, we proceed in two steps. We first show that if
an SNLS $\mathcal{S}(x,\bm{y})$ is feasible, then we find a small rational
$\mathit{t}$ for $x$ such that the system $\mathcal{S}(\mathit{t},\bm{y})$ is
feasible. This system is the result of evaluating all polynomials in
$\mathcal{S}$ at $\mathit{t}$, and thus having only $\bm{y}$ as the variables.

######  Lemma 4.1.

If the SNLS $\mathcal{S}(x,\bm{y})$ is feasible, then there is a number
$\mathit{t}\in\mathbb{Q}$ with
$|\\!|\mathit{t}|\\!|_{1}\in(\mathit{col}(\mathcal{S})\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(\deg(\mathcal{S})\cdot\mathit{row}(\mathcal{S})^{3})}$
such that $\mathcal{S}(\mathit{t},\bm{y})$ is feasible.

Lemma 4.1 is non-trivial and will occupy almost this entire section. To
explain our approach, note that the feasibility of $\mathcal{S}(x,\bm{y})$ is
equivalent to the feasibility of $\exists\bm{y}.\mathcal{S}(x,\bm{y})$. Our
first step is to eliminate the quantifier and determine a new formula
$\Phi(x)$ in which $\bm{y}$ no longer occurs and that is equivalent to the
previous one over the rationals,
$\exists\bm{y}.\mathcal{S}(x,\bm{y})\mathop{\models\rotatebox[origin={c}]{180.0}{$\models$}_{\mathbb{Q}}}\Phi(x)$.
The equivalence says that for every $\mathit{t}\in\mathbb{Q}$, we have
$\mathit{t}\models\exists\bm{y}.\mathcal{S}(x,\bm{y})$ if and only if
$\mathit{t}\models\Phi(x)$.

The second step for Lemma 4.1 is to show that if the new formula holds, then
we find a small solution for $t$. To this end, we will apply the Root
Separation Theorem, which provides a lower bound on the distance between
distinct real roots of polynomials. After establishing Lemma 4.1, we obtain
Theorem 3.2 (at the end of this section) by taking the $t$ provided by Lemma
4.1, and pair it with the $\bm{s}\in\mathbb{Q}^{n}$, which must exist
according to the quantifier elimination done in the first step of Lemma 4.1.

###  4.1 Quantifier Elimination

We show how to remove the quantifier from
$\exists\bm{y}.\mathcal{S}(x,\bm{y})$ with a tailor-made quantifier
elimination algorithm. The fact that quantifier elimination is possible in
this setting came as a surprise to us, given the non-linear nature and the
setting of rationals. For example, the real closed field
$(\mathbb{R};+,\cdot,<,0,1)$ admits quantifier elimination by a classical
result of Tarski [26, Theorem 3.3.15], but this is not true for the ordered
field $(\mathbb{Q};+,\cdot,<,0,1)$ of rationals [25, Theorem 2] (see [26, p.
71–72] for a simple example). This means, there are first-order formulas over
$(\mathbb{Q};+,\cdot,<,0,1)$ that have no quantifier-free equivalent. However,
we show that if we existentially quantify the linear variables in the formulas
induced by SNLS, then those quantifiers can be eliminated.

The precise formulation of the result needs some notation. A _lower bound
constraint_ has the form $p(x)\geq 0$ or $p(x)>0$ with $p\in\mathbb{Z}[x]$ a
polynomial with integer coefficients. The formula $\Phi(x)$ that we want to
obtain takes the form $\bigvee_{i\in I}\bigwedge_{j\in J_{i}}\Phi_{i,j}(x)$,
where the formulae $\Phi_{i,j}(x)$ are lower bound constraints. We call it a
DNFLB, short for _disjunctive normal form with lower bound constraints as the
literals_. We may also omit $x$ and write $\Phi$. We use $\deg(\Phi)$ and
$\operatorname{maxc}(\Phi)$ for the maximal degree resp. coefficient of a
polynomial in $\Phi$.

######  Theorem 4.2.

For every SNLS $\mathcal{S}(x,\bm{y})$, there is a DNFLB $\Phi(x)$ with
$\exists\bm{y}.\mathcal{S}(x,\bm{y})\mathop{\models\rotatebox[origin={c}]{180.0}{$\models$}_{\mathbb{Q}}}\Phi(x)$,
$\deg(\Phi)\in\mathcal{O}(\mathit{row}(\mathcal{S})\cdot\deg(\mathcal{S}))$,
and
$\operatorname{maxc}(\Phi)\in(\mathit{col}(\mathcal{S})\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(\mathit{row}(\mathcal{S})^{2})}$.

Since our intention is to bound the solutions $\mathit{t}$ to variable $x$,
the given estimations on the degree and the maximal coefficient suffice for
us. The proof actually gives an algorithm to compute $\Phi$ which runs in time
exponential in the dimension of $\mathcal{S}$, but we do not need the
effectiveness here. In the proof of Theorem 4.2, we will use a standard fact
about polyhedra:

######  Lemma 4.3.

Suppose $\bm{D}\in\mathbb{Q}^{m\times n}$ and $\bm{c}\in\mathbb{Q}^{m}$. If
the system $\bm{D}\cdot\bm{x}\geq\bm{c}$ has a solution in $\mathbb{Q}^{n}$,
then there is a solution $\bm{s}\in\mathbb{Q}^{n}$ that also satisfies
$\bm{D}^{\prime}\cdot\bm{s}=\bm{c}^{\prime}$, where
$(\bm{D}^{\prime},\bm{c}^{\prime})$ is a subset of the rows of
$(\bm{D},\bm{c})$ such that
$\operatorname{rank}(\bm{D}^{\prime})=\operatorname{rank}(\bm{D})$.

######  Proof 4.4.

By well-known decomposition theorems about polyhedra, a polyhedron
$P=\\{\bm{s}\in\mathbb{Q}^{n}\mid\bm{D}\cdot\bm{s}\geq\bm{c}\\}$ is non-empty
if and only if it has a non-empty minimal face [31, Theorem 8.5]. Moreover,
minimal faces can be characterized as exactly the sets of the form
$\\{\bm{s}\in\mathbb{Q}^{n}\mid\bm{D}^{\prime}\cdot\bm{s}=\bm{c}^{\prime}\\}$,
where $(\bm{D}^{\prime},\bm{c}^{\prime})$ is a subset of the rows of
$(\bm{D},\bm{c})$ such that $\bm{D}^{\prime}$ has the same rank as $\bm{D}$
[31, Theorem 8.4].

We are ready to prove Theorem 4.2:

######  Proof 4.5 (Proof of Theorem 4.2).

Let
$\mathcal{S}(x,\bm{y})=\bm{A}(x)\cdot\bm{y}\geq\bm{b}(x)\wedge\bm{y}\geq\bm{0}$.
To fix the dimension, let $\bm{A}\in\mathbb{Z}[x]^{m\times n}$. We can
equivalently write the SNLS as
$\mathcal{S}^{\prime}(x,\bm{y})=\bm{D}(x)\cdot\bm{y}\geq\bm{c}(x)$ with

$\bm{D}(x)\ =\ \left(\begin{aligned} &\bm{A}(x)\\\
&\bm{I}_{n}\end{aligned}\right)\in\mathbb{Z}[x]^{(m+n)\times
n}\qquad\bm{c}(x)\ =\ \left(\begin{aligned} &\bm{b}(x)\\\
&\bm{0}_{n}\end{aligned}\right)\in\mathbb{Z}[x]^{m+n}\ ,$

i.e. we glue the $n\times n$ identity matrix $\bm{I}_{n}$ to the bottom of
$\bm{A}(x)$ and extend $\bm{b}(x)$ by $n$ zeros.

Assume $\mathcal{S}^{\prime}$ is feasible and the solution for $x$ is
$\mathit{t}\in\mathbb{Q}$. By Lemma 4.3 and since $\bm{D}(\mathit{t})$ has
rank $n$, we can select a subset of $n$ rows of $\bm{D}(\mathit{t})$ and of
$\bm{c}(\mathit{t})$ such that the smaller system has a solution, even with
equality. More formally, for any subset $R\subseteq[1,m+n]$, denote by
$\bm{D}_{R}(\mathit{t})$ (resp. $\bm{c}_{R}(\mathit{t})$) the matrix (resp.
vector) obtained by selecting only the rows in $R$ from $\bm{D}(\mathit{t})$
(resp. $\bm{c}(\mathit{t})$). Then Lemma 4.3 tells us that there is an
$\bm{s}\in\mathbb{Q}^{n}$ with
$\bm{D}_{R}(\mathit{t})\cdot\bm{s}=\bm{c}_{R}(\mathit{t})$, where
$\bm{D}_{R}(\mathit{t})$ has rank $n$. In particular, $\bm{D}_{R}(\mathit{t})$
is invertible and thus $\det(\bm{D}_{R}(\mathit{t}))\neq 0$. The fact that
$\bm{D}_{R}(t)$ is invertible allows us to write
$\bm{s}=\bm{D}_{R}(\mathit{t})^{-1}\cdot\bm{c}_{R}(\mathit{t})$, which will be
key for our quantifier elimination. The argumentation shows that for every
$t\in\mathbb{Q}$, $\exists\bm{y}.\mathcal{S}^{\prime}(t,\bm{y})$ is equivalent
to the condition

$\bigvee_{\begin{subarray}{c}R\subseteq[1,m+n]\\\
|R|=n\end{subarray}}\det(\bm{D}_{R}(t))\neq 0\ \wedge\
\bm{D}(t)\cdot\bm{D}_{R}(t)^{-1}\cdot\bm{c}_{R}(t)\geq\bm{c}(t)\ .$ (3)

Here, of course, we only know that $\bm{D}_{R}(\mathit{t})^{-1}$ exists when
$\det(\bm{D}_{R}(\mathit{t}))\neq 0$. To express (3) using polynomials, we
employ the identity
$\bm{D}_{R}(\mathit{t})^{-1}=\tfrac{\operatorname{adj}(\bm{D}_{R}(\mathit{t}))}{\det(\bm{D}_{R}(\mathit{t}))}$
whenever $\bm{D}_{R}(\mathit{t})$ is invertible (equivalently, whenever
$\det(\bm{D}_{R}(\mathit{t}))\neq 0$). Thus, the set of all $\mathit{t}$ with
$\exists\bm{y}\colon\mathcal{S}^{\prime}(\mathit{t},\bm{y})$ can be defined by
the following DNFLB $\Phi$:

$\displaystyle\bigvee_{\begin{subarray}{c}R\subseteq[1,m+n]\\\
|R|=n\end{subarray}}\leavevmode\nobreak\ $
$\displaystyle\Big{(}\det(\bm{D}_{R}(x))>0\leavevmode\nobreak\
\wedge\leavevmode\nobreak\
\bm{D}(x)\cdot\operatorname{adj}(\bm{D}_{R}(x))\cdot\bm{c}_{R}(x)\geq\det(\bm{D}_{R}(x))\cdot\bm{c}(x)\Big{)}$
(4) $\displaystyle\vee\Big{(}\det(\bm{D}_{R}(x))<0\leavevmode\nobreak\
\wedge\leavevmode\nobreak\
\bm{D}(x)\cdot\operatorname{adj}(\bm{D}_{R}(x))\cdot\bm{c}_{R}(x)\leq\det(\bm{D}_{R}(x))\cdot\bm{c}(x)\Big{)}\
,$

where indeed all conditions are of the form $p(x)\geq 0$ or $p(x)>0$ for some
polynomials $p$. Note that here, we distinguish the cases
$\det(\bm{D}_{R}(x))<0$ and $\det(\bm{D}_{R}(x))>0$ because moving a negative
$\det(\bm{D}_{R}(x))$ to the other side of the inequality changes $\geq$ to
$\leq$. Moreover, note that (in contrast to (3)) in the formulation (4), all
terms are well-defined, independenly of whether the current choice of $R$
makes $\bm{D}_{R}(x)$ invertible or not. To be precise, we obtain the DNFLB by
subtracting the right-hand sides of the inequalities from the left-hand sides
and multiplying the result by $-1$ to invert the inequality where necessary.
The above form will suffice to give an estimate on the maximal degree and the
maximal coefficient.

It is now clear that the coefficients (resp. degrees) appearing in $\Phi$ are
exponential (resp. polynomial) in the bitsize of $\mathcal{S}$. The precise
bounds promised in the Theorem are straightforward to deduce from standard
bounds on determinants, see Appendix A for details.

###  4.2 Root Separation

To show Lemma 4.1, it remains to be shown that any feasible DNFLB $\Phi(x)$
has a solution that is exponentially bounded. The key observation is that if
$r$ and $r^{\prime}$ are adjacent roots of a polynomial $p(x)\in\mathbb{Z}[x]$
and a constraint $p(x)\geq 0$ or $p(x)>0$ is satisfied for some $\mathit{t}$
for $x$ with $r<\mathit{t}<r^{\prime}$, then any number $\mathit{t}^{\prime}$
in the open interval $(r,r^{\prime})$ will also satisfy the constraint: The
polynomial does not change its sign between $r$ and $r^{\prime}$. Thus, we can
think of $\mathbb{R}$ as being split into (i) roots of $p$ and (ii) intervals
between roots of $p$ (and the infinite intervals below the smallest and above
the largest root). Then whether $\mathit{t}\in\mathbb{Q}$ satisfies $p(x)\geq
0$ or $p(x)>0$ only depends on which of those parts of $\mathbb{R}$ the number
$\mathit{t}$ belongs to. This remains true if we refine this decomposition of
$\mathbb{R}$ according to _all_ polynomials occurring in $\Phi$.

In order to construct rational numbers with small numerator and denominator in
intervals $(r,r^{\prime})$, we will rely on a Root Separation Theorem, saying
that polynomial roots are not too close. More specifically, we use Rump’s
Bound [28, Theorem 8.5.5]:

######  Theorem 4.6 (Rump’s Bound [28, Theorem 8.5.5]).

Suppose $r,r^{\prime}\in\mathbb{R}$ are distinct roots of a polynomial
$p(x)\in\mathbb{Z}[x]$ with degree $d\in{\rm Nature}$. Then
$|r-r^{\prime}|>(d^{d+1}(1+|\\!|p(x)|\\!|_{1})^{2d})^{-1}$.

We will also use an elementary fact about rational roots of integral
polynomials. It is known as the Rational Root Theorem or Integral Root Test
[21, Chapter IV, Prop. 3.3]:

######  Lemma 4.7 (Rational Root Theorem [21, Chapter IV, Prop. 3.3]).

Let $p(x)=c_{n}x^{n}+\cdots+c_{0}\in\mathbb{Z}[x]$ be a polynomial. If $r=a/b$
is a root of $p$ with $a,b$ co-prime, then $a$ divides $c_{0}$ and $b$ divides
$c_{n}$. In particular, $|a|,|b|\leq\operatorname{maxc}(p)$.

Finally, we need a standard bound on all real roots of a polynomial [28,
Corollary 8.3.2]. This is known as Cauchy’s bound.

######  Lemma 4.8 (Cauchy’s Bound [28, Corollary 8.3.2]).

If $r\in\mathbb{R}$ is a root of a polynomial $p\in\mathbb{Z}[x]$, then
$|r|\leq 1+|\\!|p|\\!|_{1}$.

Let $r_{1}<\cdots<r_{k}\in\mathbb{R}$ be all the real roots of polynomials
occurring in $\Phi$. Observe that if $\mathit{t}\in\mathbb{Q}$ satisfies
$\Phi(x)$ and $\mathit{t}\in(r_{i},r_{i+1})$, then any rational number in
$(r_{i},r_{i+1})$ must satisfy $\Phi(x)$, because none of the polynomials in
$\Phi$ changes its sign between $r_{i}$ and $r_{i+1}$. This allows us to bound
a rational solution, by distinguishing the following cases:

  1. 1.

Suppose $\Phi(x)$ is satisfied by some rational root $r_{i}$ of $p$ in $\Phi$.
Write $r_{i}=\tfrac{a}{b}$ with $a,b$ co-prime. Then the Rational Root Theorem
(Lemma 4.7) implies $|a|,|b|\leq\operatorname{maxc}(p)$.

  2. 2.

Suppose $\Phi(x)$ has a rational solution in some interval $(r_{i},r_{i+1})$.
Since $r_{i}$ and $r_{i+1}$ are the roots of some polynomials $p,q$ in
$\Phi(x)$, as observed above, any rational number in $(r_{i},r_{i+1})$ is also
a solution to $\Phi(x)$. Note that $r_{i},r_{i+1}$ are roots of $p(x)\cdot
q(x)$ and thus by Theorem 4.6, we have $|r_{i}-r_{i+1}|>\tfrac{1}{b}$ for some
$b\in\mathbb{Z}$ that is exponentially bounded. Thus, there is an integer
$a\in(br_{i},br_{i+1})$. Note that then $\tfrac{a}{b}$ belongs to the interval
$(r_{i},r_{i+1})$ and thus satisfies $\Phi(x)$. Moreover, by the Cauchy Bound
(Lemma 4.8), we also have an exponential bound $U\in\mathbb{R}$ on
$|r_{i}|,|r_{i+1}|$ and thus on $|a|\leq|b|U$.

  3. 3.

Suppose $\Phi(x)$ has a rational solution $\mathit{t}$ outside of
$[r_{1},r_{k}]$. If $\mathit{t}>r_{k}$ then every rational number in
$[r_{k},\infty)$ is also a solution. Moreover, by Lemma 4.8, any rational
number $\mathit{t}^{\prime}$ with $\mathit{t}^{\prime}>1+|\\!|p|\\!|_{1}$ for
every polynomial $p$ occurring in $\Phi$ can be chosen, e.g.
$\mathit{t}^{\prime}=2+c$, where $c=\max\\{|\\!|p|\\!|_{1}\mid p$ polynomial
in $\Phi\\}$. On the other hand, if $\mathit{t}<r_{1}$, then
$\mathit{t}^{\prime}=-(2+c)$ is a solution by an analogous argument.

This proves that any feasible $\Phi(x)$ has a rational solution that is
exponentially bounded, which is what we will use in our application to Büchi
VASS. The precise bounds of Lemma 4.1 are shown in Section A.2.

#### Proof sketch for Theorem 3.2

For showing Theorem 3.2, we can now use the fact that if $t\in\mathbb{Q}$
admits a solution $(t,\bm{s})$, then by our argument in the proof of Theorem
4.2,
$\bm{s}^{*}:=\tfrac{\operatorname{adj}(D_{R}(t))}{\det(D_{R}(t))}\cdot\bm{c}_{R}(t)$
is also a solution, for some subset $R\subseteq[1,m+n]$. This means that we
can apply the bound on $t$ and the bounds on
$\operatorname{adj}(\bm{D}_{R}(x))$ and $\det(\bm{D}_{R}(x))$ established in
the proof of Theorem 4.2 to bound the solution $\bm{s}^{*}$. We can ensure
that all components of $\bm{c}_{R}(t)$ have the same denominator by increasing
the bit size at most $\deg(\mathcal{S})$-fold. If we compute $\bm{s}^{*}$
starting from such a vector, we get an $\bm{s}^{*}$ where all components have
the same denominator. Since the entries in $\bm{D}_{R}$ all appear in
$\mathcal{S}$ and it is well-known that the determinant has polynomial bit
size in the bit size of a matrix, it follows that there exists a solution
$(t,\bm{s})$ of polynomial bit size. The precise bounds promised in Theorem
3.2 are derived in Section A.3.

##  5 $\omega$-Regular Separability

We use the results from Section 4 to prove Theorem 3.1. Note that the lower
bounds in Theorem 3.1 easily follow from [2]. First, that paper already shows
$\mathsf{PSPACE}$-completeness of regular separability for one-dimensional
Büchi VASS, which yields the $\mathsf{PSPACE}$ lower bound for fixed dimension
$\geq 1$. In fact, their argument also yields $\mathsf{EXPSPACE}$-hardness in
the general case: The full version [3, Appendix E.1] describes a simple
reduction from intersection emptiness of one-dimensional VASS that accept by
final state to regular separability of Büchi VASS, and the construction is the
same in higher dimension. This yields $\mathsf{EXPSPACE}$-hardness of regular
separability of Büchi VASS, since intersection emptiness of VASS of arbitrary
dimension that accept by final state is $\mathsf{EXPSPACE}$-hard [24].

It remains to prove the upper bounds in Theorem 3.1. To adequately formulate
our proofs, we need to introduce additional VASS-related concepts.

#### More on Büchi VASS

Let $\mathcal{V}=(Q,q_{0},\Sigma,T,F)$ be a Büchi VASS. Consider a (possibly
infinite) run
$\sigma=(p_{0},\bm{m}_{0})\xrightarrow{w_{1}}(p_{1},\bm{m}_{1})\xrightarrow{w_{2}}\cdots$
of $\mathcal{V}$. The sequence of transitions in $\sigma$ is called a _path_
and has the form
$\rho=(p_{0},w_{1},\delta_{1},p_{1})(p_{1},w_{2},\delta_{1},p_{2})\ldots$. If
a path is finite and the source state of its first transition coincides with
the target state of its last transition, then we call it a _loop_. Since a run
is uniquely determined by the start configuration and its sequence of
transitions, we also denote a run by $\sigma=(p_{0},\bm{m}_{0}).\rho$. If
$\sigma$ is finite and $(p_{\ell},\bm{m}_{\ell})$ is its last configuration,
then we sometimes write
$\sigma=(p_{0},\bm{m}_{0}).\rho.(p_{\ell},\bm{m}_{\ell})$ to emphasize this.
The _effect_ $\delta(\rho)$ of some finite path
$\rho=(p_{0},w_{1},\delta_{1},p_{1})\ldots(p_{\ell-1},w_{\ell},\delta_{\ell},p_{\ell})$
is the sum of all induced counter changes, formally $\delta(\rho)=\sum_{1\leq
i\leq\ell}\delta_{i}$.

Recall that configurations of the Büchi VASS $\mathcal{V}$ are elements of the
set $Q\times\mathbb{N}^{d}$. We call the second component in a configuration
the _counter valuation_ and refer to the $i$-th entry as the _value of counter
$i$_. For a configuration $\mathit{cf}$ and a set of counters
$I\subseteq[1,d]$ we also use $\mathit{cf}[I]$ to denote the counter valuation
of $\mathit{cf}$ restricted to the counters in $I$. A configuration
$(q,\bm{m})$ is _coverable_ in $\mathcal{V}$ if there is a run starting in the
initial configuration $(q_{0},\bm{0})$ and reaching a configuration
$(q,\bm{m}^{\prime})$ with $\bm{m}^{\prime}\geq\bm{m}$. Here, $\geq$ is
defined component-wise.

Moreover we also consider a set of _extended configurations_ $Q\times{\rm
Nature}_{\omega}^{d}$, where ${\rm
Nature}_{\omega}=\mathbb{N}\cup\\{\omega\\}$. Here $\omega$ is used to
represent a counter value that has become unbounded. For an extended
configuration $(q,\bm{m})$ we use $\omega(q,\bm{m})\subseteq[1,d]$ to denote
the set of counters valued $\omega$ in $\bm{m}$. Comparisons and arithmetic
operations between integer values and $\omega$ behave as expected, treating
$\omega$ as $\infty$. Formally, $\omega\geq\omega$, $\omega\geq z$, and
$\omega+z=\omega$ for all $z\in\mathbb{Z}$. The _size_ of an extended
configuration is $|(q,\bm{m})|=\log_{2}|Q|+|\\!|\bm{m}|\\!|_{2}+d$, where the
extra bit per counter encodes whether it has value $\omega$ or not. We also
use the size of a unary encoding
$|\\!|(q,\bm{m})|\\!|_{1}=|Q|+|\\!|\bm{m}|\\!|_{1}+d$.

The transition relation is also lifted to extended configurations in the
expected manner. Formally, for $(q,\bm{m})$, $(q^{\prime},\bm{m}^{\prime})\in
Q\times{\rm Nature}_{\omega}^{d}$ we have
$(q,\bm{m})\xrightarrow{w}(q^{\prime},\bm{m}^{\prime})$ if there is a
transition $(q,w,\delta,q^{\prime})\in T$ such that
$\bm{m}^{\prime}=\bm{m}+\delta$, where addition between elements of ${\rm
Nature}_{\omega}^{d}$ and $\mathbb{Z}^{d}$ is defined component-wise.
Furthermore, our definitions of runs, paths, loops, etc. carry over to
_extended_ versions over the set of extended configurations in a
straightforward way. More precisely, an _extended run_ is a sequence of
extended configurations
$\mathit{cf}_{1}\xrightarrow{w_{1}}\mathit{cf}_{2}\xrightarrow{w_{2}}\cdots$,
an _extended path_ is the underlying sequence of transitions of an extended
run, and an _extended loop_ is a finite extended path starting and ending in
the same state. To cover an extended configuration, intuitively, the
$\omega$-counters need to become unbounded, and the remaining counters need to
be covered. Formally, an extended configuration $(q,\bm{m})$ is _coverable_ in
$\mathcal{V}$ if for every $k\in\mathbb{N}$ there is a run starting in the
initial configuration $(q_{0},\bm{0})$ and reaching a configuration
$(q,\bm{m}_{k})\in Q\times\mathbb{N}^{d}$ such that $\bm{m}_{k}[j]\geq k$ for
every counter $j\in\omega(q,\bm{m})$ and $\bm{m}_{k}[i]\geq\bm{m}[i]$ for
every counter $i\in[1,d]\setminus\omega(q,\bm{m})$.

Finally, we sometimes want to restrict only some counters of the VASS to stay
non-negative. In this case, we consider extended configurations in
$Q\times\mathbb{Z}_{\omega}^{d}$, where
$\mathbb{Z}_{\omega}=\mathbb{Z}\cup\\{\omega\\}$. We say an extended run
$\sigma=\mathit{cf}.\rho$ _remains non-negative_ on counters $I\subseteq[1,d]$
if $\mathit{cf}^{\prime}[I]\subseteq\mathbb{N}^{|I|}$ for all extended
configurations $\mathit{cf}^{\prime}$ on $\sigma$.

#### Dyck Language

Towards the $\mathsf{EXPSPACE}$ upper bound of Theorem 3.1, a first step is to
reduce the separability problem to a variant where one language is fixed to
the Dyck language. The Dyck language $\mathit{D}_{n}$ with $n$-letters is
defined over the alphabet $\Sigma_{n}=\\{a_{i},\bar{a}_{i}\;|\;i\in[1,n]\\}$.
It contains those words $w$ where, for every prefix $v$ with $w=v.u$, we have
at least as many letters $a_{i}$ as $\bar{a}_{i}$. Thus, the letters behave
like VASS counters and, indeed, the Dyck language is accepted by a single-
state VASS $\mathcal{D}_{n}$ with $n$ counters that increments the $i$-th
counter upon seeing letter $a_{i}$ and decrements the $i$-th counter upon
seeing $\bar{a}_{i}$. If a VASS is defined over the Dyck alphabet
$\Sigma_{n}$, we also call it $n$-visible. We will sometimes treat an
$n$-visible VASS of dimension $d$ as a $(d+n)$-dimensional VASS, and refer to
the additional $n$ counters as external. Note that this amounts to forming the
product with $\mathcal{D}_{n}$. Given a path $\rho$, we use $\exteff(\rho)$
for the effect on the external counters in this product construction.
Moreover, we write $\delta\varphi(\rho)$ to denote the combined effect on both
internal and external counters, i.e. the $(d+n)$-dimensional vector
$(\delta(\rho),\varphi(\rho))$.

To avoid an exponential blow-up, our reduction uses a variant of VASS whose
transitions are labeled by compressed words. Essentially, the reduction takes
$\mathcal{V}_{1}$ and $\mathcal{V}_{2}$ and produces a VASS $\mathcal{V}$ that
is a product of $\mathcal{V}_{1}$ and $\mathcal{V}_{2}$. Moreover, it acts on
its counters like $\mathcal{V}_{1}$; the input labels of $\mathcal{V}$
correspond to the counter updates of $\mathcal{V}_{2}$. Since the latter are
binary-encoded, the new VASS will have binary encoded input words. Let us make
this precise. A _label-compressed VASS_ (lcVASS) $\mathcal{V}$ is a VASS,
where the transitions are of the form $(p,a^{m},\delta,q)\in
Q\times\Sigma^{*}\times\mathbb{Z}^{d}\times Q$, where $a\in\Sigma$ and
$m\in\mathbb{N}$ is given in binary. Thus, for an lcVASS $\mathcal{V}$, we
define its _size_ as
$|\mathcal{V}|=|Q|+|F|+\sum_{(q,a^{m},\delta,q^{\prime})\in
T}(\log_{2}(m)+|\\!|\delta|\\!|_{2})$. The reduction that fixes the Dyck
language is captured by the following lemma.

######  Lemma 5.1 ([2, Lemma 3.4]).

Given $\mathcal{V}_{1}$ and $\mathcal{V}_{2}$ over $\Sigma$, we can compute in
time polynomial in $|\mathcal{V}_{1}|+|\mathcal{V}_{2}|$ an $n$-visible lcVASS
$\mathcal{V}$ so that
$\mathit{L}(\mathcal{V}_{1})\mathop{|}\mathit{L}(\mathcal{V}_{2})$ if and only
if $\mathit{L}(\mathcal{V})\mathop{|}\mathit{D}_{n}$. Here, $n$ is the
dimension of $\mathcal{V}_{2}$.

The polynomial time bound is not mentioned in [2], but the simple construction
they use (from [11]) clearly implies this bound. The latter separability
problem $\mathit{L}(\mathcal{V})\mathop{|}\mathit{L}(\mathit{D}_{n})$ has been
studied closely in [2] as well. They first show that $\mathcal{V}$ can be
transformed so as to make the language $\mathit{L}(\mathcal{V})$ pumpable. For
the resulting VASS, they show that
$\mathit{L}(\mathcal{V})\mathop{|}\mathit{L}(\mathit{D}_{n})$ holds if and
only if the so called Karp-Miller graph of $\mathsf{KM}(\mathcal{V})$ does not
contain an inseparability witness. Unfortunately, the transformation required
for pumpability involves another Karp-Miller graph construction, and therefore
does not fit into the space bound we aim for (said graph can be of
Ackermannian size in the worst case). Instead, we reformulate the witness.

######  Definition 5.2.

Let $\mathcal{V}$ be an $n$-visible $d$-dimensional VASS. An _inseparability
bloom_ for $\mathcal{V}$ is a tuple
$\usym{2740}=(q_{f},I,\alpha,\beta,\gamma)$ with $q_{f}$ a final state, loops
$\alpha$, $\beta$, $\gamma$ starting and ending in $q_{f}$, and a partition of
the counters $\Omega\uplus I=[1,d+n]$ so that

  1. (i)

for all $\rho=\alpha,\beta,\gamma$, we have $\delta\varphi(\rho)[I]\geq 0$,

  2. (ii)

$\delta(\alpha)+\delta(\beta)+\delta(\gamma)\geq 0$

  3. (iii)

$\varphi(\alpha)+\varphi(\beta)\geq 0$,

  4. (iv)

there is a $\mathit{t}\in\mathbb{Q}$ with
$\varphi(\alpha)+\varphi(\beta)+\varphi(\gamma)=\mathit{t}\cdot\varphi(\alpha)$.

The _size_ of the bloom is
$|\usym{2740}|=\log_{2}|Q|+|I|+|\alpha|+|\beta|+|\gamma|$.

A _stem for $\usym{2740}$_ is an extended run $\mathit{cf}.\sigma$ of the
product VASS $\mathcal{V}\times\mathcal{D}_{n}$ with the following properties:
It ends in an extended configuration $\mathit{cf}^{\prime}=(q_{f},\bm{m})$ for
some $\bm{m}\in{\rm Nature}_{\omega}^{d+n}$ with
$\Omega\subseteq\omega(\mathit{cf}^{\prime})$, and the counters in
$I\setminus\omega(\mathit{cf})$ remain non-negative when executing $\sigma$
from $\mathit{cf}$ resp. $\alpha$, $\beta$, and $\gamma$ from
$\mathit{cf}^{\prime}$.

An _inseparability flower_
$\mathop{\text{---}\\!\usym{2740}}=(\mathit{cf}.\sigma,\usym{2740})$ consists
of an inseparability bloom and a suitable stem. The size is
$|\mathop{\text{---}\\!\usym{2740}}|=|\\!|\mathit{cf}|\\!|_{1}+|\sigma|+|\usym{2740}|$.
The flower is _coverable_ if the extended configuration $\mathit{cf}$ is
coverable in the product VASS $\mathcal{V}\times\mathcal{D}_{n}$.

The following can be derived from the results in [2], refer to Appendix B for
the details.

######  Lemma 5.3.

Let $\mathcal{V}$ be $n$-visible. We have
$\mathit{L}(\mathcal{V})\mathop{\not|}\mathit{D}_{n}$ if and only if some
inseparability flower is coverable.

Our main result is the following. Note: the unary counter encoding strengthens
the bound.

######  Theorem 5.4.

If an inseparability flower is coverable in an $n$-visible lcVASS
$\mathcal{V}$ of dimension $d$, then there is one of size at most
$|\mathop{\text{---}\\!\usym{2740}}|=2^{|\mathcal{V}|^{\mathcal{O}((d+n)^{2})}}$.

#### Main algortihm

We now have all ingredients to formulate the algorithm that proves the upper
bounds in Theorem 3.1. We first describe the $\mathsf{EXPSPACE}$ upper bound.
Given $\mathcal{V}_{1}$ and $\mathcal{V}_{2}$ whose languages we wish to
separate, we first compute the lcVASS $\mathcal{V}$ using Lemma 5.1. This
takes poly time. The task is to check
$\mathit{L}(\mathcal{V})\mathop{|}\mathit{D}_{n}$, where $n$ is the dimension
of $\mathcal{V}_{2}$. Using Lemma 5.3, we have to find an inseparability
flower for $\mathcal{V}$ that is coverable. Theorem 5.4 bounds the size of the
flowers we have to consider. We thus use non-determinism to find a flower of
bounded size followed by a somewhat involved coverability check. Savitch’s
theorem [30] turns the non-deterministic algorithm into a deterministic one.

We detect a flower of bounded size as follows. We first guess the final state
$q_{f}\in F$ and the partitioning of the counters $I\uplus\Omega$. With this
information, we can guess the stem.

Towards obtaining a suitable stem, we start by guessing an extended
configuration $\mathit{cf}$, whose non-$\omega$-entries are at most doubly
exponentially large. We can store such configurations in exponential space. If
$\Omega\subseteq\omega(\mathit{cf})$ fails, we abort. We now guess a path
$\sigma$ of doubly exponential length from $\mathit{cf}$ to a configuration
$\mathit{cf}^{\prime}$. As we proceed, we store the length of the path, which
only needs exponential space. We abort, if one of the following happens while
guessing $\sigma$: a counter from $I\setminus\omega(\mathit{cf})$ becomes
negative, $\sigma$ becomes too long, or the last state on $\sigma$ is
different from $q_{f}$. If we have not aborted until now, we have determined
$\mathit{cf}.\sigma.\mathit{cf}^{\prime}$ that may serve as a stem for a bloom
with final state $q_{f}$ and partition $I\uplus\Omega$.

Given the stem, we can finish the construction of the bloom by guessing the
cycles $\rho=\alpha,\beta,\gamma$. The reason we proceed in this order is the
following. The cycles are too long to be stored in exponential space. Instead,
we check the non-negativity required by a stem on-the-fly, while constructing
the cycles. To do so, we need the configuration $\mathit{cf}^{\prime}$, which
we can store upon finishing the guess of $\sigma$ above. While guessing the
cycles, we store their length and the numbers $\inteff(\rho)$ and
$\exteff(\rho)$. It is readily checked that these numbers are bounded by

$\displaystyle 2^{|\mathcal{V}|}\cdot
2^{|\mathcal{V}|^{\mathcal{O}((d+n)^{2})}}=2^{|\mathcal{V}|^{\mathcal{O}((d+n)^{2})}}\
.$

This means we can store them in exponential space. We abort, if one of the
following applies: an intermediate valuation becomes negative on
$I\setminus\omega(\mathit{cf})$, the path becomes too long, or the last state
is different from $q_{f}$. We compute the operations and comparisons required
by (i) to (iv) in Definition 5.2. For (iv), we start with counter $d+1$ and
store the quotient
$\frac{\varphi(\alpha)[d+1]+\varphi(\beta)[d+1]+\varphi(\gamma)[d+1]}{\varphi(\alpha)[d+1]}$
as the rational number $\mathit{t}$. As the numerator and denominator will be
at most doubly exponential, we can store the number in exponential space. For
the remaining entries, we only perform the required comparison. As noted
above, they can be executed in polynomial time. If a comparison fails, we
reject. If we have not rejected up to now, we have determined an
inseparability flower while using space
$|\mathcal{V}|^{\mathcal{O}((d+n)^{2})}\leq
2^{|\mathcal{V}|\cdot\mathcal{O}((d+n)^{2})}=2^{\mathit{poly}(|\mathcal{V}_{1}|+|\mathcal{V}_{2}|)}$.

It remains to check whether this flower is coverable. There are two
challenges. First, since $\mathit{cf}$ is extended, we have a combination of a
simultaneous unboundedness and a coverability problem. Second, the
non-$\omega$-entries in $\mathit{cf}$ may be doubly exponentially large. We
reduce the problem to simultaneous unboundedness, which is in
$\mathsf{EXPSPACE}$ as shown by Demri [12, Theorem 4.6(I)]. The reduction uses
a simple gadget that subtracts the counter valuation to be covered and, if
succcessful, makes a new target counter $j$ unbounded. In the end we check
simultaneous unboundedness of $\omega(\mathit{cf})\cup\\{j\\}$. To handle the
large values, we utilize Lipton’s construction [24], which allows a VASS to
simulate $\mathsf{EXPSPACE}$-computations. As a remark, simultaneous
unboundedness cannot be expressed by a polynomial-sized formula in Yen’s logic
[34], a fact that was first observed in [12], which means we cannot just
invoke the bounds in [1].

For the $\mathsf{PSPACE}$ upper bound, we merely need to observe that in fixed
dimension, all our bounds on counter values become singly exponential.
Moreover, for the gadget that subtracts counter values, we do not need the
Lipton construction, as we can subtract exponentially bounded values directly
using transitions. Finally, in fixed dimension, the simultaneous unboundedness
check is also possible in $\mathsf{PSPACE}$, as shown by Demri [12, Theorem
4.6(II)].

The remainder of the paper proves Theorem 5.4. SNLS help us deal with
Constraint (iv).

##  6 Proof of Theorem 5.4

In this section we fix an $n$-visible lcVASS
$\mathcal{V}=(Q,q_{0},\Sigma_{n},T,F)$. Note that since $\mathcal{V}$ is
label-compressed, the effect on the external counters $\exteff(\rho)$ for a
path $\rho$ is also compressed. This matches the effect $\inteff(\rho)$, which
is anyway encoded in binary.

The proof is Rackoff-like, and we explain the analogy as we proceed. Like in
Rackoff’s upper bound for coverability [29], we reason over all (extended)
configurations. Unlike Rackoff, however, we do not look at short covering
sequences from a given configuration, but rather at small flowers rooted in
said configuration. To bound the size while maximizing over all
configurations, we measure each flower’s size without considering the
configuration it is rooted in. We therefore define the _flower bound_

$\displaystyle\mathcal{B}_{\mathcal{V}}\ =\
\max_{\mathit{cf}}\min\\{|\sigma|+|\usym{2740}|\;|\;(\mathit{cf}.\sigma,\usym{2740})\text{
is an inseparability flower}\\}\ .$

Theorem 5.4 is an immediate consequence of the following.

######  Lemma 6.1.

$\mathcal{B}_{\mathcal{V}}\leq 2^{|\mathcal{V}|^{\mathcal{O}((d+n)^{2})}}$.

#### Step I: From length bounds to flower size bounds

Before we prove Lemma 6.1, let us see how it implies Theorem 5.4. Notice that
Lemma 6.1 makes a statement about the lengths of the runs $\sigma$, $\alpha$,
$\beta$, $\gamma$, whereas Theorem 5.4 also promises a small starting
configuration $\mathit{cf}$. Thus, it remains to construct a small starting
configuration.

######  Proof 6.2 (Proof of Theorem 5.4).

To begin, assume
$\mathop{\text{---}\\!\usym{2740}}=(\mathit{cf}.\sigma,\usym{2740})$ is
coverable. By Lemma 6.1, there is another flower
$(\mathit{cf}.\sigma^{\prime},\usym{2740}^{\prime})$ that is rooted in the
same extended configuration and satisfies
$|\sigma^{\prime}|+|\usym{2740}^{\prime}|\leq\mathcal{B}_{\mathcal{V}}$. The
extended configuration $\mathit{cf}$ may not obey the desired bound. Thus, we
replace it by $\mathit{cf}^{\prime}$ defined by
$\omega(\mathit{cf}^{\prime})=\omega(\mathit{cf})$ and
$\mathit{cf}^{\prime}[\mathit{j}]=\min\\{\mathit{cf}[\mathit{j}],\mathcal{B}_{\mathcal{V}}\cdot
2^{|\mathcal{V}|}\\}$ for all $\mathit{j}\in I\setminus\omega(\mathit{cf})$.
Here, we keep the $\omega$-entries, and for each non-$\omega$-counter, we take
the value of $\mathit{cf}$ unless it is larger than
$\mathcal{B}_{\mathcal{V}}\cdot 2^{|\mathcal{V}|}$, in which case we truncate
to this value. We now claim that
$\mathop{\text{---}\\!\usym{2740}}^{\prime}=(\mathit{cf}^{\prime}.\sigma^{\prime},\usym{2740}^{\prime})$
is still a coverable inseparability flower, and its size is at most doubly
exponential (satisfying the desired bound). Coverability is immediate by
$\mathit{cf}^{\prime}\leq\mathit{cf}$. We also have
$|\\!|\mathit{cf}^{\prime}|\\!|_{1}\leq 2^{2^{\mathcal{O}(|\mathcal{V}|)}}$.
To be an inseparability flower, we have to check that the counters whose
values we truncated when moving from $\mathit{cf}$ to $\mathit{cf}^{\prime}$
remain non-negative while executing $\sigma$, and also $\sigma.\rho$ with
$\rho=\alpha,\beta,\gamma$. This, however, is clear by the fact that
$\sigma.\rho$ has length at most $\mathcal{B}_{\mathcal{V}}$, and each
transition can subtract at most $2^{|\mathcal{V}|}$ tokens. As we have this
budget available in $\mathit{cf}^{\prime}$, the run remains non-negative.

In the remainder of the section, we prove Lemma 6.1. Similar to Rackoff’s
proof for coverability, we generalize the notion of flowers to admit negative
counter values. Then we use an induction on the number of non-negative
counters to establish a bound on the length of shortest generalized flowers.
Let $\mathit{i}\in[0,d+n]$, $\usym{2740}=(q_{f},I,\alpha,\beta,\gamma)$ a
bloom, and $\Omega=[1,d+n]\setminus I$. We call an extended run
$\mathit{cf}.\sigma$ of $\mathcal{V}\times\mathcal{D}_{n}$ an _$\mathit{i}$
-stem for $\usym{2740}$_, if it ends in an extended configuration
$\mathit{cf}^{\prime}$ with $\mathit{cf}^{\prime}=(q_{f},\bm{m}^{\prime})$ for
some $\bm{m}^{\prime}$, $\Omega\subseteq\omega(\mathit{cf})$, and the counters
in $([1,\mathit{i}]\cap I)\setminus\omega(\mathit{cf})$ remain non-negative
when executing $\sigma$ from $\mathit{cf}$ resp. $\alpha$, $\beta$, and
$\gamma$ from $\mathit{cf}^{\prime}$ in $\mathcal{V}\times\mathcal{D}_{n}$.
Here, we use $[1,0]=\emptyset$. We call a pair
$(\mathit{cf}.\sigma,\usym{2740})$ consisting of an $\mathit{i}$-stem and an
inseparability bloom an _$\mathit{i}$ -inseparability flower_. Note that a
$(d+n)$-inseparability flower is an inseparability flower as in Definition
5.2. We say the flower is _$\mathit{b}$ -bounded_ with $\mathit{b}\in{\rm
Nature}\setminus\\{0\\}$, if the counters in $([1,\mathit{i}]\cap
I)\setminus\omega(\mathit{cf})$ are bounded by $\mathit{b}$ along
$\mathit{cf}.\sigma.\rho$ for all $\rho=\alpha,\beta,\gamma$. We wish to
establish an estimate on the following function $f$, note that
$\mathit{f}(d+n)=\mathcal{B}_{\mathcal{V}}$:

$\displaystyle\mathit{f}(\mathit{i})=\
\max_{\mathit{cf}}\min\\{|\sigma|+|\usym{2740}|\;|\;(\mathit{cf}.\sigma,\usym{2740})\text{
is an $\mathit{i}$-inseparability flower}\\}\ .$

#### Step II: From value bounds to length bounds

Similar to Rackoff’s proof, we will bound $f(i+1)$ in terms of $f(i)$, which
will then yield the bound on $\mathcal{B}_{\mathcal{V}}=f(n+d)$. However,
there is a key difference to Rackoff’s proof: When constructing runs that, in
the first $i+1$ coordinates stay non-negative, Rackoff argues that if such a
run only uses counter values in $[0,b]$ on the first $i+1$ coordinates, then
there is such a run of length at most $|Q|\cdot(b+1)^{i+1}$: whenever a
combination of values in $[0,b]$ (and a control state) repeats, we can cut out
the infix in between. Hence, _value bounds yield length bounds_. Our setting
requires a different argument: Simply cutting out infixes in
$\alpha,\beta,\gamma$ might spoil the properties (ii), (iii), and (iv) of
$i$-inseparability flowers. Instead, we use our results on SNLS to obtain
length bounds from value bounds. The technique is similar to some other
generalizations of Rackoff’s result by Yen [34, Lemma 3.5] Habermehl [14,
Lemma 3.2] and Atig and Habermehl [1, Lemma 5]. However, the following proof
also needs to work with non-linear constraints (which are also not present in
Demri’s extension of Rackoff’s result [12]).

######  Lemma 6.3.

Let $\mathop{\text{---}\\!\usym{2740}}=(\mathit{cf}.\sigma,\usym{2740})$ be a
$\mathit{b}$-bounded $\mathit{i}$-inseparability flower. Then there is an
$\mathit{i}$-inseparability flower
$\mathop{\text{---}\\!\usym{2740}}^{\prime}=(\mathit{cf}.\sigma^{\prime},\usym{2740}^{\prime})$
with
$|\sigma^{\prime}|+|\usym{2740}^{\prime}|\leq(2^{|\mathcal{V}|}\cdot|Q|\cdot\mathit{b})^{\mathcal{O}((d+n)^{6})}$.

######  Proof 6.4.

Let $\mathop{\text{---}\\!\usym{2740}}=(\mathit{cf}.\sigma,\usym{2740})$ be a
$\mathit{b}$-bounded $\mathit{i}$-inseparability flower with
$\usym{2740}=(q_{f},I,\alpha,\beta,\gamma)$. Let $\Omega$ be the complement of
$I$. Let $\widehat{\mathit{cf}}$ be the extended configuration reached by
$\mathit{cf}.\sigma$.

Let $\mathit{D}=([1,\mathit{i}]\cap I)\setminus\omega(\mathit{cf})$ be the
counters we wish to keep non-negative. By a _$\mathit{D}$ -loop_, we mean an
extended run $\mathit{cf}_{1}.\tau.\mathit{cf}_{2}$ of
$\mathcal{V}\times\mathcal{D}_{n}$ where $\tau$ is a loop,
$\mathit{cf}_{1}[\mathit{D}]=\mathit{cf}_{2}[\mathit{D}]$, and
$\mathit{cf}_{1}[\Omega]=\mathit{cf}_{2}[\Omega]$. The $\mathit{D}$-loop is
called _irreducible_ if it does not contain further $\mathit{D}$-loops. By the
pigeonhole principle, any run that is longer than
$\mathit{u}_{\mathit{len}}=|Q|\cdot(\mathit{b}+1)^{|\mathit{D}\cup\Omega|}$
contains a $\mathit{D}$-loop. This means the length of an irreducible
$\mathit{D}$-loop is at most $\mathit{u}_{\mathit{len}}$. Moreover, these
loops can have at most $2\cdot
2^{|\mathcal{V}|}\cdot\mathit{u}_{\mathit{len}}$ distinct effects on each
counter, where the leading $2$ is for the distinction between positive and
negative values. This analysis yields an upper bound of
$\mathit{u}_{\mathit{num}}=(2^{|\mathcal{V}|+1}\cdot\mathit{u}_{\mathit{len}})^{d+n}$
on the number of irreducible $\mathit{D}$-loops with distinct effects. We show
how to construct a flower as promised in the lemma.

We begin by cutting out irreducible $\mathit{D}$-loops from $\sigma$, yielding
$\sigma^{\prime}$ of length at most $\mathit{u}_{\mathit{len}}$. The extended
configuration $\mathit{cf}^{\prime}$ reached by $\mathit{cf}.\sigma^{\prime}$
coincides with $\widehat{\mathit{cf}}$ on the $\omega$-entries and on the
non-$\omega$-entries for $\mathit{D}$.

Next, we want to shorten $\rho=\alpha,\beta,\gamma$. To this end, we first
decompose them into irreducible $\mathit{D}$-loops. We assume all such
$\mathit{D}$-loops have distinct effects, otherwise we pick a representative.
With the previous analysis, the result is
$\rho_{0},\rho_{1},\ldots,\rho_{\mathit{v}}$ with
$\mathit{v}\leq\mathit{u}_{\mathit{num}}$. Here, $\rho_{0}$ is the loop on the
final state into which the irreducible $\mathit{D}$-loops
$\rho_{1},\ldots,\rho_{\mathit{v}}$ are inserted. Note that $\rho_{0}$ is not
necessarily a $\mathit{D}$-loop. What we know, however, is that $\rho_{0}$ has
a non-negative effect on the counters in $I$, due to Condition (i) in the
definition of inseparability blooms. Since we want to be able to insert all
the $\mathit{D}$-loops directly into $\rho_{0}$, the latter should still
contain the same starting configurations for such loops as $\rho$, at least
when only considering the counters in $\mathit{D}\cup\Omega$. Therefore we
cannot guarantee that $\rho_{0}$ contains no $\mathit{D}$-loops, because
cutting all of them out might reduce the number of such configurations visited
by $\rho_{0}$. However, $\rho_{0}$ still has length at most
$\mathit{u}_{\mathit{len}}^{2}$ by the following argument. If we mark in
$\rho_{0}$ the first occurrence of each element from
$Q\times[0,b]^{\mathit{D}\cup\Omega}$, then each infix leading from one such
marker to the next has at most length $\mathit{u}_{\mathit{len}}$, because
longer infixes still contain a $\mathit{D}$-loop that has no marked
configuration and can therefore be removed. Since there are at most
$|Q\times[0,\mathit{b}]^{\mathit{D}\cup\Omega}|=|Q|\cdot(\mathit{b}+1)^{|\mathit{D}\cup\Omega|}=\mathit{u}_{\mathit{len}}$
markers, we obtain the stated length bound of $\mathit{u}_{\mathit{len}}^{2}$
for $\rho_{0}$.

A vector $\bm{x}\in{\rm Nature}^{\mathit{v}}$ with $\bm{x}[0]>0$ and
$\bm{x}[\mathit{j}]\geq 0$ for $1\leq j\leq\mathit{v}$ can now be turned into
a run $\rho_{\bm{x}}$ by glueing together $\bm{x}[\mathit{j}]$-many instances
of $\rho_{\mathit{j}}$. Note that also the base loop $\rho_{0}$ may be
repeated. As the order of the transitions does not influence the effect of the
run, $\delta\varphi(\rho)=\delta\varphi(\rho_{\bm{y}})$ holds, where
$\bm{y}=\Psi(\rho)$ is the so-called Parikh vector that counts the occurrences
of irreducible loops in $\rho$. As a consequence, we can directly define the
effect on the vector $\bm{x}$, namely
$\delta\varphi(\bm{x})=\sum_{i=0}^{\mathit{v}}\bm{x}[\mathit{j}]\cdot\delta\varphi(\rho_{\mathit{j}})\in\mathbb{Z}^{d+n}$.

With irreducible $\mathit{D}$-loops at hand, we can formulate the search for a
small bloom as an SNLS. We define the vectors
$\bm{x}_{\alpha},\bm{x}_{\beta},\bm{x}_{\gamma}$, and the following
constraints:

$\displaystyle\bm{x}_{\alpha}[0],\bm{x}_{\beta}[0],\bm{x}_{\gamma}[0]\geq$
$\displaystyle\ 1\qquad$
$\displaystyle\qquad\delta(\bm{x}_{\alpha}+\bm{x}_{\beta}+\bm{x}_{\gamma})[1,d]\geq$
$\displaystyle\ 0$
$\displaystyle\bm{x}_{\alpha},\bm{x}_{\beta},\bm{x}_{\gamma}\geq$
$\displaystyle\ 0$
$\displaystyle\varphi(\bm{x}_{\alpha}+\bm{x}_{\beta})[d+1,d+n]\geq$
$\displaystyle\ 0$
$\displaystyle\delta\varphi(\bm{x}_{\alpha})[I],\delta\varphi(\bm{x}_{\beta})[I],\delta\varphi(\bm{x}_{\gamma})[I]\geq$
$\displaystyle\ 0$
$\displaystyle(\varphi(\bm{x}_{\alpha}+\bm{x}_{\beta}+\bm{x}_{\gamma})-\mathit{t}\cdot\varphi(\bm{x}_{\alpha}))[d+1,d+n]=$
$\displaystyle\ 0$

The constraints on the left say that we repeat the base loops at least once,
and the remaining loops a non-negative number of times. The last constraint is
Condition (i) in the definition of blooms. The constraints on the right
correspond to the Conditions (ii) to (iv).

It is readily checked that $(\Psi(\alpha),\Psi(\beta),\Psi(\gamma))$ solves
the SNLS. This means Theorem 3.2 applies and yields a small rational solution.
To turn it into an integer solution, we observe that our SNLS is monotonic in
the sense that if $(\bm{x}_{\alpha},\bm{x}_{\beta},\bm{x}_{\gamma})$ is a
solution, so is $(k\bm{x}_{\alpha},k\bm{x}_{\beta},k\bm{x}_{\gamma})$ for any
$k\geq 1$. We multiply the rational solution by the common denominator to
obtain the integer solution
$(\bm{x}_{\alpha}^{\prime},\bm{x}_{\beta}^{\prime},\bm{x}_{\gamma}^{\prime})$
with the associated loops $\alpha^{\prime},\beta^{\prime},\gamma^{\prime}$.

We argue that
$\mathop{\text{---}\\!\usym{2740}}^{\prime}=(\mathit{cf}.\sigma^{\prime},\usym{2740}^{\prime})$
with
$\usym{2740}^{\prime}=(q_{f},I,\alpha^{\prime},\beta^{\prime},\gamma^{\prime})$
is an $\mathit{i}$-inseparability flower. Remember that $\mathit{cf}^{\prime}$
is the configuration reached by $\mathit{cf}.\sigma^{\prime}$. As
$\mathit{cf}$ and $I$ have not changed, the only thing we have to show is the
non-negativity for the counters in $\mathit{D}$. For $\sigma^{\prime}$, this
follows from the non-negativity of $\sigma$, and the fact that we only cut-out
$\mathit{D}$-loops. For
$\rho^{\prime}=\alpha^{\prime},\beta^{\prime},\gamma^{\prime}$, which are
executed from $\mathit{cf}^{\prime}$, we argue as follows. The base loop
$\rho_{0}$ has the same effect on the $\mathit{D}$-counters as $\rho$, because
we obtained $\rho_{0}$ by cutting-out $\mathit{D}$-loops from $\rho$. The
effect of $\rho$ on even the entire set $I$ is non-negative due to Condition
(i) for blooms. This means if one repetition of $\rho_{0}$ stays non-negative
from $\mathit{cf}^{\prime}$, arbitrarily many repetitions will. The one
repetition stays non-negative, because $\rho$ was non-negative from
$\widehat{\mathit{cf}}$ (the extended configuration reached by
$\mathit{cf}.\sigma$), and $\mathit{cf}^{\prime}$ coincides with
$\widehat{\mathit{cf}}$ on $\mathit{D}$. Since the $\mathit{D}$-loops that we
glue into $\rho_{0}$ come with a valuation of the counters in $\mathit{D}$,
and this valuation keeps them non-negative in $\rho$, the entire
$\rho^{\prime}$ stays non-negative.

We analyze the complexity of our system $\mathcal{S}$. It has at most
$\mathit{row}(\mathcal{S})\in\mathcal{O}(d+n)$ many rows, and note that the
non-negativity constraints do not count towards the rows. There are at most
$\mathit{col}(\mathcal{S})\in\mathcal{O}(\mathit{u}_{\mathit{num}})$ many
columns. The degree is $\deg(\mathcal{S})=1$. The maximal coefficient is
bounded from above by the largest possible loop effect,
$\operatorname{maxc}(\mathcal{S})\leq
2^{|\mathcal{V}|}\cdot\mathit{u}_{\mathit{len}}^{2}$. Then, Theorem 3.2 gives
us rational solutions $\bm{x}_{\alpha},\bm{x}_{\beta},\bm{x}_{\gamma}$ of the
form $\bm{x}_{\rho}[i]=\dfrac{a}{K}$, meaning $K$ is the common denominator of
all entries, with

$\displaystyle|\\!|\bm{x}_{\rho}|\\!|_{1}\in$ $\displaystyle\
(\mathit{col}(\mathcal{S})\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(\deg(\mathcal{S})^{2}\cdot\mathit{row}(\mathcal{S})^{4})}$
$\displaystyle=$ $\displaystyle\ (\mathcal{O}(\mathit{u}_{\mathit{num}})\cdot
2^{|\mathcal{V}|}\cdot\mathit{u}_{\mathit{len}}^{2})^{\mathcal{O}((d+n)^{4})}$
$\displaystyle=$ $\displaystyle\
(\mathcal{O}((2^{|\mathcal{V}|+1}\cdot\mathit{u}_{\mathit{len}})^{d+n})\cdot
2^{|\mathcal{V}|}\cdot\mathit{u}_{\mathit{len}}^{2})^{\mathcal{O}((d+n)^{4})}$
$\displaystyle=$ $\displaystyle\
(2^{|\mathcal{V}|}\cdot\mathit{u}_{\mathit{len}})^{\mathcal{O}((d+n)^{5})}=\
(2^{|\mathcal{V}|}\cdot|Q|\cdot(\mathit{b}+1))^{\mathcal{O}((d+n)^{6})}$
$\displaystyle=$ $\displaystyle\
(2^{|\mathcal{V}|}\cdot|Q|\cdot\mathit{b})^{\mathcal{O}((d+n)^{6})}\ .$

We already argued that the integer vectors $K\bm{x}_{\alpha}$,
$K\bm{x}_{\beta}$, $K\bm{x}_{\gamma}$ are also solutions with runs
$\alpha^{\prime},\beta^{\prime},\gamma^{\prime}$. Since each entry of these
vectors is smaller than
$(2^{|\mathcal{V}|}\cdot|Q|\cdot\mathit{b})^{\mathcal{O}((d+n)^{6})}$, and we
have at most
$\mathit{u}_{\mathit{num}}=(2^{|\mathcal{V}|}\cdot|Q|\cdot(\mathit{b}+1))^{\mathcal{O}((d+n)^{2})}$
many loops with maximal size
$\mathit{u}_{\mathit{len}}^{2}=|Q|^{2}\cdot(\mathit{b}+1)^{2(d+n)}$, we get

$\displaystyle|\rho^{\prime}|$
$\displaystyle\leq(2^{|\mathcal{V}|}\cdot|Q|\cdot\mathit{b})^{\mathcal{O}((d+n)^{6})}\cdot(2^{|\mathcal{V}|}\cdot|Q|\cdot(\mathit{b}+1))^{\mathcal{O}((d+n)^{2})}\cdot|Q|^{2}\cdot(\mathit{b}+1)^{2(d+n)}$
$\displaystyle=(2^{|\mathcal{V}|}\cdot|Q|\cdot\mathit{b})^{\mathcal{O}((d+n)^{6})}\
.$

#### Step III: Rackoff-style induction

We now give the bound on $\mathit{f}(\mathit{i})$ that we need to prove Lemma
6.1. In the base case, no counter has to remain non-negative and so we have a
$1$-bounded $0$-inseparability flower. We employ the bound from Lemma 6.3.

######  Lemma 6.5.

$\mathit{f}(0)=(2^{|\mathcal{V}|}|Q|)^{\mathcal{O}((d+n)^{6})}$.

In the induction step, and as in Rackoff’s result, the bound takes the form of
a recurrence.

######  Lemma 6.6.

$\mathit{f}(i+1)\leq(2^{|\mathcal{V}|}\cdot\mathit{f}(\mathit{i}))^{\mathcal{O}((d+n)^{6})}$.

######  Proof 6.7.

Consider an $(\mathit{i}+1)$-inseparability flower
$\mathop{\text{---}\\!\usym{2740}}=(\mathit{cf}.\sigma,\usym{2740})$ with
$\usym{2740}=(q_{f},I,\alpha,\beta,\gamma)$ and $\Omega=[1,d+n]\setminus I$.
Let $\mathit{r}(\mathit{i})=2^{|\mathcal{V}|}\cdot\mathit{f}(\mathit{i})$
serve as an abbreviation. We proceed by a case distinction. If
$\mathop{\text{---}\\!\usym{2740}}$ is $\mathit{r}(\mathit{i})$-bounded, then
Lemma 6.3 provides another $(\mathit{i}+1)$-inseparability flower
$(\mathit{cf}.\sigma^{\prime},\usym{2740}^{\prime})$ with
$|\sigma^{\prime}|+|\usym{2740}^{\prime}|\leq(2^{|\mathcal{V}|}\cdot|Q|\cdot\mathit{r}(\mathit{i}))^{\mathcal{O}((d+n)^{6})}=(2^{|\mathcal{V}|}\cdot\mathit{f}(\mathit{i}))^{\mathcal{O}((d+n)^{6})}$.
This satisfies the bound stated in the lemma.

If $\mathop{\text{---}\\!\usym{2740}}$ is not
$\mathit{r}(\mathit{i})$-bounded, then $\sigma.\rho$ with
$\rho=\alpha,\beta,\gamma$ exceeds $\mathit{r}(i)$. We identify the first
moment when this happens, say after $\rho_{1}$ and for the $(i+1)$-th counter.
The case where the run exceeds the bound already in $\sigma$ is simpler. The
run decomposes into

$\displaystyle\mathit{cf}\xrightarrow{\sigma}\mathit{cf}_{1}\xrightarrow{\rho_{1}}\mathit{cf}^{\prime}\xrightarrow{\rho_{2}}\mathit{cf}_{2}\
.$

We argue that also $(\mathit{cf}^{\prime}.\rho_{2},\usym{2740})$ is an
$(\mathit{i}+1)$-flower, which means $\mathit{cf}^{\prime}.\rho_{2}$ is an
$(\mathit{i}+1)$-stem for $\usym{2740}$. Since $\rho$ is a loop, it returns to
$q_{f}$. We have $\omega(\mathit{cf})=\omega(\mathit{cf}^{\prime})$ and since
$\Omega\subseteq\omega(\mathit{cf})$, we get
$\Omega\subseteq\omega(\mathit{cf}^{\prime})$. As $\usym{2740}$ is a bloom,
$\rho$ has a non-negative effect on the counters in $I$. This means
$\mathit{cf}_{1}[I]\leq\mathit{cf}_{2}[I]$, and so the counters in
$([1,\mathit{i}+1]\cap I)\setminus\omega(\mathit{cf}^{\prime})$ remain non-
negative when executing $\alpha$, $\beta$, $\gamma$ from $\mathit{cf}_{2}$ as
they did from $\mathit{cf}_{1}$. Also $\rho_{2}$ remains non-negative from
$\mathit{cf}^{\prime}$, because $\rho$ remained non-negative from
$\mathit{cf}_{1}$.

Since $(\mathit{cf}^{\prime}.\rho_{2},\usym{2740})$ is an
$(\mathit{i}+1)$-flower, it is an $\mathit{i}$-flower. The induction
hypothesis yields another $\mathit{i}$-flower
$\mathop{\text{---}\\!\usym{2740}}^{\prime}=(\mathit{cf}^{\prime}.\sigma^{\prime},\usym{2740}^{\prime})$
with $|\sigma^{\prime}|+|\usym{2740}^{\prime}|\leq\mathit{f}(\mathit{i})$. Let
$\usym{2740}^{\prime}=(q_{f}^{\prime},I^{\prime},\alpha^{\prime},\beta^{\prime},\gamma^{\prime})$
and let $\Omega^{\prime}$ be the complement of $I^{\prime}$.

We argue that $\mathop{\text{---}\\!\usym{2740}}^{\prime}$ is actually an
$(\mathit{i}+1)$-flower. If the counter $i+1$ that exceeds the bound
$\mathit{r}(\mathit{i})$ does not belong to $I^{\prime}$, there is nothing to
show. Otherwise, even
$\sigma^{\prime}.\alpha^{\prime}.\beta^{\prime}.\gamma^{\prime}$ in succession
could subtract at most $\mathit{f}(\mathit{i})\cdot
2^{|\mathcal{V}|}=\mathit{r}(\mathit{i})$ tokens from counter $i+1$. Since
this counter carries more than $\mathit{r}(\mathit{i})$ tokens, this leaves us
with a positive balance.

We show that also
$(\mathit{cf}.\sigma.\rho_{1}.\sigma^{\prime},\usym{2740}^{\prime})$ is an
$(\mathit{i}+1)$-flower, meaning $\mathit{cf}.\sigma.\rho_{1}.\sigma^{\prime}$
is an $(\mathit{i}+1)$-stem for $\usym{2740}^{\prime}$. We have
$\omega(\mathit{cf})=\omega(\mathit{cf}^{\prime})$ and so
$\Omega^{\prime}\subseteq\omega(\mathit{cf}^{\prime})$ implies
$\Omega^{\prime}\subseteq\omega(\mathit{cf})$. It remains to show that the
counters in $([1,\mathit{i}+1]\cap I^{\prime})\setminus\omega(\mathit{cf})$
remain non-negative. Consider the prefix $\sigma.\rho_{1}$ executed from
$\mathit{cf}$. For the counters that also belong to $I$, non-negativity holds
as $\mathop{\text{---}\\!\usym{2740}}$ is an $(i+1)$-flower. Assume there was
a counter in $([1,\mathit{i}+1]\cap I^{\prime})\setminus\omega(\mathit{cf})$
that did not belong to $I$. Then it belonged to $\Omega$. But as
$\Omega\subseteq\omega(\mathit{cf})$, we had a contradiction. For the suffix
$\sigma^{\prime}$ executed from $\mathit{cf}^{\prime}$, and for
$\alpha^{\prime},\beta^{\prime},\gamma^{\prime}$, non-negativity holds as
$\mathop{\text{---}\\!\usym{2740}}^{\prime}$ is an $(\mathit{i}+1)$-flower.

To estimate the size of the newly constructed flower rooted in $\mathit{cf}$,
we assume $\sigma.\rho_{1}$ does not repeat configurations on the first
$(\mathit{i}+1)$-counters. If it does, we cut out the infix and adapt the
values of the counters that are allowed to fall below zero. Then the length of
$\sigma.\rho_{1}$ is bounded by
$|Q|\cdot\mathit{r}(\mathit{i})^{\mathit{i}+1}$, and we have

$\displaystyle|\sigma.\rho_{1}.\sigma^{\prime}|+|\usym{2740}^{\prime}|\leq$
$\displaystyle\
|Q|\cdot\mathit{r}(\mathit{i})^{\mathit{i}+1}+\mathit{f}(\mathit{i})\leq\
(2^{|\mathcal{V}|}\cdot\mathit{f}(\mathit{i}))^{\mathcal{O}(\mathit{i}+1)}\leq(2^{|\mathcal{V}|}\cdot\mathit{f}(\mathit{i}))^{\mathcal{O}((d+n)^{6})}\
.$

It remains to solve the recurrence. Let $a=2^{|\mathcal{V}|}$ and
$b=\mathcal{O}((d+n)^{6})$. We have

$\displaystyle\mathit{f}(d+n)=(a\ldots(a\cdot\mathit{f}(0))^{b}\ldots)^{b}\leq(a^{d+n}\cdot\mathit{f}(0))^{b^{d+n}}\
.$

Since $\mathit{f}(0)=(2^{|\mathcal{V}|}\cdot|Q|)^{\mathcal{O}((d+n)^{6})}$, we
obtain the promised $\mathcal{B}_{\mathcal{V}}=\mathit{f}(d+n)\leq
2^{|\mathcal{V}|^{\mathcal{O}((d+n)^{2})}}$.

pages main.pages.ctrpages pages0 pages

## References

  * [1] M. F. Atig and P. Habermehl.  On Yen’s path logic for Petri nets.  Int. J. Found. Comput. Sci., 22(4):783–799, 2011.  doi:10.1142/S0129054111008428.
  * [2] P. Baumann, R. Meyer, and G. Zetzsche.  Regular separability in Büchi VASS.  In Proc. STACS, volume 254 of LIPIcs, pages 9:1–9:19. Schloss Dagstuhl, 2023.  doi:10.4230/LIPICS.STACS.2023.9.
  * [3] Pascal Baumann, Roland Meyer, and Georg Zetzsche.  Regular separability in Büchi VASS.  CoRR, abs/2301.11242, 2023.  arXiv:2301.11242, doi:10.48550/ARXIV.2301.11242.
  * [4] M. Blockelet and S. Schmitz.  Model checking coverability graphs of vector addition systems.  In Proc. MFCS, volume 6907 of LNCS, pages 108–119. Springer, 2011.  doi:10.1007/978-3-642-22993-0_13.
  * [5] L. Clemente, W. Czerwiński, S. Lasota, and C. Paperman.  Regular separability of parikh automata.  In Proc. ICALP, volume 80 of LIPIcs, pages 117:1–117:13. Schloss Dagstuhl, 2017.  doi:10.4230/LIPICS.ICALP.2017.117.
  * [6] L. Clemente, W. Czerwiński, S. Lasota, and C. Paperman.  Separability of reachability sets of vector addition systems.  In H. Vollmer and B. Vallée, editors, Proc. STACS, volume 66 of LIPIcs, pages 24:1–24:14. Schloss Dagstuhl, 2017.  doi:10.4230/LIPICS.STACS.2017.24.
  * [7] W. Czerwiński and P. Hofman.  Language inclusion for boundedly-ambiguous vector addition systems is decidable.  In Proc. CONCUR, volume 243 of LIPIcs, pages 16:1–16:22. Schloss Dagstuhl, 2022.  doi:10.4230/LIPICS.CONCUR.2022.16.
  * [8] W. Czerwiński, P. Hofman, and G. Zetzsche.  Unboundedness problems for languages of vector addition systems.  In Proc. ICALP, volume 107 of LIPIcs, pages 119:1–119:15. Schloss Dagstuhl, 2018.  doi:10.4230/LIPICS.ICALP.2018.119.
  * [9] W. Czerwiński and S. Lasota.  Regular separability of one counter automata.  Log. Methods Comput. Sci., 15(2), 2019.  doi:10.23638/LMCS-15(2:20)2019.
  * [10] W. Czerwiński, S. Lasota, R. Meyer, S. Muskalla, K. N. Kumar, and P. Saivasan.  Regular separability of well-structured transition systems.  In Proc. CONCUR, volume 118 of LIPIcs, pages 35:1–35:18. Schloss Dagstuhl, 2018.  doi:10.4230/LIPICS.CONCUR.2018.35.
  * [11] W. Czerwiński and G. Zetzsche.  An approach to regular separability in vector addition systems.  In Proc. LICS, pages 341–354. ACM, 2020.  doi:10.1145/3373718.3394776.
  * [12] S. Demri.  On selective unboundedness of VASS.  JCSS, 79(5):689–713, 2013.  doi:10.1016/J.JCSS.2013.01.014.
  * [13] E. M. Gurari and O. H. Ibarra.  An NP-complete number-theoretic problem.  J. ACM, 26(3):567–581, 1979.  doi:10.1145/322139.322152.
  * [14] P. Habermehl.  On the complexity of the linear-time $\mu$-calculus for Petri Nets.  In Proc. ICATPN, volume 1248 of LNCS, pages 102–116. Springer, 1997.  doi:10.1007/3-540-63139-9_32.
  * [15] R. M. Karp and R. E. Miller.  Parallel program schemata.  JCSS, 3(2):147–195, 1969.  doi:10.1016/S0022-0000(69)80011-5.
  * [16] E. Keskin and R. Meyer.  Separability and non-determinizability of WSTS.  In Proc. CONCUR, volume 279 of LIPIcs, pages 8:1–8:17. Schloss Dagstuhl, 2023.  doi:10.4230/LIPICS.CONCUR.2023.8.
  * [17] E. Keskin and R. Meyer.  On the separability problem of VASS reachability languages.  In To appear in Proc. of LICS, 2024.
  * [18] C. Köcher and G. Zetzsche.  Regular separators for VASS coverability languages.  In Proc. FSTTCS, volume 284 of LIPIcs, pages 15:1–15:19. Schloss Dagstuhl, 2023.  doi:10.4230/LIPICS.FSTTCS.2023.15.
  * [19] S. R. Kosaraju.  Decidability of reachability in vector addition systems (preliminary version).  In Proc. STOC, pages 267–281. ACM, 1982.  doi:10.1145/800070.802201.
  * [20] J.-L. Lambert.  A structure to decide reachability in Petri nets.  Theor. Comput. Sci., 99(1):79–104, 1992.  doi:10.1016/0304-3975(92)90173-D.
  * [21] S. Lang.  Algebra, Rev. 3rd Ed. Springer, New York, 2002.
  * [22] J. Leroux.  Vector addition system reachability problem: a short self-contained proof.  In Proc. POPL, pages 307–316. ACM, 2011.  doi:10.1145/1926385.1926421.
  * [23] J. Leroux and S. Schmitz.  Demystifying reachability in vector addition systems.  In Proc. LICS, pages 56–67. IEEE Computer Society, 2015.  doi:10.1109/LICS.2015.16.
  * [24] R. J. Lipton.  The reachability problem requires exponential space.  Technical Report 63, Yale University, 1976.
  * [25] Angus Macintyre, Kenneth McKenna, and Lou van den Dries.  Elimination of quantifiers in algebraic structures.  Advances in Mathematics, 47(1):74–87, 1983.  doi:10.1016/0001-8708(83)90055-5.
  * [26] D. Marker.  Model Theory: An Introduction.  Springer, New York, 2002.
  * [27] E. W. Mayr.  An algorithm for the general Petri net reachability problem.  SIAM J. Comput., 13(3):441–460, 1984.  doi:10.1137/0213029.
  * [28] B. Mishra.  Algorithmic Algebra.  Texts and Monographs in Computer Science. Springer, 1993.  doi:10.1007/978-1-4612-4344-1.
  * [29] C. Rackoff.  The covering and boundedness problems for vector addition systems.  Theor. Comput. Sci., 6:223–231, 1978.  doi:10.1016/0304-3975(78)90036-1.
  * [30] W. J. Savitch.  Relationships between nondeterministic and deterministic tape complexities.  JCSS, 4(2):177–192, 1970.  doi:10.1016/S0022-0000(70)80006-X.
  * [31] A. Schrijver.  Theory of linear and integer programming.  John Wiley & Sons, 1986.
  * [32] R. S. Thinniyam and G. Zetzsche.  Regular separability and intersection emptiness are independent problems.  In Proc. FSTTCS, volume 150 of LIPIcs, pages 51:1–51:15. Schloss Dagstuhl, 2019.  doi:10.4230/LIPICS.FSTTCS.2019.51.
  * [33] V. Weispfenning.  The complexity of almost linear diophantine problems.  J. Symb. Comput., 10(5):395–404, 1990.  doi:10.1016/S0747-7171(08)80051-X.
  * [34] H.-C. Yen.  A unified approach for deciding the existence of certain Petri net paths.  Information and Computation, 96(1):119–137, 1992.  doi:10.1016/0890-5401(92)90059-O.

todos main.todos.ctrtodos todos0 todos

pagestotal main.pagestotal.ctrpagestotal pagestotal0 pagestotal

##  Appendix A Additional material on Section 4

We continue our notation $n=\mathit{col}(\bm{A}(x))$ and
$m=\mathit{row}(\bm{A}(x))$ from the main paper. In contexts like $\deg(-)$,
$\operatorname{maxc}(-)$, etc. we ommit the parameter $x$ where convenient.
For example we write $\deg(\bm{A})$ instead of $\deg(\bm{A}(x))$.

###  A.1 Precise bounds for Theorem 4.2

Here, we prove that the DNFLB $\Phi$ constructed in Equation 4 satisfies the
bounds promised in Theorem 4.2.

To that end, it suffices to compute for all $R$ the maximal degrees and
maximal coefficients of the terms $\det(\bm{D}_{R}(x))$,
$\bm{D}(x)\cdot\operatorname{adj}(\bm{D}_{R}(x))\cdot\bm{c}_{R}(x)$, and
$\det(\bm{D}_{R}(x))\cdot\bm{c}(x)$. Let $d_{R,i,j}(x)$ be the entry in the
$i$-th row and $j$-th column of $\bm{D}_{R}(x)$. Further let $[1,n]=P\uplus Q$
where $Q$ is the set of row indices $i<n$ for which a $j_{i}<n$ exists with
$d_{R,i,j_{i}}=1$ and $d_{R,i,j}=0$ for all $j\neq j_{i}$. We construct
$\bm{D}_{R}(x)$ by first augmenting $\bm{A}$ by $n$ rows of the form
$(\ldots,1,\ldots)$ with exactly one non-zero component, and then choosing
$|R|=n$ rows. This implies $|P|\leq m$. We recall Leibniz’ formula for
computing the determinant $\det(\bm{D}_{R}(x))=\sum_{\sigma\in
S_{n}}\operatorname{sgn}(\sigma)\cdot\prod_{i=1}^{n}d_{R,i,\sigma(i)}$. Define
$T=\\{\sigma\in S_{n}\;|\;\forall i\in Q.\;\sigma(i)=j_{i}\\}$, where $j_{i}$
is the non-zero valued column of the $i$-th row in $\bm{D}_{R}$. We observe
that if $\sigma\in S_{n}$ with $\sigma(i)\neq j_{i^{\prime}}$ for some
$i^{\prime}\in Q$, then $\prod_{i=1}^{n}d_{R,i,\sigma(i)}=0$ because it
contains the operand $d_{R,i^{\prime},j_{i^{\prime}}}=0$. Then,

$\sum_{\sigma\in
S_{n}}\operatorname{sgn}(\sigma)\cdot\prod_{i=1}^{n}d_{R,i,\sigma(i)}=\sum_{\sigma\in
T}\operatorname{sgn}(\sigma)\cdot\prod_{i=1}^{n}d_{R,i,\sigma(i)}=\sum_{\sigma\in
T}\operatorname{sgn}(\sigma)\cdot\prod_{i\in P}d_{R,i,\sigma(i)}.$

The latter equality follows from the fact that $\sigma(i)=j_{i}$ for all
$\sigma\in T$ and $i\in Q$, where we have $d_{R,i,j_{i}}=1$ by definition of
$Q$. The formula shows
$\deg(\det(\bm{D}_{R}(x)))\leq|P|\cdot\deg(\mathcal{S}^{\prime})\leq
m\cdot\deg(\mathcal{S}^{\prime})$. Because $\sigma(i)=j_{i}$ for all
$\sigma\in S_{n}$ and $i\in Q$, this fixes the images of all but $|P|$ inputs.
Since $\sigma\in T$ are permutations, we can conclude $|T|=|P|!\leq m!$.
Regarding the maximal coefficient, note that each polynomial $d_{R,i,j}(x)$ is
an additive term of at most $\deg(\bm{D}_{R}(x))+1$ monomials, each with a
potentially large coefficient. Therefore, Leibniz’ formula and the above
equality yield

$\displaystyle\operatorname{maxc}(\det(\bm{D}_{R}(x)))\leavevmode\nobreak\ $
$\displaystyle\leq
m!\cdot\big{(}(\deg(\bm{D}_{R}(x))+1)\cdot\operatorname{maxc}(\bm{D}_{R}(x))\big{)}^{|P|}$
$\displaystyle\leq
m!\cdot\big{(}(\deg(\bm{D}_{R}(x))+1)\cdot\operatorname{maxc}(\bm{D}_{R}(x))\big{)}^{m}$
$\displaystyle\leq
2^{m\log_{2}m}\cdot(\deg(\mathcal{S}^{\prime})+1)^{m}\cdot(\operatorname{maxc}(\mathcal{S}^{\prime}))^{m}$
$\displaystyle\leq(\deg(\mathcal{S}^{\prime})\cdot\operatorname{maxc}(\mathcal{S}^{\prime}))^{\mathcal{O}(m^{2})}.$

Recall that each entry of the adjugate $\operatorname{adj}(\bm{D}_{R}(x))$ can
be computed by deleting one row and one column from $\bm{D}_{R}(x)$ and
computing the determinant of the resulting matrix. This implies
$\deg(\operatorname{adj}(\bm{D}_{R}(x)))\leq\deg(\det(\bm{D}_{R}(x)))$. We
cannot conclude
$\operatorname{maxc}(\operatorname{adj}(\bm{D}_{R}(x)))\leq\operatorname{maxc}(\det(\bm{D}_{R}(x)))$,
because terms with conflicting signs in the Leibniz formula might negate each
other in $\det(\bm{D}_{R}(x))$, while not doing so in
$\operatorname{adj}(\bm{D}_{R}(x))$. However, the approximation we do above
for $\operatorname{maxc}(\det(\bm{D}_{R}(x)))$ assumes that all summands have
the same sign, and therefore is also an upperbound for
$\operatorname{maxc}(\operatorname{adj}(\bm{D}_{R}(x)))$. We have

$\displaystyle\deg(\bm{D}(x)\cdot\operatorname{adj}(\bm{D}_{R}(x))\cdot\bm{c}_{R}(x))\leavevmode\nobreak\
$ $\displaystyle\leq
2\cdot\deg(\mathcal{S}^{\prime})+m\cdot\deg(\mathcal{S}^{\prime})$
$\displaystyle=(m+2)\cdot\deg(\mathcal{S}^{\prime})$
$\displaystyle=\mathcal{O}(m\cdot\deg(\mathcal{S}^{\prime}))\ .$

For the maximal coefficient, we again remark that each polynomial consists of
at most $\deg+1$ monomials, and further that computing each entry per matrix
multiplication here involves adding up $n$ terms.

Thus, we get

$\displaystyle\operatorname{maxc}(\bm{D}(x)\cdot\operatorname{adj}(\bm{D}_{R}(x))\cdot\bm{c}_{R}(x))$
$\displaystyle\leavevmode\nobreak\ \begin{aligned} \leq\leavevmode\nobreak\
&(\deg(\bm{D}(x))\cdot\operatorname{maxc}(\bm{D}(x)))\cdot
n\cdot(\deg(\operatorname{adj}(\bm{D}_{R}(x)))\cdot\operatorname{maxc}(\operatorname{adj}(\bm{D}_{R}(x))))\\\
&\cdot n\cdot(\deg(\bm{c}_{R}(x))\cdot\operatorname{maxc}(\bm{c}_{R}(x)))\\\
\leq\leavevmode\nobreak\
&(\deg(\mathcal{S}^{\prime})\cdot\operatorname{maxc}(\mathcal{S}^{\prime}))^{2}\cdot
n^{2}\cdot(m\cdot\deg(\mathcal{S}^{\prime}))\cdot(\deg(\mathcal{S}^{\prime})\cdot\operatorname{maxc}(\mathcal{S}^{\prime}))^{\mathcal{O}(m^{2})}\\\
=\leavevmode\nobreak\
&(n\cdot\deg(\mathcal{S}^{\prime})\cdot\operatorname{maxc}(\mathcal{S}^{\prime}))^{\mathcal{O}(m^{2})}\
.\end{aligned}$

$\deg(\det(\bm{D}_{R}(x))\cdot\bm{c}(x))\leq
m\cdot\deg(\mathcal{S}^{\prime})+\deg(\mathcal{S}^{\prime})=\mathcal{O}(m\cdot\deg(\mathcal{S}^{\prime}))$,

$\displaystyle\operatorname{maxc}(\det(\bm{D}_{R}(x))\cdot\bm{c}(x))$
$\displaystyle\leavevmode\nobreak\
\leq(\operatorname{maxc}(\det(\bm{D}_{R}(x)))\cdot\deg(\det(\bm{D}_{R}(x))))\cdot
m\cdot(\operatorname{maxc}(\bm{c}(x))\cdot\deg(\bm{c}(x)))$
$\displaystyle\leavevmode\nobreak\
\leq(\deg(\mathcal{S}^{\prime})\cdot\operatorname{maxc}(\mathcal{S}^{\prime}))^{\mathcal{O}(m^{2})}\cdot\deg(\mathcal{S}^{\prime})^{2}\cdot\operatorname{maxc}(\mathcal{S}^{\prime})$
$\displaystyle\leavevmode\nobreak\
=(\deg(\mathcal{S}^{\prime})\cdot\operatorname{maxc}(\mathcal{S}^{\prime}))^{\mathcal{O}(m^{2})}\
.$

Since $\deg(\mathcal{S}^{\prime})=\deg(\mathcal{S})$ and
$\operatorname{maxc}(\mathcal{S}^{\prime})=\operatorname{maxc}(\mathcal{S})$
by construction, we obtain the required values for polynomials appearing in
$\Phi(x)$.

###  A.2 Precise bounds for Lemma 4.1

In this subsection, we provide a proof of Lemma 4.1 that yields the precise
bounds promised in the statement.

With a DNFLB $\Phi(x)$ in hand, we now establish a bound on the size of a
smallest solution. To this end we apply a root separation theorem that gives a
lower bound on the distance of distinct real roots of a polynomial. We define
the _real roots_ of a polynomial $p(x)\in\mathbb{Z}[x]$ as
$\mathsf{Roots}_{\mathbb{R}}(p(x))=\\{-\infty,\infty\\}\cup\\{r\in\mathbb{R}\;|\;p(r)=0\\}$.
The advantage of including $-\infty$ and $\infty$ is that the entire set
$\mathbb{R}$ decomposes into intervals between adjacent roots of $p(x)$, which
will save us case distinctions. Thus, recall that the number of (even complex)
roots of a polynomial of degree $d$ is at most $d+2$. For a DNFLB $\Phi(x)$,
we define $\mathsf{Roots}_{\mathbb{R}}(\Phi(x))$ as the set of all real roots
among its polynomials. Finally, we define
$\mathsf{Separation}(p(x))=\min_{r\neq
r^{\prime}\in\mathsf{Roots}_{\mathbb{R}}(p(x))}|r-r^{\prime}|$ as the minimal
distance between two distinct real roots. We restate Rump’s bound from the
main paper. See 4.6

We now formulate the feasibility of $\Phi(x)$ in terms of constraints on real
roots. Consider one of its lower bound constraints $p(x)>0$. Let
$-\infty=r_{1}<r_{2}<\ldots<r_{k}=\infty$ be the real roots of $p(x)$. The key
observation is that, on the entire interval $(r_{i},r_{i+1})$, the polynomial
$p(x)$ is either positive or negative. We evaluate up-front which is the case,
and collect in the set $P\subseteq\mathsf{Roots}_{\mathbb{R}}(p(x))$ the roots
$r_{i}$ where a positive interval starts. Then the lower bound constraint
$p(x)>0$ is equivalent to $\bigvee_{r_{i}\in P}r_{i}<x<r_{i+1}$. We refer to a
formula of the form $\ell<x<u$ as an _interval constraint_ , and call $\ell$ a
lower and $u$ an upper bound.

Consider a conjunction of interval constraints $\bigwedge_{i\in
I}\ell_{i}<x<u_{i}$ with $I$ a finite index set. A rational number
$\mathit{t}\in\mathbb{Q}$ will only satisfy this conjunction if it is larger
than the largest lower bound $\ell=\max_{i\in I}\ell_{i}$, and smaller than
the least upper bound $u=\min_{i\in I}u_{i}$. This means the conjunction is
equivalent to the single interval constraint $\ell<x<u$.

To deal with lower bound constraints $p(x)\geq 0$ that are not strict, we
generalize interval constraints to admit both relations, $<$ and $\leq$. To
generalize the elimination of conjunctions, these relations can also be mixed,
so we also consider $\ell\leq x<u$ an interval constraint. We refer to a
disjunction of interval constraints as a DINC $\Theta(x)$. We use
$\mathsf{Bounds}(\Theta(x))$ for the set of bounds that appear in $\Theta(x)$.
The discussion yields the following.

######  Lemma A.1.

For every DNFLB $\Phi(x)$, there is a DINC $\Theta(x)$ that satisfies
$\Phi(x)\mathop{\models\rotatebox[origin={c}]{180.0}{$\models$}_{\mathbb{Q}}}\Theta(x)$
and $\mathsf{Bounds}(\Theta(x))\subseteq\mathsf{Roots}_{\mathbb{R}}(\Phi(x))$.

With this, we are finally ready to prove Lemma 4.1.

######  Proof A.2 (Proof of Lemma 4.1).

Consider an SNLS
$\mathcal{S}(x,\bm{y})=\bm{A}(x)\cdot\bm{y}\geq\bm{b}(x)\wedge\bm{y}\geq 0$
that is feasible (over the rationals). Let $\bm{A}(x)$ be an $m\times n$
matrix. We first apply Theorem 4.2 to obtain the DNFLB $\Phi(x)$ whose
polynomials have a degree bounded by $\mathcal{O}(m\cdot\deg(\mathcal{S}))$
and a maximal coefficient bounded by
$n^{2}\cdot(\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(m^{2})}$.
We then apply Lemma A.1 to turn this DNFLB into a DINC $\Theta(x)$.

Since the SNLS is feasible and the two transformations yield formulae that are
equivalent over the rationals, there is an interval constraint $\ell<x<u$ in
$\Theta(x)$ that has a rational solution. We show that there is even a
rational $\mathit{t}=\frac{a}{b}$ with $\ell<\mathit{t}<u$ that satisfies the
bound promised by Lemma 4.1. We proceed by a case distinction along $\ell$ and
$u$.

Case $\bm{\ell<u}$:

In the special case $\ell=-\infty$ and $u=\infty$, we pick $a=0$ and $b=1$ as
a solution. Assume $u\neq\infty$, the case $\ell\neq-\infty$ is similar. Then
$\ell\in\mathsf{Roots}_{\mathbb{R}}(p_{1})$ and
$u\in\mathsf{Roots}_{\mathbb{R}}(p_{2})$ for two polynomials in $\Phi(x)$.
Note that $p_{1}$ and $p_{2}$ may be different. However, $\ell$ and $u$ are
both roots of the product polynomial $p_{\times}=p_{1}\cdot p_{2}$, meaning
$\ell,u\in\mathsf{Roots}_{\mathbb{R}}(p_{\times})$. Note that
$\deg(p_{\times})=\deg(p_{1})+\deg(p_{2})\in\mathcal{O}(m\cdot\deg(\mathcal{S}))$
and $|\\!|p_{\times}|\\!|_{1}\leq|\\!|p_{1}|\\!|_{1}\cdot|\\!|p_{2}|\\!|_{1}$.
Therefore using Rump’s Bound we get

$\displaystyle|u-\ell|$ $\displaystyle\leavevmode\nobreak\
>\leavevmode\nobreak\ $
$\displaystyle\big{(}\deg(p_{\times})^{\deg(p_{\times})+1}\cdot(1+|p_{\times}|_{1})^{2\deg(p_{\times})}\big{)}^{-1}$
$\displaystyle\leavevmode\nobreak\ \geq\leavevmode\nobreak\ $
$\displaystyle\left(\begin{aligned}
&\mathcal{O}(m\cdot\deg(\mathcal{S}))^{\mathcal{O}(m\cdot\deg(\mathcal{S}))}\\\
&\cdot\Big{(}\mathcal{O}(m\cdot\deg(\mathcal{S}))\cdot(n\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(m^{2})}\Big{)}^{\mathcal{O}(m\cdot\deg(\mathcal{S}))}\end{aligned}\right)^{-1}$
$\displaystyle\leavevmode\nobreak\ \geq\leavevmode\nobreak\ $
$\displaystyle(n\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{-\mathcal{O}(m^{3}\cdot\deg(\mathcal{S}))}.$

In the following, we use $B$ as a shorthand for
$(n\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(m^{3}\cdot\deg(\mathcal{S}))}$.
Immediately, we get $B(u-\ell)>1$. Thus, there is an integer $a\in\mathbb{Z}$
such that $B\ell<Bu-1\leq a<Bu$. Dividing by $B$ yields $\ell<\frac{a}{B}<u$,
meaning we can choose a denominator $b\in\mathbb{N}\setminus\\{0\\}$ for a
suitable solution with $b\leq B$. Let $u$ be a root of $p_{1}$. We apply
Cauchy’s bound Lemma 4.8 on root sizes, and get

$|u|\leq
1+|p_{1}|_{1}\leq\mathcal{O}(m\cdot\deg(\mathcal{S}))\cdot(n\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(m^{2})}\leq(n\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(m^{2})},$

and therefore $|a|\leq B|u|+1\leq
B\cdot(n\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(m^{2})}$.
Due to the $\mathcal{O}$-notation, the second factor is subsumed by $B$ here.

Case $\bm{\ell=u}$:

Then $\frac{a}{b}=\ell=u$, and this is a root of a polynomial $p(x)$ in
$\Phi(x)$. Thus, there is a polynomial $p$ in $\Phi(x)$ such that
$\frac{a}{b}\in\mathsf{Roots}(p)$. Since also $\frac{a}{b}\in\mathbb{Q}$ we
get that $a,b\leq\operatorname{maxc}(p)$ using the Rational Root Theorem
(Theorem 4.7). This implies
$a,b\leq(n\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(m^{2})}$.

In all cases
$B=(n\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(m^{3}\cdot\deg(\mathcal{S}))}$
is a bound on the complexity of $x$, as required.

###  A.3 Proof of Theorem 3.2

We can now put the ingredients together and show Theorem 3.2. We write
$n=\mathit{col}(\mathcal{S})=\mathit{col}(\mathcal{S}^{\prime})$ and
$m=\mathit{row}(\mathcal{S})$, as in the previous subsections. According to
Lemma 4.1, we know that if our system

$\mathcal{S}:=\bm{A}(x)\cdot\bm{y}\geq\bm{b}(x)\wedge\bm{y}\geq 0$

is feasible with some $(t,\bm{s})\in\mathbb{Q}\times\mathbb{Q}^{n}$, then for
some $t\in\mathbb{Q}$ with

$|\\!|t|\\!|_{1}\leq(n\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(m^{3}\cdot\deg(\mathcal{S}))}.$

We can now apply the argument from Theorem 4.2 again: We have shown there that
if there exists a solution $\bm{s}$ for a particular $t$ with
$\bm{A}(t)\cdot\bm{s}\geq\bm{b}(t)$ and $\bm{s}\geq\bm{0}$, then for some
$R\subseteq[1,m+n]$, for which $\bm{D}_{R}(t)$ is invertible, the following
$\bm{s}^{*}$ is a solution to $\mathcal{S}$:

$\bm{s}^{*}=\bm{D}_{R}^{-1}(t)\cdot
c_{R}(t)=\frac{\operatorname{adj}(\bm{D}_{R}(t))}{\det(\bm{D}_{R}(t))}\cdot
c_{R}(t).$

Moreover, in the proof of Theorem 4.2, we have seen that

$\displaystyle\deg(\det(\bm{D}_{R}(x)))$ $\displaystyle\leq
m\cdot\deg(\mathcal{S}^{\prime})$
$\displaystyle\deg(\operatorname{adj}(\bm{D}_{R}(x)))$ $\displaystyle\leq
m\cdot\deg(\mathcal{S}^{\prime})$
$\displaystyle\operatorname{maxc}(\det(\bm{D}_{R}(x)))$
$\displaystyle\leq(n\cdot\deg(\mathcal{S}^{\prime})\cdot\operatorname{maxc}(\mathcal{S}^{\prime}))^{\mathcal{O}(m^{2})}$
$\displaystyle\operatorname{maxc}(\operatorname{adj}(\bm{D}_{R}(x)))$
$\displaystyle\leq(n\cdot\deg(\mathcal{S}^{\prime})\cdot\operatorname{maxc}(\mathcal{S}^{\prime}))^{\mathcal{O}(m^{2})}$
$\displaystyle|\\!|\operatorname{adj}(D_{R}(t))|\\!|_{1}$
$\displaystyle\leq\deg(\operatorname{adj}(\bm{D}_{R}(x)))\cdot\operatorname{maxc}(\operatorname{adj}(\bm{D}_{R}(x)))\cdot|\\!|t|\\!|_{1}^{\deg(\operatorname{adj}(\bm{D}_{R}(x)))}$
$\displaystyle\leq
m\cdot\deg(\mathcal{S}^{\prime})\cdot(n\cdot\deg(\mathcal{S}^{\prime})\cdot\operatorname{maxc}(\mathcal{S}^{\prime}))^{\mathcal{O}(m^{2})}\cdot|\\!|t|\\!|_{1}^{m\cdot\deg(\mathcal{S}^{\prime})}$
$\displaystyle\leq(n\cdot\deg(\mathcal{S}^{\prime})\cdot\operatorname{maxc}(\mathcal{S}^{\prime}))^{\mathcal{O}(m^{2})}\cdot|\\!|t|\\!|_{1}^{m\cdot\deg(\mathcal{S}^{\prime})}$
$\displaystyle\leq(n\cdot\deg(\mathcal{S}^{\prime})\cdot\operatorname{maxc}(\mathcal{S}^{\prime}))^{\mathcal{O}(m^{2})}\cdot\left((n\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}\mathcal{S})^{\mathcal{O}(m^{3}\cdot\deg(\mathcal{S}))}\right)^{m\cdot\deg(\mathcal{S}^{\prime})}$
$\displaystyle\leq(n\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(m^{4}\cdot\deg(\mathcal{S})^{2})}$

Since for $\det(D_{R}(x))$, we have the same bounds on maximal coefficients
and degree as for $\operatorname{adj}(D_{R}(x))$, we can show similarly:

$\displaystyle|\\!|\det(\bm{D}_{R}(t))|\\!|_{1}\leq(n\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(m^{4}\cdot\deg(\mathcal{S})^{2})}$

Moreover, clearly:

$|\\!|c_{R}(t)|\\!|_{1}\leq\operatorname{maxc}(\mathcal{S})\cdot|\\!|t|\\!|_{1}\leq(n\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}\mathcal{S})^{\mathcal{O}(m^{3}\cdot\deg(\mathcal{S}))}.$

Furthermore, we have

$|\\!|\operatorname{adj}(\bm{D}_{R}(t))\cdot c_{R}(t)|\\!|_{1}\leq
n\cdot(|\\!|\operatorname{adj}(\bm{D}_{R}(t))|\\!|_{1}+|\\!|c_{R}(t)|\\!|_{1})\leq(n\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(m^{4}\cdot\deg(\mathcal{S})^{2})}.$

Therefore, we can upper bound $\bm{s}^{*}$ as follows:

$\displaystyle|\\!|\bm{s}^{*}|\\!|_{1}$
$\displaystyle=\left\|\frac{\operatorname{adj}(\bm{D}_{R}(t))}{\det(\bm{D}_{R}(t))}\cdot
c_{R}(t)\right\|_{1}\leq|\\!|\operatorname{adj}(\bm{D}_{R}(t))\cdot
c_{R}(t)|\\!|_{1}+|\\!|\det(\bm{D}_{R}(t))|\\!|_{1}$
$\displaystyle\leq(n\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(m^{4}\cdot\deg(\mathcal{S})^{2})}+(n\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(m^{4}\cdot\deg(\mathcal{S})^{2})}$
$\displaystyle\leq(n\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(m^{4}\cdot\deg(\mathcal{S})^{2})}$
$\displaystyle\leq(\mathit{col}(\mathcal{S})\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(\mathit{row}(\mathcal{S})^{4}\cdot\deg(\mathcal{S})^{2})}$

As we mentioned in the main paper, if we can ensure that all components of
$c_{R}(t)$ have the same denominator, we also ensure this for $\bm{s}^{*}$. To
avoid clutter, we did not argue this property in the bound above. However,
this does not change the bound. In order to ensure that the components of
$c_{R}(t)$ all have the same denominator, we only need to multiply the
denominator and nominator of each component by a factor of at most
$q^{\deg(\mathcal{S})}$ where $q$ is the denominator of $t$. This is because
the components of $c_{R}(t)$ are obtained by summing integer multiples of
$1,t^{1},\ldots,t^{\deg(\mathcal{S})}$. The bit size of $c_{R}(t)$, and thus
the resulting $\bm{s}^{*}$, blows up by a factor of at most
$\deg(\mathcal{S})$, which is absorbed by the term
$(\mathit{col}(\mathcal{S})\cdot\deg(\mathcal{S})\cdot\operatorname{maxc}(\mathcal{S}))^{\mathcal{O}(\mathit{row}(\mathcal{S})^{4}\cdot\deg(\mathcal{S})^{2})}$.
This completes the proof of Theorem 3.2.

##  Appendix B Additional material on Section 5

In this section we show Lemma 5.3. To do this, we use the inseparability
characterization given in [2]. We break Lemma 5.3 down into its two
directions.

######  Lemma B.1.

Let $\mathcal{V}$ be an $n$-visible VASS. If there is a coverable
inseparability flower $(\mathit{cf}.\sigma,\usym{2740})$, then
$\mathit{L}(\mathcal{V})\mathrel{\not|}D_{n}$.

######  Lemma B.2.

Let $\mathcal{V}$ be an $n$-visible VASS. If
$\mathit{L}(\mathcal{V})\mathrel{\not|}D_{n}$, then there is a coverable
inseparability flower $(\mathit{cf}.\sigma,\usym{2740})$.

For Lemma B.1, we use the basic separator characterization of regular
separability in [2]. Given a Büchi VASS $\mathcal{V}$, regular separability of
its language $\mathit{L}(\mathcal{V})$ from $D_{n}$ is characterized in terms
of inclusion in a finite union of so-called basic separators. The authors
identify two families of languages that together make up the set of basic
separators, $\\{P_{i,k}\;|\;i\in[1,n],k\in{\rm Nature}\\}$ and
$\\{S_{\bm{x},k}\;|\;\bm{x}\in\mathbb{N}^{n},k\in{\rm Nature}\\}$. We will
define these families below. Let us first formally state the characterization.

######  Lemma B.3 ([2]).

Let $\mathcal{V}$ be an $n$-visible VASS. Then,
$\mathit{L}(\mathcal{V})\mathrel{|}D_{n}$ if and only if there is a number
$k\in{\rm Nature}$ and a finite set of vectors $X\subseteq{\rm Nature}^{n}$
such that

$\mathit{L}(\mathcal{V})\subseteq\bigcup_{i\in[1,n]}P_{i,k}\cup\bigcup_{\bm{x}\in
X}S_{\bm{x},k}\ .$

Both language families impose conditions on the letter balance along a word.
Given a word $w\in\Sigma_{n}^{*}$ its _letter balance_ $\varphi(w)$ is a
vector in $\mathbb{Z}^{n}$, whose $i$-th component $\varphi_{i}(w)$ counts how
many more letters $a_{i}$ than $\bar{a}_{i}$ appear in $w$. In other words
this balance is equal to the effect on the external counters of a finite run
$\mathit{cf}.\rho$ that is labeled by the word $w$, i.e.
$\varphi(w)=\exteff(\rho)$.

The language $P_{i,k}\subseteq\Sigma_{n}^{\omega}$ contains words whose
balance is bounded by $k$ in the $i$-th component before becoming negative for
some prefix. In contrast, the language
$S_{\bm{x},k}\subseteq\Sigma_{n}^{\omega}$ is prefix independent. It contains
words whose $\bm{x}$-weighted balance gradually decreases beyond some point,
while all suffixes beyond the same point have an $\bm{x}$-weighted balance
bounded by $k$. Here the _$\bm{x}$ -weighted balance_ of a word
$v\in\Sigma_{n}^{*}$ for some vector $\bm{x}\in{\rm Nature}^{n}$ is the dot
product $\langle\bm{x},\varphi(v)\rangle\in\mathbb{Z}$.

These language families are defined formally below, for all $i\in[1,n]$,
$\bm{x}\in{\rm Nature}^{n}$, and $k\in{\rm Nature}$. For a word
$w\in\Sigma_{n}^{*}$ or $w\in\Sigma_{n}^{\omega}$, we use $\mathsf{prefix}(w)$
to denote the set of finite prefixes of $w$, and $\mathsf{infix}(w)$ to denote
the set of finite infixes of $w$.

$\displaystyle P_{i,k}$ $\displaystyle=\\{w\in\Sigma_{n}^{\omega}\;|\;\exists
v\in\mathsf{prefix}(w).\varphi_{i}(v)<0\wedge\forall
u\in\mathsf{prefix}(v).\varphi_{i}(u)\leq k\\}$ $\displaystyle S_{\bm{x},k}$
$\displaystyle=\\{w.v\in\Sigma_{n}^{\omega}\;|\;\forall
u\in\mathsf{infix}(v).\langle\bm{x},\varphi(u)\rangle\leq
k\;\;\wedge\;\;v=v_{0}.v_{1}\ldots,\forall j\in{\rm
Nature}.\;\langle\bm{x},\varphi(v_{j})\rangle<0\\}$

With this at hand, we show Lemma B.1. We recall the argument in [2,
Proposition 5.5] and extend it to include the basic separators of the form
$P_{i,k}$ for all $i\in[1,n]$, $k\in{\rm Nature}$.

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

Let $\mathcal{V}$ be an $n$-visible VASS, and let
$(\mathit{cf}.\sigma,\usym{2740})$ be a coverable inseparability flower where
$\usym{2740}=(q_{f},I,\alpha,\beta,\gamma)$ and $[1,d+n]=\Omega\uplus I$.
Towards a contradiction, suppose $\mathit{L}(\mathcal{V})\mathrel{|}D_{n}$.
Then, by Lemma B.3, we know that there is a number $k\in{\rm Nature}$ and a
finite set $X\subseteq{\rm Nature}^{n}$ such that

$\mathit{L}(\mathcal{V})\subseteq\bigcup_{i\in[1,n]}P_{i,k}\cup\bigcup_{\bm{x}\in
X}S_{\bm{x},k}\ .$

Let the effect $\delta\varphi(-)$ of the prefixes of $\alpha$, $\beta$, and
$\gamma$ be bounded from below by $-y\leq-1$ for every counter, and let the
run $\mathit{cf}.\sigma$ end in the extended configuration $(q_{f},\bm{m})$.
Let $\bm{m}^{\prime}\in{\rm Nature}^{d+n}$ be obtained from $\bm{m}$ by
replacing all instances of $\omega$ with $3\cdot(k+1)\cdot y$. Since
$(\mathit{cf}.\sigma,\usym{2740})$ is coverable, $(q_{f},\bm{m})$ is coverable
as well, hence there must be witnessing runs covering the non-$\omega$
counters of $(q_{f},\bm{m})$ and reaching arbitrarily high values for the
counters in $\omega(q_{f},\bm{m})\supseteq\Omega$. In particular, there must
be some run $(q_{0},\bm{0}).\rho$ that covers the configuration
$(q_{f},\bm{m}^{\prime})$.

We know that upon taking $\alpha$, $\beta$, and $\gamma$ from
$(q_{f},\bm{m})$, the counter $i$ remains positive and the counter valuation
does not decrease, for all $i\in I$. Clearly this remains true if we repeat
these loops $(k+1)$-times, i.e. taking $\alpha^{k+1}$, $\beta^{k+1}$, and
$\gamma^{k+1}$. By our choice of $y$, we also know that starting from some
counter valuation $u\in{\rm Nature}$ for counter $i\in[1,d+n]$, during
execution of $\alpha$, $\beta$, and $\gamma$ we always remain above the
valuation $u-y$ for this counter. Therefore, since $\bm{m}^{\prime}$ has a
counter valuation of $3\cdot(k+1)\cdot y$ for all counters in
$\Omega\subseteq\omega(q_{f},\bm{m})$, taking
$\alpha^{k+1}.\beta^{k+1}.\gamma^{k+1}$ from $(q_{f},\bm{m}^{\prime})$ keeps
the counters in $\Omega$ positive as well. So, we deduce that the run
$(q_{0},\bm{0}).\rho.\alpha^{k+1}.\beta^{k+1}.\gamma^{k+1}$ remains positive
in all counters $[1,d+n]$. Furthermore condition (ii) for an inseparability
bloom, $\delta(\alpha)+\delta(\beta)+\delta(\gamma)\geq 0$, implies that
$\alpha^{k+1}.\beta^{k+1}.\gamma^{k+1}$ can be infinitely repeated to produce
a run that remains positive in the counters $\\{1,\ldots d\\}$. Because
$\alpha$, $\beta$, and $\gamma$ are loops on the final state $q_{f}$, the run
$(q_{0},\bm{0}).\rho.(\alpha^{k+1}.\beta^{k+1}.\gamma^{k+1})^{\omega}$ is an
accepting run in $\mathcal{V}$. Let $w\in\Sigma_{n}^{\omega}$ be the word
labeling this run. The argument in the proof of [2, Proposition 5.5] applies
to show $w\not\in S_{\bm{x},k}$ for all $\bm{x}\in X$.

It remains to argue that $w\not\in P_{i,k}$ for all $i<n$. If $d+i\in I$, then
we know that the counter $d+i$ never becomes negative along the run, and thus
the same holds for the $i$th component of the letter balance. Then $w\not\in
P_{i,k}$. If $d+i\in\Omega$, then taking $\rho$ from $(q_{0},\bm{0})$ covers
$(q_{f},\bm{m}^{\prime})$, where $\bm{m}^{\prime}[d+i]\geq k+1$ by definition.
Therefore the $i$th letter balance exceeds bound $k+1$ before it can drop
below $0$, so $w\not\in P_{i,k}$.

For the direction of Lemma B.2, we do not directly argue from an assumption of
inseparability. Instead, we use another characterization provided in [2,
Theorem 5.3]. This characterization follows in two steps. First, it is shown
that a Büchi VASS $\mathcal{V}_{\mathsf{pump}}$ can be constructed from
$\mathcal{V}$ such that the language $\mathit{L}(\mathcal{V}_{\mathsf{pump}})$
is (so-called) _pumpable_ , and $\mathit{L}(\mathcal{V})\mathrel{|}D_{n}$ if
and only if $\mathit{L}(\mathcal{V}_{\mathsf{pump}})\mathrel{|}D_{n}$. The
definition of pumpability is not needed for the purposes of this paper.

For our proof, we only need the second step of the characterization: If
$\mathit{L}(\mathcal{V})$ is pumpable, then
$\mathit{L}(\mathcal{V})\mathrel{\not|}D_{n}$ if and only if the Büchi
Automaton $\mathsf{KM}(\mathcal{V})$ contains a structure called a _KM-
inseparability flower_ 111In [2] this structure is simply called
_inseparability flower_. Since we already use this term for a different
structure, which does not involve the KM-graph, we felt it appropriate to add
the prefix “KM-” for the version from [2], to differentiate the two.. We
define these kinds of flowers and the notation $\mathsf{KM}(\mathcal{V})$
below. Putting the two steps together, we get the following characterization.

######  Lemma B.5 ([2]).

Let $\mathcal{V}$ be an $n$-visible VASS. Then,
$\mathit{L}(\mathcal{V})\mathrel{\not|}D_{n}$ if and only if
$\mathsf{KM}(\mathcal{V}_{\mathsf{pump}})$ contains a KM-inseparability
flower.

We recall the definitions we need. For the rest of this section, fix a Büchi
VASS $\mathcal{V}=(Q,q_{0},\Sigma_{n},T,F)$. We start with the definition of
the Karp-Miller graph [15] of a VASS, as formulated in [2]. The _Karp-Miller
graph_
$\mathsf{KM}(\mathcal{V})=(Q_{\mathsf{KM}},(q_{0},\bm{0}),T,T_{\mathsf{KM}},F\times{\rm
Nature}_{\omega}^{d})$ is a Büchi Automaton with states
$Q_{\mathsf{KM}}\subseteq Q\times{\rm Nature}_{\omega}^{d}$, whose transitions
are labeled with the transitions of $\mathcal{V}$. Its states and transitions
are constructed by starting with $Q_{\mathsf{KM}}=\emptyset$ and
$T_{\mathsf{KM}}=\\{(q_{0},\bm{0})\\}$, and repeating the following steps
towards a fixed point. Pick a transition $t=(q,a,\bm{x},q^{\prime})\in T$ and
a state $(q,\bm{m})\in T_{\mathsf{KM}}$. First simulate
$(q,a,\bm{x},q^{\prime})$ from $(q,\bm{m})$, to get
$(q^{\prime},\bm{m}+\bm{x})$. If $(q^{\prime},\bm{m}+\bm{x})\notin Q\times{\rm
Nature}^{d+n}_{\omega}$, continue. In the other case construct
$\bm{m}_{\omega}$ from $\bm{m}+\bm{x}$ as follows: (1) for $i\in[1,d]$, if
there is a state $(q^{\prime},\bm{m}^{\prime}),\in Q_{\mathsf{KM}}$ with
$\bm{m}^{\prime}\leq\bm{m}+\bm{x}$ and $\bm{m}^{\prime}[i]<(\bm{m}+\bm{x})[i]$
such that $(q,\bm{m})$ is reachable from $(q^{\prime},\bm{m}^{\prime})$ using
the transitions generated so far, then set $\bm{m}_{\omega}[i]=\omega$; (2)
otherwise, set $\bm{m}_{\omega}[i]=(\bm{m}+\bm{x})[i]$. Finally set
$Q_{\mathsf{KM}}:=Q_{\mathsf{KM}}\cup\\{(q^{\prime},\bm{m}_{\omega})\\}$ and
$T_{\mathsf{KM}}:=T_{\mathsf{KM}}\cup\\{(q,\bm{m})\xrightarrow{t}(q^{\prime},\bm{m}_{\omega})\\}$.
This process reaches a fixed point after finitely many states, since $({\rm
Nature}_{\omega}^{d},\leq)$ is a well quasi order. In particular, this means
that the state space of the Karp Miller graph is finite. It is immediate from
the definition that if $(q,\bm{m})\in Q\times{\rm Nature}^{d}_{\omega}$ can be
reached in $\mathsf{KM}(\mathcal{V})$, then $(q,\bm{m})$ is coverable in
$\mathcal{V}$.

Now we define $\mathcal{V}_{\mathsf{pump}}$. The VASS
$\mathcal{V}_{\mathsf{pump}}=(Q_{\mathsf{pump}},q_{0},\Sigma_{n},T_{\mathsf{pump}},F\times{\rm
Nature}^{d+n}_{\omega})$ has the states $Q_{\mathsf{KM}}$ of the Karp-Miller
graph $\mathsf{KM}(\mathcal{V}\times\mathcal{D}_{n})$ as its state space, and
$((q,\bm{m}),a,\bm{x},(q^{\prime},\bm{m}^{\prime}))\in T_{\mathsf{pump}}$ if
and only if $(q,\bm{m})\xrightarrow{t}(q^{\prime},\bm{m}^{\prime})$ is a
transition in $\mathsf{KM}(\mathcal{V}\times\mathcal{D}_{n})$ for some
$t=(q,a,\bm{x},q^{\prime})$.

A KM-inseparability flower in $\mathsf{KM}(\mathcal{V}_{\mathsf{pump}})$
consists of a reachable final state $(q_{f},\bm{m})$ in
$\mathsf{KM}(\mathcal{V}_{\mathsf{pump}})$ with three loops $\alpha$, $\beta$,
$\gamma$ on that state that fulfill the following three conditions.

  1. (a)

$\delta(\alpha)+\delta(\beta)+\delta(\gamma)\geq\bm{0}$,

  2. (b)

$\varphi(\alpha)+\varphi(\beta)\geq\bm{0}$,

  3. (c)

there is $t\in\mathbb{Q}$ with
$\varphi(\alpha)+\varphi(\beta)+\varphi(\gamma)-t\cdot\varphi(\alpha)=\bm{0}$.

Here, for a path (or cycle) $\rho$ in the Karp-Miller graph, we write
$\delta(\rho)$ to refer to the effect of the transition sequence it was
labelled by. In other words for all $\chi\in\\{\alpha,\beta,\gamma\\}$ in
$\mathsf{KM}(\mathcal{V}_{\mathsf{pump}})$ labelled by a sequence of
transitions $\rho_{\chi}$ of $\mathcal{V}_{\mathsf{pump}}$, we define
$\delta(\chi):=\delta(\rho_{\chi})$.

We are now ready to prove Lemma B.2.

######  Proof B.6 (Proof of Lemma B.2).

Let $\mathcal{V}$ be an $n$-visible VASS with
$\mathit{L}(\mathcal{V})\mathrel{\not|}D_{n}$. Then by Lemma B.5
$\mathsf{KM}(\mathcal{V}_{\mathsf{pump}})$ contains a KM-inseparability
flower. This means that there is a state $(q_{f},\bm{m})$ of
$\mathsf{KM}(\mathcal{V}_{\mathsf{pump}})$ and there are three loops $\alpha$,
$\beta$, $\gamma$ on this state with the properties (a), (b), (c). Recall that
the state space of $\mathcal{V}_{\mathsf{pump}}$ is that of
$\mathsf{KM}(\mathcal{V}\times\mathcal{D}_{n})$. Also recall that
$((q,\bm{n}),a,\bm{x},(q^{\prime},\bm{n}^{\prime}))\in T_{\mathsf{pump}}$ if
and only if there is a transition
$(q,\bm{n})\xrightarrow{t}(q^{\prime},\bm{n}^{\prime})$ in
$\mathsf{KM}(\mathcal{V}\times\mathcal{D}_{n})$ for some
$t=(q,a,\bm{x},q^{\prime})\in T$. Therefore
$q_{f}=(q_{f}^{\prime},\bm{m}^{\prime})$ is a state in
$\mathsf{KM}(\mathcal{V}\times\mathcal{D}_{n})$, for some
$\bm{m}^{\prime}\in{\rm Nature}^{d+n}_{\omega}$ and final $q_{f}^{\prime}$ in
$\mathcal{V}$ with three loops $\alpha^{\prime}$, $\beta^{\prime}$,
$\gamma^{\prime}$ on it in $\mathsf{KM}(\mathcal{V}\times\mathcal{D}_{n})$
that fulfill (a), (b), and (c). Here $\alpha^{\prime}$, $\beta^{\prime}$,
$\gamma^{\prime}$ are obtained by extracting the
$\mathcal{V}_{\mathsf{pump}}$-transitions from the labels of $\alpha$,
$\beta$, $\gamma$ and then matching them to the corresponding transitions in
$\mathsf{KM}(\mathcal{V}\times\mathcal{D}_{n})$. Since $\alpha^{\prime}$,
$\beta^{\prime}$, $\gamma^{\prime}$ are themselves labelled by transition
sequences (of $\mathcal{V}\times\mathcal{D}_{n}$), we can extract again to
obtain the loops $\alpha_{\mathcal{V}}$, $\beta_{\mathcal{V}}$,
$\gamma_{\mathcal{V}}$ in $\mathcal{V}$ (ignoring the
$\mathcal{D}_{n}$-components of the transitions). We claim that
$((q_{f}^{\prime},\bm{m}^{\prime}).\varepsilon,\usym{2740})$ is an
inseparability flower with
$\usym{2740}=(q_{f}^{\prime},I,\alpha_{\mathcal{V}},\beta_{\mathcal{V}},\gamma_{\mathcal{V}})$
and $I=\\{i\in\\{1,\ldots d+n\\}\;|\;\bm{m}^{\prime}[i]\neq\omega\\}$. Since
$(q_{f}^{\prime},\bm{m}^{\prime})$ is reachable in
$\mathsf{KM}(\mathcal{V}\times\mathcal{D}_{n})$, we get that
$(q_{f}^{\prime},\bm{m}^{\prime})$ is coverable in
$\mathcal{V}\times\mathcal{D}_{n}$. This shows the coverability of
$((q_{f}^{\prime},\bm{m}^{\prime}).\varepsilon,\usym{2740})$. For all $i\in
I$, the loops $\alpha^{\prime}$, $\beta^{\prime}$, $\gamma^{\prime}$ lead from
a non-$\omega$ counter valuation to the same non-$\omega$ counter valuation in
$\mathsf{KM}(\mathcal{V}\times\mathcal{D}_{n})$ at counter $i$. Since
non-$\omega$ counter valuations are precisely tracked in Karp-Miller graphs,
we deduce that $\delta\varphi(\rho_{\mathcal{V}})[I]=\bm{0}$ for all
$\rho_{\mathcal{V}}\in\\{\alpha_{\mathcal{V}},\beta_{\mathcal{V}},\gamma_{\mathcal{V}}\\}$.
This shows Condition (i) of inseparability flowers. The Conditions (ii),
(iii), (iv) are the same as (a), (b), (c), respectively, and are inherited
from $\alpha^{\prime}$, $\beta^{\prime}$, $\gamma^{\prime}$. It only remains
to show that $(q_{f}^{\prime},\bm{m}^{\prime}).\varepsilon$ is a stem for
$\usym{2740}$. The state $q_{f}^{\prime}$ is already final in $\mathcal{V}$ so
$(q_{f}^{\prime},\bm{m}^{\prime}).\varepsilon$ trivially ends in a final
state. Since $\bm{m}^{\prime}\in{\rm Nature}^{d+n}_{\omega}$ the counters
trivially remain non-negative along
$(q_{f}^{\prime},\bm{m}^{\prime}).\varepsilon$. We also know
$\Omega=\\{1,\ldots,d+n\\}\setminus I=\omega(q_{f}^{\prime},\bm{m}^{\prime})$.
The trivial run $(q_{f}^{\prime},\bm{m}^{\prime}).\varepsilon$ reaches
$(q_{f}^{\prime},\bm{m}^{\prime})$. The argument for $\alpha$, $\beta$,
$\gamma$ remaining non-negative on the counters $I$ when executed from
$(q_{f}^{\prime},\bm{m}^{\prime})$ is similar to the argument for condition
(i). The counters $i\in I$ are non-$\omega$ and thus precisely tracked along
$\alpha$, $\beta$, $\gamma$ from $(q_{f}^{\prime},\bm{m}^{\prime})$. Since the
Karp-Miller graph does not allow transitions into or from negative counter
valuations, we deduce that the valuations of the counters $I$ remain positive
along $\alpha$, $\beta$, $\gamma$ from $(q_{f}^{\prime},\bm{m}^{\prime})$.
This concludes the proof.