[a] [b]

# Separators in Continuous Petri Nets

Michael Blondin0000-0003-2914-2734  and  Javier Esparza0000-0001-9862-4919
Université de Sherbroke, Sherbrooke, Canada<EMAIL_ADDRESS>Technical University of Munich, Munich, Germany<EMAIL_ADDRESS>
###### Abstract.

Leroux has proved that unreachability in Petri nets can be witnessed by a
Presburger separator, i.e. if a marking $\bm{m}_{\text{src}}$ cannot reach a
marking $\bm{m}_{\text{tgt}}$, then there is a formula $\varphi$ of Presburger
arithmetic such that: $\varphi(\bm{m}_{\text{src}})$ holds; $\varphi$ is
forward invariant, i.e., $\varphi(\bm{m})$ and
$\bm{m}\rightarrow\bm{m}^{\prime}$ imply $\varphi(\bm{m}^{\prime}$); and
$\neg\varphi(\bm{m}_{\text{tgt}})$ holds. While these separators could be used
as explanations and as formal certificates of unreachability, this has not yet
been the case due to their worst-case size, which is at least Ackermannian,
and the complexity of checking that a formula is a separator, which is at
least exponential (in the formula size).

We show that, in continuous Petri nets, these two problems can be overcome. We
introduce locally closed separators, and prove that: (a) unreachability can be
witnessed by a locally closed separator computable in polynomial time; (b)
checking whether a formula is a locally closed separator is in NC (so, simpler
than unreachability, which is P-complete).

We further consider the more general problem of (existential) set-to-set
reachability, where two sets of markings are given as convex polytopes. We
show that, while our approach does not extend directly, we can efficiently
certify unreachability via an altered Petri net.

###### Key words and phrases:

Petri net and continuous reachability and separators and certificates.

M. Blondin was supported by a Discovery Grant from the Natural Sciences and
Engineering Research Council of Canada (NSERC), and by the Fonds de recherche
du Québec – Nature et technologies (FRQNT). J. Esparza was supported by an ERC
Advanced Grant (787367: PaVeS)

##  1\. Introduction

Petri nets form a widespread formalism of concurrency with several
applications ranging from the verification of concurrent programs to the
analysis of chemical systems. The reachability problem — which asks whether a
marking $\bm{m}_{\text{src}}$ can reach another marking $\bm{m}_{\text{tgt}}$
— is fundamental as a plethora of problems, such as verifying safety
properties, reduce to it (e.g. [GS92, FMW+17, BMTZ21]).

Leroux has shown that unreachability in Petri nets can be witnessed by a
Presburger _separator_ , i.e., if a marking $\bm{m}_{\text{src}}$ cannot reach
a marking $\bm{m}_{\text{tgt}}$, then there exists a formula $\varphi$ of
Presburger arithmetic such that: $\varphi(\bm{m}_{\text{src}})$ holds;
$\varphi$ is forward invariant, i.e., $\varphi(\bm{m})$ and
$\bm{m}\rightarrow\bm{m}^{\prime}$ imply $\varphi(\bm{m}^{\prime}$); and
$\varphi(\bm{m}_{\text{tgt}})$ does not hold [Ler12]. Intuitively, $\varphi$
“separates” $\bm{m}_{\text{tgt}}$ from the set of markings reachable from
$\bm{m}_{\text{src}}$. Leroux’s result leads to a very simple algorithm to
decide the Petri net reachability problem, consisting of two semi-algorithms;
the first one explores the markings reachable from $\bm{m}_{\text{src}}$, and
halts if and when it hits $\bm{m}_{\text{tgt}}$, while the second enumerates
formulas from Presburger arithmetic, and halts if and when it hits a
separator.

Separators can be used as _explanations_ and as formal _certificates_.
Verifying a safety property can be reduced to proving that a target marking
(or set of markings) is not reachable from a source marking, and a separator
is an invariant of the system that _explains_ why the property holds. Further,
if a reachability tool produces separators, then the user can check that the
properties of a separator indeed hold, and so trust the result even if they do
not trust the tool (e.g., because it has not been verified, or is executed on
a remote faster machine). Yet, in order to be useful as explanations and
certificates, separators have to satisfy two requirements: (1) they should not
be too large, and (2) checking that a formula is a separator should have low
complexity, and, in particular, strictly lower complexity than deciding
reachability. This does not hold, at least in the worst-case, for the
separators of [Ler12]: In the worst case, the separator has a size at least
Ackermannian in the Petri net size (a consequence of the fact that the
reachability problem is Ackermann-complete [LS19, Ler21, CO21]) and the
complexity of the check is at least exponential.

In this paper, we show that, unlike the above, _continuous_ Petri nets do have
separators satisfying properties (1) and (2). Continuous Petri nets are a
relaxation of the standard Petri net model, called _discrete_ in the
following, in which transitions are allowed to fire “fluidly”: instead of
firing once, consuming $i_{p}$ tokens from each input place $p$ and adding
$o_{q}$ tokens to each output place $q$, a transition can fire $\alpha$ times
for any nonnegative real number $\alpha$, consuming and adding $\alpha\cdot
i_{p}$ and $\alpha\cdot o_{q}$ tokens, respectively. Continuous Petri nets are
interesting in their own right [DA10], and moreover as an overapproximation of
the discrete model. In particular, if $\bm{m}_{\text{tgt}}$ is not reachable
from $\bm{m}_{\text{src}}$ under the continuous semantics, then it is also not
under the discrete one. As reachability in continuous Petri nets is P-complete
[FH15], and so drastically more tractable than discrete reachability, this
approximation is used in many tools for the verification of discrete Petri
nets, VAS, or multiset rewriting systems (e.g. [BFHH17, BEH+20, EHJM20]).

It is easy to see that unreachability in continuous Petri nets can be
witnessed by separators expressible in linear arithmetic (the first-order
theory of the reals with addition and order). Indeed, Blondin et al. show in
[BFHH17] that the continuous reachability relation is expressible by an
existential formula $\textit{reach}(\bm{m},\bm{m}^{\prime})$ of linear
arithmetic, from which we can obtain a separator for any pair of unreachable
markings. Namely, for all markings $\bm{m}_{\text{src}}$ and
$\bm{m}_{\text{tgt}}$, if $\bm{m}_{\text{tgt}}$ is not reachable from
$\bm{m}_{\text{src}}$, then the formula
$\textit{sep}_{\bm{m}_{\text{src}}}(\bm{m})\coloneqq\neg\textit{reach}(\bm{m}_{\text{src}},\bm{m})$
is a separator. Further, $\textit{reach}(\bm{m},\bm{m}^{\prime})$ has only
linear size. However, these separators do not satisfy property (2). Indeed,
while the reachability problem for continuous Petri nets is P-complete [FH15],
checking if a formula of linear arithmetic is a separator is coNP-hard, even
for quantifier-free formulas in disjunctive normal form, a very small
fragment. So, the separators arising from [BFHH17] cannot be directly used as
certificates.

In this paper, we overcome this problem. We identify a class of _locally
closed separators_ , satisfying the following properties: unreachability can
always be witnessed by locally closed separators; locally closed separators
can be constructed in polynomial time; and checking whether a formula is a
locally closed separator is computationally strictly111Assuming
$\text{P}\neq\text{NC}$. easier than deciding unreachability. Let us examine
the last claim in more detail. While the reachability problem for continuous
Petri nets is decidable in polynomial time, it is still time consuming for
larger models, which can have tens of thousands of nodes. Indeed, for a Petri
net with $n$ places and $m$ transitions, the algorithm of [FH15] requires to
solve $\mathcal{O}(m^{2})$ linear programming problems in $n$ variables, each
of them with up to $m$ constraints. Moreover, since the problem is P-complete,
it is unlikely that a parallel computer can significantly improve performance.
We prove that, on the contrary, checking if a formula is a locally closed
separator is in NC rather than P-complete, and so efficiently parallelizable.
Further, the checking algorithm only requires to solve linear programming
problems in _a single_ variable.

We further consider “set-to-set reachability” where one must determine whether
there exists a marking $\bm{m}_{\text{src}}\in A$ that can reach some marking
$\bm{m}_{\text{tgt}}\in B$. This naturally generalizes the case where
$A=\\{\bm{m}_{\text{src}}\\}$ and $B=\\{\bm{m}_{\text{tgt}}\\}$. We focus on
the case where sets $A$ and $B$ are convex polytopes, as it can be solved in
polynomial time for continuous Petri nets [BH17]. We prove that,
unfortunately, we cannot validate locally closed separators in NC for set-to-
set reachability. Nonetheless, we show that we can efficiently construct and
validate locally closed separators (respectively in P and NC), at the cost of
working with an altered Petri net that encodes $A$ and $B$.

The paper is organized as follows. Section 2 introduces terminology, and
defines separators (actually, a slightly different notion called bi-
separators). Section 3 recalls the characterization of the reachability
relation given by Fraca and Haddad in [FH15], and derives a characterization
of _un_ reachability suitable for finding bi-separators. Section 4 shows that
checking the separators derivable from [BFHH17] is coNP-hard, and introduces
locally closed bi-separators. Sections 5 and 6 show that locally closed bi-
separators satisfy the aforementioned properties (1) and (2). Finally, Section
7 shows the limitation and extension of our approach to set-to-set
reachability.

##  2\. Preliminaries

#### Numbers, vectors and relations.

We write $\mathbb{N}$, $\mathbb{R}$ and $\mathbb{R}_{+}$ to denote the
naturals (including $0$), reals, and non-negative reals (including $0$). Given
$a,b\in\mathbb{N}$, we write $[a..b]$ to denote $\\{a,a+1,\ldots,b\\}$. Let
$S$ be a finite set. We write $\bm{e}_{s}$ to denote the unit vector
$\bm{e}_{s}\in\mathbb{R}^{S}$ such that $\bm{e}_{s}(s)=1$ and
$\bm{e}_{s}(t)=0$ for all $s,t\in S$ such that $t\neq s$. Given
$\bm{x},\bm{y}\in\mathbb{R}^{S}$, we write $\bm{x}\sim_{S}\bm{y}$ to indicate
that $\bm{x}(s)\sim\bm{y}(s)$ for all $s\in S$, where $\sim$ is a total order
such as $\leq$. We define the _support_ of a vector $\bm{x}\in\mathbb{R}^{S}$
as $\mathrm{supp}(\bm{x})\coloneqq\\{s\in S:\bm{x}(s)>0\\}$. We write
$\bm{x}(S)\coloneqq\sum_{s\in S}\bm{x}(s)$. The _transpose_ of a binary
relation $\mathcal{R}$ is
$\mathcal{R}^{\mathsf{T}}\coloneqq\\{(y,x):(x,y)\in\mathcal{R}\\}$.

#### Petri nets.

A _Petri net_ 222In this work, “Petri nets” stands for “continuous Petri
nets”. In other words, we will consider standard Petri nets, but equipped with
a _continuous_ reachability relation. We will work over the reals, but note
that it is known that working over the rationals is equivalent. For
decidability issues, we will assume input numbers to be rationals. is a tuple
$\mathcal{N}=(P,T,F)$ where $P$ and $T$ are disjoint finite sets, whose
elements are respectively called _places_ and _transitions_ , and where
$F=(\mathbf{F}_{-},\mathbf{F}_{+})$ with $\mathbf{F}_{-},\mathbf{F}_{+}\colon
P\times T\to\mathbb{N}$. For every $t\in T$, vectors
$\Delta_{t}^{-},\Delta_{t}^{+}\in\mathbb{N}^{P}$ are respectively defined as
the column of $\mathbf{F}_{-}$ and $\mathbf{F}_{+}$ associated to $t$, i.e.
$\Delta_{t}^{-}\coloneqq\mathbf{F}_{-}\cdot\bm{e}_{t}$ and
$\Delta_{t}^{+}\coloneqq\mathbf{F}_{+}\cdot\bm{e}_{t}$. A _marking_ is a
vector $\bm{m}\in\mathbb{R}_{+}^{P}$. For every $Q\subseteq P$, let
$\bm{m}(Q)\coloneqq\sum_{p\in Q}\bm{m}(p)$. We say that transition $t$ is
_$\alpha$ -enabled_ if $\bm{m}\geq\alpha\Delta_{t}^{-}$ holds. If this is the
case, then $t$ can be _$\alpha$ -fired_ from $\bm{m}$, which leads to marking
$\bm{m}^{\prime}\coloneqq\bm{m}-\alpha\Delta_{t}^{-}+\alpha\Delta_{t}^{+}$,
which we denote $\bm{m}\xrightarrow{\alpha t}\bm{m}^{\prime}$. A transition is
_enabled_ if it is $\alpha$-enabled for some real number $\alpha>0$. We define
$\mathbf{F}\coloneqq\mathbf{F}_{+}-\mathbf{F}_{-}$ and
$\Delta_{t}\coloneqq\mathbf{F}\cdot\bm{e}_{t}$. In particular,
$\bm{m}\xrightarrow{\alpha t}\bm{m}^{\prime}$ implies
$\bm{m}^{\prime}=\bm{m}+\alpha\Delta_{t}$. For example, for the Petri net of
Figure 1:

$\\{p_{1}\mapsto 2,p_{2}\mapsto 0,p_{3}\mapsto 0,p_{4}\mapsto
0\\}\xrightarrow{(1/2)t_{1}}\\{p_{1}\mapsto 3/2,p_{2}\mapsto 1/2,p_{3}\mapsto
0,p_{4}\mapsto 0\\}.$

Moreover, w.r.t. to orderings $p_{1}<\cdots<p_{4}$ (rows) and
$t_{1}<\cdots<t_{4}$ (columns):

$\mathbf{F}_{-}=\begin{bmatrix}1&2&2&0\\\ 0&0&1&0\\\ 0&0&0&1\\\
0&1&0&0\end{bmatrix},\ \mathbf{F}_{+}=\begin{bmatrix}0&0&1&0\\\ 1&0&0&0\\\
0&1&1&0\\\ 0&1&0&1\end{bmatrix}\ \text{ and }\
\mathbf{F}=\begin{bmatrix}-1&-2&-1&0\\\ 1&0&-1&0\\\ 0&1&1&-1\\\
0&0&0&1\end{bmatrix}.$

$p_{1}$$t_{1}$$p_{2}$$t_{3}$$t_{2}$$p_{4}$$p_{3}$$t_{4}$$2$$2$ Figure 1. A
Petri net and two markings $\bm{m}_{\text{src}}=\\{p_{1}\mapsto 2,p_{2}\mapsto
0,p_{3}\mapsto 0,p_{4}\mapsto 0\\}$ (black circles) and
$\bm{m}_{\text{tgt}}=\\{p_{1}\mapsto 0,p_{2}\mapsto 0,p_{3}\mapsto
0,p_{4}\mapsto 1\\}$ (colored squares).

A sequence $\sigma=\alpha_{1}t_{1}\cdots\alpha_{n}t_{n}$ is a _firing
sequence_ from $\bm{m}_{\text{src}}$ to $\bm{m}_{\text{tgt}}$ if there are
markings $\bm{m}_{0},\ldots,\bm{m}_{n}$ satisfying
$\bm{m}_{\text{src}}=\bm{m}_{0}\xrightarrow{\alpha_{1}t_{1}}\bm{m}_{1}\cdots\xrightarrow{\alpha_{n}t_{n}}\bm{m}_{n}=\bm{m}_{\text{tgt}}$.
We write $\bm{m}_{0}\xrightarrow{\sigma}\bm{m}_{n}$. We say that
$\bm{m}_{\text{src}}$ _enables_ $\sigma$, and that $\bm{m}_{\text{tgt}}$
enables $\sigma$ backwards, or _backward-enables_ $\sigma$. The _support_ of
$\sigma$ is the set $\\{t_{1},\ldots,t_{n}\\}$. For example, for the Petri net
of Figure 1, we have
$\bm{m}_{\text{src}}\xrightarrow{\sigma}\bm{m}_{\text{tgt}}$ where

$\displaystyle\bm{m}_{\text{src}}$ $\displaystyle=\\{p_{1}\mapsto
2,p_{2}\mapsto 0,p_{3}\mapsto 0,p_{4}\mapsto 0\\},$
$\displaystyle\bm{m}_{\text{tgt}}$ $\displaystyle=\\{p_{1}\mapsto
0,p_{2}\mapsto 0,p_{3}\mapsto 0,p_{4}\mapsto 1\\},$ $\displaystyle\sigma$
$\displaystyle=(1/2)t_{1}\ (1/2)t_{3}\ (1/2)t_{4}\ (1/2)t_{2}\ (1/2)t_{4}.$

We write $\bm{m}\xrightarrow{}\bm{m}^{\prime}$ to denote that
$\bm{m}\xrightarrow{\alpha t}\bm{m}^{\prime}$ for some transition $t$ and some
$\alpha>0$, and $\bm{m}\xrightarrow{}^{*}\bm{m}^{\prime}$ to denote that
$\bm{m}\xrightarrow{\sigma}\bm{m}^{\prime}$ for some firinng sequence
$\sigma$.

The Petri net $\mathcal{N}_{U}$ is obtained by removing transitions
$T\setminus U$ from $\mathcal{N}$. In particular,
$\bm{m}\xrightarrow{}^{U^{*}}\bm{m}^{\prime}$ holds in $\mathcal{N}$ iff
$\bm{m}\xrightarrow{}^{*}\bm{m}^{\prime}$ holds in $\mathcal{N}_{U}$.

The _transpose_ of $\mathcal{N}=(P,T,(\mathbf{F}_{-},\mathbf{F}_{+}))$ is
$\mathcal{N}^{\mathsf{T}}\coloneqq(P,T,(\mathbf{F}_{+},\mathbf{F}_{-}))$. We
have $\bm{m}_{\text{src}}\xrightarrow{\sigma}\bm{m}_{\text{tgt}}$ in
$\mathcal{N}$ iff $\bm{m}_{\text{tgt}}\xrightarrow{\tau}\bm{m}_{\text{src}}$
in $\mathcal{N}^{\mathsf{T}}$, where $\tau$ is the reverse of $\sigma$. For
$U\subseteq T$, we write $U^{\mathsf{T}}$ to denote $U$ in the context of
$\mathcal{N}^{\mathsf{T}}$.

#### Linear arithmetic and Farkas’ lemma.

An _atomic proposition_ is a linear inequality of the form $\bm{a}\bm{x}\leq
b$ or $\bm{a}\bm{x}<b$, where $b$ and the components of $\bm{a}$ are over
$\mathbb{R}$. Such a proposition is _homogeneous_ if $b=0$. A _linear formula_
is a first-order formula over atomic propositions with variables ranging over
$\mathbb{R}_{+}$ (the classical definition uses $\mathbb{R}$, but in our
context variables will encode markings.) The _solutions_ of a linear formula
$\varphi$, denoted $\llbracket\varphi\rrbracket$, are the assignments to the
free variables of $\varphi$ that satisfy $\varphi$. A linear formula is
_homogeneous_ if all of its atomic propositions are homogeneous. For every
formula $\varphi(\bm{x},\bm{y})$ where $\bm{x}$ and $\bm{y}$ have the same
arity, we write $\varphi^{\mathsf{T}}$ to denote the formula that
syntactically swaps $\bm{x}$ and $\bm{y}$, so that
$\llbracket\varphi^{\mathsf{T}}\rrbracket=\llbracket\varphi\rrbracket^{\mathsf{T}}$.
Throughout the paper, we will use Farkas’ lemma, a fundamental result of
linear arithmetic that rephrases the absence of solution to a system into the
existence of one for another system. The lemma has many variants, of which we
give just one.

######  Lemma 1 (Farkas’ lemma).

Let $\mathbf{A}\in\mathbb{R}^{m\times n}$ and $\bm{b}\in\mathbb{R}^{m}$. The
formula $\mathbf{A}\bm{x}\leq\bm{b}$ has no solution iff
$\mathbf{A}^{\mathsf{T}}\bm{y}=\bm{0}\land\bm{b}^{\mathsf{T}}\bm{y}<0\land\bm{y}\geq\bm{0}$
has a solution.

Indeed, it cannot be the case that both system have solutions, as one could
otherwise derive the contradiction
$0=\bm{x}^{\mathsf{T}}\mathbf{A}^{\mathsf{T}}\bm{y}\leq\bm{b}^{\mathsf{T}}\bm{y}<0$.
For some geometric intuition, consider the case in which $m=n$ (the general
case is very similar), and assume that some vectors $\bm{x}$ and $\bm{y}$
satisfy the conditions. We derive a contradiction as follows:

  1. (1)

$\mathbf{A}^{\mathsf{T}}\bm{y}=\bm{0}\wedge\bm{y}\geq\bm{0}$ states that
$\bm{y}$ is a vector in the positive orthant perpendicular to all column
vectors of $\mathbf{A}$. Let $H$ be the hyperplane with normal vector
$\bm{y}$. Then all points of the positive orthant lie on the same side of $H$.

  2. (2)

$\bm{b}^{\mathsf{T}}\bm{y}<0$ states that $\bm{y}$ and $\bm{b}$ lie on
opposite sides of $H$. So, $\bm{b}$ and the positive orthant also lie on
opposite sides of $H$.

  3. (3)

$\bm{b}-\mathbf{A}\bm{x}\geq\bm{0}$ is equivalent to
$\bm{b}=\mathbf{A}\bm{x}+\bm{p}$ for some vector $\bm{p}$ in the positive
orthant. Since $\mathbf{A}\bm{x}\in H$ ($\mathbf{A}\bm{x}$ is a linear
combination of the columns of $\mathbf{A}$), this implies that $\bm{b}$ and
$\bm{p}$ lie on the same side of $H$, contradicting (2).

###  2.1. Separators and bi-separators

Let us fix a Petri net $\mathcal{N}=(P,T,F)$ and two markings
$\bm{m}_{\text{src}},\bm{m}_{\text{tgt}}\in\mathbb{R}_{+}^{P}$.

A _separator_ for $(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})$ is a linear
formula $\varphi$ over $\mathbb{R}_{+}^{P}$ such that:

  1. (1)

$\bm{m}_{\text{src}}\in\llbracket\varphi\rrbracket$;

  2. (2)

$\varphi$ is _forward invariant_ , i.e.,
$\bm{m}\in\llbracket\varphi\rrbracket$ and
$\bm{m}\xrightarrow{}\bm{m^{\prime}}$ implies
$\bm{m}^{\prime}\in\llbracket\varphi\rrbracket$; and

  3. (3)

$\bm{m}_{\text{tgt}}\notin\llbracket\varphi\rrbracket$.

It follows immediately from the definition that if there is a separator
$\varphi$ for $(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})$, then
$\bm{m}_{\text{src}}\not\xrightarrow{}^{*}\bm{m}_{\text{tgt}}$. Thus, in order
to show that $\bm{m}_{\text{src}}\not\xrightarrow{}^{*}\bm{m}_{\text{tgt}}$ in
$\mathcal{N}$, we can either give a separator for
$(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})$ w.r.t. $\mathcal{N}$, or a
separator for $(\bm{m}_{\text{tgt}},\bm{m}_{\text{src}})$ w.r.t.
$\mathcal{N}^{\mathsf{T}}$. Let us call them _forward_ and _backward_
separators. Loosely speaking, a forward separator shows that
$\bm{m}_{\text{tgt}}$ is not among the markings reachable from
$\bm{m}_{\text{src}}$, and a backward separator shows that
$\bm{m}_{\text{src}}$ is not among the markings backward-reachable from
$\bm{m}_{\text{tgt}}$. Bi-separators are formulas from which we can easily
obtain forward and backward separators. The symmetry w.r.t. forward and
backward reachability make them easier to handle.

A linear formula $\varphi$ over $\mathbb{R}_{+}^{P}\times\mathbb{R}_{+}^{P}$
is

  * •

_forward invariant_ if
$(\bm{m},\bm{m}^{\prime})\in\llbracket\varphi\rrbracket$ and
$\bm{m}^{\prime}\xrightarrow{}\bm{m}^{\prime\prime}$ imply
$(\bm{m},\bm{m}^{\prime\prime})\in\llbracket\varphi\rrbracket$;

  * •

_backward invariant_ if
$(\bm{m}^{\prime},\bm{m}^{\prime\prime})\in\llbracket\varphi\rrbracket$ and
$\bm{m}\xrightarrow{}\bm{m}^{\prime}$ imply
$(\bm{m},\bm{m}^{\prime\prime})\in\llbracket\varphi\rrbracket$; and

  * •

_bi-invariant_ if it is forward and backward invariant.

A _bi-separator_ for $(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})$ is a bi-
invariant linear formula $\varphi$ such that
$(\bm{m}_{\text{src}},\bm{m}_{\text{src}})\in\llbracket\varphi\rrbracket$,
$(\bm{m}_{\text{tgt}},\bm{m}_{\text{tgt}})\in\llbracket\varphi\rrbracket$ and
$(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})\notin\llbracket\varphi\rrbracket$.

The following proposition shows how to obtain separators from bi-separators.

######  Proposition 2.

Let $\varphi$ be a bi-separator for
$(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})$. The following holds:

  * •

$\mathmakebox[27pt][l]{\psi(\bm{m})}\coloneqq\varphi(\bm{m}_{\text{src}},\bm{m})$
is a separator for $(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})$ in
$\mathcal{N}$;

  * •

$\mathmakebox[27pt][l]{\psi^{\prime}(\bm{m})}\coloneqq\varphi(\bm{m},\bm{m}_{\text{tgt}})$
is a separator for $(\bm{m}_{\text{tgt}},\bm{m}_{\text{src}})$ in
$\mathcal{N}^{\mathsf{T}}$.

######  Proof 2.1.

It suffices to prove the first statement, the second is symmetric. We have
$\bm{m}_{\text{src}}\in\llbracket\psi\rrbracket$ and
$\bm{m}_{\text{tgt}}\notin\llbracket\psi\rrbracket$ as
$(\bm{m}_{\text{src}},\bm{m}_{\text{src}})\in\llbracket\varphi\rrbracket$ and
$(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})\notin\llbracket\varphi\rrbracket$.

It remains to show that $\psi$ is forward invariant. Let
$\bm{m}\in\llbracket\psi\rrbracket$ and $\bm{m}\xrightarrow{\alpha
t}\bm{m}^{\prime}$. Since
$(\bm{m}_{\text{src}},\bm{m})\in\llbracket\varphi\rrbracket$ and $\varphi$ is
forward invariant, it is the case that
$(\bm{m}_{\text{src}},\bm{m}^{\prime})\in\llbracket\varphi\rrbracket$. Hence,
$\bm{m}^{\prime}\in\llbracket\psi\rrbracket$ as desired.

##  3\. A characterization of unreachability

Given a Petri net $\mathcal{N}=(P,T,F)$, a set of transitions $U\subseteq T$,
and two markings
$\bm{m}_{\text{src}},\bm{m}_{\text{tgt}}\in\mathbb{R}_{+}^{P}$, we write
$\bm{m}_{\text{src}}\xhookrightarrow{}^{U}\bm{m}_{\text{tgt}}$ to denote that
$\bm{m}_{\text{src}}\xrightarrow{\sigma}\bm{m}_{\text{tgt}}$ for some sequence
$\sigma$ with support $U$. In words,
$\bm{m}_{\text{src}}\xrightarrow{\sigma}\bm{m}_{\text{tgt}}$ denotes that
$\bm{m}_{\text{tgt}}$ can be reached from $\bm{m}_{\text{src}}$ by firing
_all_ transitions of $U$ and _only_ transitions of $U$. We say that
$\bm{m}_{\text{tgt}}$ is _$U$ -reachable_ from $\bm{m}_{\text{src}}$

In [FH15], Fraca and Haddad gave the following characterization of
$U$-reachability in continuous Petri nets:

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

Let $\mathcal{N}=(P,T,F)$ be a Petri net, let $U\subseteq T$, and let
$\bm{m}_{\text{src}},\bm{m}_{\text{tgt}}\in\mathbb{R}_{+}^{P}$. It is the case
that $\bm{m}_{\text{src}}\xhookrightarrow{}^{U}\bm{m}_{\text{tgt}}$ iff the
following conditions hold:

  1. (1)

some vector $\bm{x}\in\mathbb{R}_{+}^{T}$ with support $U$ satisfies
$\bm{m}_{\text{src}}+\mathbf{F}\bm{x}=\bm{m}_{\text{tgt}}$,

  2. (2)

some firing sequence $\sigma$ with support $U$ is enabled at
$\bm{m}_{\text{src}}$, and

  3. (3)

some firing sequence $\tau$ with support $U$ is backward-enabled at
$\bm{m}_{\text{tgt}}$.

Furthermore, these conditions can be checked in polynomial time.

Theorem 3 provides a witness of $U$-reachability in the shape of a vector
$\bm{x}$ and two firing sequences $\sigma$ and $\tau$. In this section, we
find a witness of $U$-unreachability, i.e., a witness showing that
$\bm{m}_{\text{src}}\not\xhookrightarrow{}^{U}\bm{m}_{\text{tgt}}$.

Consider the logical form of Theorem 3:

$\begin{gathered}\bm{m}_{\text{src}}\xhookrightarrow{}^{U}\bm{m}_{\text{tgt}}\\\
\iff(\exists\bm{x}\in\mathbb{R}_{+}^{T}\colon
A_{1}(\bm{x}))\land(\exists\sigma\in T^{*}\colon
A_{2}(\sigma))\land(\exists\tau\in T^{*}\colon A_{3}(\tau)),\end{gathered}$
(1)

where $A_{1}(\bm{x}),A_{2}(\sigma),A_{3}(\tau)$ denote that $\bm{x}$ has
support $U$ and satisfies
$\bm{m}_{\text{src}}+\mathbf{F}\bm{x}=\bm{m}_{\text{tgt}}$, that $\sigma$ has
support $U$ and is enabled at $\bm{m}_{\text{src}}$, and that $\tau$ has
support $U$ and is backward-enabled at $\bm{m}_{\text{tgt}}$, respectively.
The theorem is logically equivalent to

$\begin{gathered}\bm{m}_{\text{src}}\not\xhookrightarrow{}^{U}\bm{m}_{\text{tgt}}\\\
\iff(\forall\bm{x}\in\mathbb{R}_{+}^{T}\colon\neg
A_{1}(\bm{x}))\lor(\forall\sigma\in T^{*}\colon\neg
A_{2}(\sigma))\lor(\forall\tau\in T^{*}\colon\neg A_{3}(\tau)).\end{gathered}$
(2)

To obtain a witness of $U$-unreachability, we proceed in two steps:

  * •

In Section 3.1, we define predicates $B_{2}(Q)$ and $B_{3}(R)$, where
$Q,R\subseteq P$, satisfying

$\begin{gathered}(\forall\sigma\in T^{*}\colon\neg
A_{2}(\sigma))\Longleftrightarrow(\exists Q\subseteq P\colon B_{2}(Q)),\\\
(\forall\tau\in T^{*}\colon\neg A_{3}(\tau))\Longleftrightarrow(\exists
R\subseteq P\colon B_{3}(R)).\\\ \end{gathered}$ (3)

  * •

In Section 3.2, we define a predicate $B_{1}(\bm{y})$, where
$\bm{y}\in\mathbb{R}_{+}^{P}$, satisfying

$\begin{gathered}(\forall\bm{x}\in\mathbb{R}_{+}^{T}\colon\neg
A_{1}(\bm{x}))\Longrightarrow(\exists\bm{y}\in\mathbb{R}_{+}^{P}\colon
B_{1}(\bm{y}))\Longrightarrow\bm{m}_{\text{src}}\not\xhookrightarrow{}^{U}\bm{m}_{\text{tgt}}.\end{gathered}$
(4)

Applying propositional logic to (2), (3), and (4) we obtain:

$\begin{gathered}\bm{m}_{\text{src}}\not\xhookrightarrow{}^{U}\bm{m}_{\text{tgt}}\\\
\iff(\exists\bm{y}\in\mathbb{R}_{+}^{P}\colon B_{1}(\bm{y}))\vee(\exists
Q\subseteq P\colon B_{2}(Q))\vee(\exists R\subseteq P\colon
B_{3}(R)).\end{gathered}$ (5)

This shows that $U$-unreachability is witnessed either by a vector $\bm{y}$, a
set $Q$, or a set $R$.

###  3.1. The predicates $B_{2}(Q)$ and $B_{3}(R)$

The predicates $B_{2}(Q)$ and $B_{3}(R)$ were already implicitly defined in
[FH15] in terms of sets of places called _siphons_ and _traps_. Given a set of
places $X$, let ${\rm Phys.~{}Rev.~{}E}{X}$ (resp. ${{X}^{\bullet}}$) be the
set of transitions $t$ such that $\mathbf{F}_{+}(p,t)>0$ (resp.
$\mathbf{F}_{-}(p,t)>0$) for some $p\in X$. A _siphon_ of $\mathcal{N}$ is a
subset $Q$ of places such that ${\rm
Phys.~{}Rev.~{}E}{Q}\subseteq{{Q}^{\bullet}}$. A _trap_ is a subset $R$ of
places such that ${{R}^{\bullet}}\subseteq{\rm Phys.~{}Rev.~{}E}{R}$.
Informally, empty siphons remain empty, and marked traps remain marked.
Formally, if $\bm{m}\xrightarrow{}\bm{m}^{\prime}$, then $\bm{m}(Q)=0$ implies
$\bm{m}^{\prime}(Q)=0$, and $\bm{m}(R)>0$ implies $\bm{m}^{\prime}(R)>0$.
Fraca and Haddad proved in [FH15]:

######  Proposition 4 ([FH15]).

Let $\mathcal{N}=(P,T,F)$ be a Petri net, let $U\subseteq T$, and let
$\bm{m}\in\mathbb{R}_{+}^{P}$. The following statements hold:

  * •

No firing sequence with support $U$ is enabled at $\bm{m}$ iff there exists a
siphon $Q$ of $\mathcal{N}_{U}$ such that ${{Q}^{\bullet}}\neq\emptyset$ and
$\bm{m}(Q)=0$;

  * •

No firing sequence with support $U$ is backward-enabled at $\bm{m}$ iff there
exists a trap $R$ of $\mathcal{N}_{U}$ such that ${\rm
Phys.~{}Rev.~{}E}{R}\neq\emptyset$ and $\bm{m}(R)=0$.

The if-direction of the proposition is easy to prove. A siphon $Q$ of
$\mathcal{N}_{U}$ satisfies ${{Q}^{\bullet}}\subseteq U$. Since $Q$ is empty
at $\bm{m}$, if we only fire transitions from $U$ then $Q$ remains empty, and
so no transition of ${{Q}^{\bullet}}$ ever becomes enabled. So, transitions of
${{Q}^{\bullet}}$ can only fire after transitions that do not belong to $U$
have fired first. But no such firing sequence has support $U$, and we are
done. The case of traps is analogous. For the only-if direction, we refer the
reader to [FH15].

By Proposition 4, the predicates

$\displaystyle B_{2}(Q)$ $\displaystyle\coloneqq\text{$Q$ is a siphon of
$\mathcal{N}_{U}$ such that ${{Q}^{\bullet}}\neq\emptyset$ and
$\bm{m}_{\text{src}}(Q)=0$},$ $\displaystyle B_{3}(R)$
$\displaystyle\coloneqq\text{$R$ is a trap of $\mathcal{N}_{U}$ such that
${\rm Phys.~{}Rev.~{}E}{R}\neq\emptyset$ and $\bm{m}_{\text{tgt}}(R)=0$},$

satisfy (3).

###  3.2. The predicate $B_{1}(\mathbf{y})$

In order to define the predicate $B_{1}(\bm{y})$, we need to introduce
_exclusion functions_.

Let $\mathcal{N}=(P,T,F)$ be a Petri net, let
$\bm{m}_{\text{src}},\bm{m}_{\text{tgt}}\in\mathbb{R}_{+}^{P}$ and let
$S\subseteq S^{\prime}\subseteq T$. An _exclusion function for
$(S,S^{\prime})$_ is a function $f\colon\mathbb{R}_{+}^{P}\to\mathbb{R}$ such
that

  1. (1)

for all $t\in S^{\prime}$, if $\bm{m}\xrightarrow{t}\bm{m}^{\prime}$ then
$f(\bm{m})\leq f(\bm{m}^{\prime})$; and

  2. (2)

either $f(\bm{m}_{\text{src}})>f(\bm{m}_{\text{tgt}})$, or
$f(\bm{m}_{\text{src}})=f(\bm{m}_{\text{tgt}})$ and there exists $t\in S$ such
that if $\bm{m}\xrightarrow{t}\bm{m}^{\prime}$ then
$f(\bm{m})<f(\bm{m}^{\prime})$.

An _exclusion function for $S$_ is an exclusion function for $(S,S)$. An
exclusion function $f\colon\mathbb{R}_{+}^{P}\to\mathbb{R}$ is _linear_ if
there exists a vector $\bm{y}\in\mathbb{R}^{P}$ such that
$f(\bm{m})=\sum_{p\in P}\bm{y}(p)\cdot\bm{m}(p)$ for every
$\bm{m}\in\mathbb{R}_{+}^{P}$. Abusing language, we speak of the linear
exclusion function $\bm{y}$.

We define:

$B_{1}(\bm{y})\coloneqq\text{$\bm{y}$ is a linear exclusion function for
$U$}.$

We can easily show the second implication of (4), namely that an exclusion
function for $U$ is a witness of $U$-unreachabilty:

######  Lemma 5.

If there exists a (linear) exclusion function for $U\subseteq T$, then
$\bm{m}_{\text{src}}\not\xhookrightarrow{}^{U}\bm{m}_{\text{tgt}}$.

######  Proof 3.1.

Let $f$ be an exclusion function for $U$. Call $f(\bm{m})$ the _value_ of
$\bm{m}$. By the definition of an exclusion function, either
$\bm{m}_{\text{tgt}}$ has lower value than $\bm{m}_{\text{src}}$ and no
transition of $U$ decreases the value, or $\bm{m}_{\text{src}}$ and
$\bm{m}_{\text{tgt}}$ have the same value, no transition of $U$ decreases the
value, and at least one transition of $U$ increases it. So, it is impossible
to reach $\bm{m}_{\text{tgt}}$ from $\bm{m}_{\text{src}}$ by firing _all_ and
_only_ the transitions of $U$.

The first implication of (4) is shown in the forthcoming Proposition 7. We
first need a technical lemma, one of the many consequences of Farkas’ lemma.
Recall that, given ${\sim}\in\\{\leq,=,\geq\\}$, the notation
$\bm{x}\sim_{U}\bm{y}$ stands for “$\bm{x}(t)\sim\bm{y}(t)$ for all $t\in U$”.

######  Lemma 6.

The system $\exists\bm{x}\geq\bm{0}:\mathbf{A}\bm{x}=\bm{b}\land
U\subseteq\mathrm{supp}(\bm{x})\subseteq V$ has no solution iff this system
has a solution:
$\exists\bm{y}:\mathbf{A}^{\mathsf{T}}\bm{y}\geq_{V}\bm{0}\land\bm{b}^{\mathsf{T}}\bm{y}\leq
0\land\bm{b}^{\mathsf{T}}\bm{y}<\sum_{t\in
U}(\mathbf{A}^{\mathsf{T}}\bm{y})(t)$.

Rather than giving a proof (which appears in the appendix), let us give some
geometric intuition. Consider the case in which $\emptyset=U\subseteq V=T$. In
this case, $U\subseteq\mathrm{supp}(\bm{x})\subseteq V$ holds vacuously, and
we can replace “$\geq_{V}$” by “$\geq$” and
“$\bm{b}^{\mathsf{T}}\bm{y}<\sum_{t\in U}(\mathbf{A}^{\mathsf{T}}\bm{y})(t)$”
by “$\bm{b}^{\mathsf{T}}\bm{y}<0$”. The conditions can now be geometrically
interpreted as follows:

  1. (1)

$\exists\bm{x}\geq\bm{0}:\mathbf{A}\bm{x}=\bm{b}$. The vector $\bm{b}$ lies in
the cone spanned by the columns of $\mathbf{A}$.

  2. (2)

$\exists\bm{y}:\mathbf{A}^{\mathsf{T}}\bm{y}\geq\bm{0}\land\bm{b}^{\mathsf{T}}\bm{y}<0$.
There exists a hyperplane $H$ (the hyperplane perpendicular to $\bm{y}$) such
that all columns of $\mathbf{A}$ lie on the same side of the hyperplane as
$\bm{y}$ (because $\mathbf{A}^{\mathsf{T}}\bm{y}\geq\bm{0}$), while $\bm{b}$
lies on the opposite side (because $\bm{b}^{\mathsf{T}}\bm{y}<0$).

Clearly, the two conditions are incompatible. The conditions of the general
case $U\subseteq V$ are similar, but restricted to the columns of $\mathbf{A}$
for which $\bm{x}$ is positive: (1) now states that $\bm{b}$ lies in the cone
spanned by these columns, and (2) that some hyperplane separates these columns
from $\bm{b}$.

We are now ready to prove the first implication of (4), namely

$(\forall\bm{x}\in\mathbb{R}_{+}^{T}\colon\neg
A_{1}(\bm{x}))\Longrightarrow(\exists\bm{y}\in\mathbb{R}_{+}^{P}\colon\neg
B_{1}(\bm{y})).$

Recall that $A_{1}(\bm{x})$ means that $\bm{x}$ has support $U$ and satisfies
$\bm{m}_{\text{src}}+\mathbf{F}\bm{x}=\bm{m}_{\text{tgt}}$, and
$B_{1}(\bm{y})$ means that $\bm{y}$ is a linear exclusion function for $U$. We
prove a slightly more general result; the first implication of (4) is the
special case $S=U=S^{\prime}$:

######  Proposition 7.

Let $\mathcal{N}=(P,T,F)$ be a Petri net, let
$\bm{m}_{\text{src}},\bm{m}_{\text{tgt}}\in\mathbb{R}_{+}^{P}$, and let
$S\subseteq S^{\prime}\subseteq T$. If no vector $\bm{x}\in\mathbb{R}_{+}^{T}$
satisfies $S\subseteq\mathrm{supp}(\bm{x})\subseteq S^{\prime}$ and
$\bm{m}_{\text{src}}+\mathbf{F}\bm{x}=\bm{m}_{\text{tgt}}$, then there exists
a linear exclusion function for $(S,S^{\prime})$.

######  Proof 3.2.

Assume no such $\bm{x}\in\mathbb{R}_{+}^{T}$ exists. Let
$\bm{b}\coloneqq\bm{m}_{\text{tgt}}-\bm{m}_{\text{src}}$. By Lemma 6, there
exists $\bm{y}\in\mathbb{R}^{P}$ such that:
$\mathbf{F}^{\mathsf{T}}\bm{y}\geq_{S^{\prime}}\bm{0}\land\bm{b}^{\mathsf{T}}\bm{y}\leq
0\land\bm{b}^{\mathsf{T}}\bm{y}<\sum_{s\in
S}(\mathbf{F}^{\mathsf{T}}\bm{y})_{s}$. We show that
$f(\bm{k})\coloneqq\bm{y}^{\mathsf{T}}\bm{k}$ is a linear exclusion function
for $(S,S^{\prime})$.

  1. (1)

We have
$f(\bm{m}_{\text{tgt}})-f(\bm{m}_{\text{src}})=\bm{y}^{\mathsf{T}}\bm{m}_{\text{tgt}}-\bm{y}^{\mathsf{T}}\bm{m}_{\text{src}}=\bm{y}^{\mathsf{T}}(\bm{m}_{\text{tgt}}-\bm{m}_{\text{src}})=\bm{y}^{\mathsf{T}}\bm{b}=\bm{b}^{\mathsf{T}}\bm{y}\leq
0,$ and hence $f(\bm{m}_{\text{tgt}})\leq f(\bm{m}_{\text{src}})$.

  2. (2)

Let $\bm{m}\xrightarrow{\lambda s}\bm{m}^{\prime}$ with $s\in S^{\prime}$ and
$\lambda\in\mathbb{R}_{+}$. We have
$\bm{m}^{\prime}=\bm{m}+\lambda\mathbf{F}\bm{e}_{s}$. Thus:
$f(\bm{m}^{\prime})=\bm{y}^{\mathsf{T}}\bm{m}^{\prime}=\bm{y}^{\mathsf{T}}\bm{m}+\lambda(\bm{y}^{\mathsf{T}}\mathbf{F})\bm{e}_{s}=\bm{y}^{\mathsf{T}}\bm{m}+\lambda(\mathbf{F}^{\mathsf{T}}\bm{y})^{\mathsf{T}}\bm{e}_{s}\geq\bm{y}^{\mathsf{T}}\bm{m}=f(\bm{m})$,
where the inequality follows from $\lambda>0$,
$\mathbf{F}^{\mathsf{T}}\bm{y}\geq_{S^{\prime}}\bm{0}$ and $s\in S^{\prime}$.

  3. (3)

Recall that $\bm{b}^{\mathsf{T}}\bm{y}\leq 0$ and $\sum_{s\in
S}(\mathbf{F}^{\mathsf{T}}\bm{y})_{s}>\bm{b}^{\mathsf{T}}\bm{y}$. If the
latter sum equals zero, then $\bm{b}^{\mathsf{T}}\bm{y}<0$, and hence we are
done since
$f(\bm{m}_{\text{tgt}})-f(\bm{m}_{\text{src}})=\bm{b}^{\mathsf{T}}\bm{y}<0$.

Otherwise, we have $\sum_{s\in S}(\mathbf{F}^{\mathsf{T}}\bm{y})_{s}>0$ since
$S\subseteq S^{\prime}$ and
$\mathbf{F}^{\mathsf{T}}\bm{y}\geq_{S^{\prime}}\bm{0}$. Therefore, there
exists a transition $s\in S$ such that
$(\mathbf{F}^{\mathsf{T}}\bm{y})_{s}>0$. Let
$\bm{m}\xrightarrow{s}\bm{m}^{\prime}$. We have
$\bm{m}^{\prime}=\bm{m}+\lambda\mathbf{F}\bm{e}_{s}$ for some $\lambda>0$.
Thus,
$f(\bm{m}^{\prime})=\bm{y}^{\mathsf{T}}\bm{m}+\lambda(\mathbf{F}^{\mathsf{T}}\bm{y})^{\mathsf{T}}\bm{e}_{s}>\bm{y}^{\mathsf{T}}\bm{m}=f(\bm{m})$,
where the inequality holds by $\lambda>0$ and
$(\mathbf{F}^{\mathsf{T}}\bm{y})_{s}>0$.

Putting together Theorem 3 with Proposition 4, and Proposition 7, we obtain
the following characterization of unreachability:

######  Proposition 8.

Let $\mathcal{N}=(P,T,F)$ be a Petri net, let $U\subseteq T$, and
$\bm{m}_{\text{src}},\bm{m}_{\text{tgt}}\in\mathbb{R}_{+}^{P}$. It is the case
that $\bm{m}_{\text{src}}\not\xhookrightarrow{}^{U}\bm{m}_{\text{tgt}}$ iff

  1. (1)

there exists a linear exclusion function for $U$, or

  2. (2)

there exists a siphon $Q$ of $\mathcal{N}_{U}$ such that
${{Q}^{\bullet}}\neq\emptyset$ and $\bm{m}_{\text{src}}(Q)=0$, or

  3. (3)

there exists a trap $R$ of $\mathcal{N}_{U}$ such that ${\rm
Phys.~{}Rev.~{}E}{R}\neq\emptyset$ and $\bm{m}_{\text{tgt}}(R)=0$.

This proposition shows that we can produce a witness of unreachability for a
given support either as an exclusion function, a siphon, or a trap. The
following example shows how to use this to show that a marking cannot be
reached from another one.

Consider the Petri net of Figure 1, but with
$\bm{m}_{\text{tgt}}\coloneqq\\{p_{1}\mapsto 0,p_{2}\mapsto 0,p_{3}\mapsto
1,p_{4}\mapsto 0\\}$ as target. We prove
$\bm{m}_{\text{src}}\not\xrightarrow{}^{*}\bm{m}_{\text{tgt}}$. For the sake
of contradiction, assume
$\bm{m}_{\text{src}}\xhookrightarrow{}^{U}\bm{m}_{\text{tgt}}$ for some
$U\subseteq T$. We proceed in several steps:

  * •

_Claim: $t_{4}\notin U$_. The function $f(\bm{m})\coloneqq\bm{m}(p_{4})$ is an
exclusion function for $T$. Indeed, since no transition decreases the number
of tokens of $p_{4}$, $\bm{m}\xrightarrow{t}\bm{m}^{\prime}$ implies
$f(\bm{m})\leq f(\bm{m}^{\prime})$ for every transition $t\in T$. Furthermore,
$f(\bm{m}_{\text{src}})=0=f(\bm{m}_{\text{tgt}})$, and, since $t_{4}$ adds
tokens to $p_{4}$, $\bm{m}\xrightarrow{t_{4}}\bm{m}^{\prime}$ implies
$f(\bm{m})<f(\bm{m}^{\prime})$. It follows that no firing sequence from
$\bm{m}_{\text{src}}$ to $\bm{m}_{\text{tgt}}$ can fire $t_{4}$. Therefore,
$\bm{m}_{\text{tgt}}$ is reachable from $\bm{m}_{\text{src}}$ in $\mathcal{N}$
iff it is reachable from $\bm{m}_{\text{src}}$ in
$\mathcal{N}_{T\setminus\\{t_{4}\\}}$.

  * •

_Claim: $t_{2}\notin U$_. The set $Q\coloneqq\\{p_{4}\\}$ is a siphon of
$\mathcal{N}_{T\setminus\\{t_{4}\\}}$ (but not of $\mathcal{N}$). Since
$\bm{m}_{\text{src}}(Q)=0$, it is impossible to use transitions of
$\mathcal{N}_{T\setminus\\{t_{4}\\}}$ that consume from $Q$, i.e. transitions
of ${{Q}^{\bullet}}=\\{t_{2}\\}$. So $\bm{m}_{\text{tgt}}$ is reachable from
$\bm{m}_{\text{src}}$ in $\mathcal{N}$ iff it is reachable from
$\bm{m}_{\text{src}}$ in $\mathcal{N}_{T\setminus\\{t_{2},t_{4}\\}}$

  * •

_Claim: $t_{1},t_{3}\notin U$_. The set $R\coloneqq\\{p_{1},p_{2}\\}$ is a
trap of $\mathcal{N}_{T\setminus\\{t_{2},t_{4}\\}}$ (but not of
$\mathcal{N}_{T\setminus\\{t_{4}\\}}$). Since $\bm{m}_{\text{tgt}}(R)=0$, it
is impossible to reach $\bm{m}_{\text{tgt}}$ using transitions of
$\mathcal{N}_{T\setminus\\{t_{2},t_{4}\\}}$ that produce in $R$, i.e.
transitions of ${\rm Phys.~{}Rev.~{}E}{R}=\\{t_{1},t_{3}\\}$.

By the claims, $\bm{m}_{\text{tgt}}$ is reachable from $\bm{m}_{\text{src}}$
in $\mathcal{N}$ iff it is reachable from $\bm{m}_{\text{src}}$ in
$\mathcal{N}_{\emptyset}$. But this can only happen if
$\bm{m}_{\text{src}}=\bm{m}_{\text{tgt}}$, which is not the case.

In the next section, we transform this collection of witnesses of
unreachability into one single separator that can be used as certificate.

##  4\. Separators as certificates

Let $\mathcal{N}=(P,T,F)$ be a Petri net and let
$\bm{m}_{\text{src}},\bm{m}_{\text{tgt}}\in\mathbb{R}_{+}^{P}$ be markings of
$\mathcal{N}$. From [BFHH17], one can easily show that if
$\bm{m}_{\text{src}}\not\xrightarrow{}^{*}\bm{m}_{\text{tgt}}$, then there is
a separator for $(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})$. Indeed, [BFHH17,
Prop. 3.2] shows that there exists an existential formula $\psi$ of linear
arithmetic such that $\bm{m}\xrightarrow{}^{*}\bm{m}^{\prime}$ iff
$(\bm{m},\bm{m}^{\prime})\in\llbracket\psi\rrbracket$. Thus, the formula
$\varphi(\bm{m})\coloneqq\psi(\bm{m}_{\text{src}},\bm{m})$ is a separator.

However, $\varphi$ is not adequate as a _certificate_ of unreachability.
Indeed, checking a certificate for
$\bm{m}_{\text{src}}\not\xrightarrow{}^{*}\bm{m}_{\text{tgt}}$ should have
smaller complexity than deciding whether
$\bm{m}_{\text{src}}\xrightarrow{}^{*}\bm{m}_{\text{tgt}}$. This is not the
case for existential linear formulas, because
$\bm{m}_{\text{src}}\xrightarrow{}^{*}\bm{m}_{\text{tgt}}$ can be decided in
polynomial time, but checking that an existential linear formula is a
separator is coNP-hard.

######  Proposition 9.

The problem of determining whether an existential linear formula $\varphi$ is
a separator for $(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})$ is coNP-hard, even
if $\varphi$ is a quantifier-free formula in DNF and homogeneous (i.e., each
atomic proposition $\bm{a}\bm{x}\sim b$ is such that $b=0$.)

######  Proof 4.1.

We give a reduction from the problem of determining whether a DNF boolean
formula $\psi(x_{1},\ldots,x_{m})$ is a tautology. Since $\psi$ is in DNF, we
can test whether it is satisfiable in polynomial time. Obviously, if it is
not, then it is not a tautology. Thus, we consider the case where $\psi$ is
satisfiable. We define $\psi^{\prime}$ as $\psi$ but where literals are
modified as follows: $x_{i}$ becomes $\bm{m}(x_{i})>0$, and $\neg x_{i}$
becomes $\bm{m}(x_{i})\leq 0$. We construct a Petri net $\mathcal{N}=(P,T,F)$,
where $P=\\{x_{1},\ldots,x_{m},p,q\\}$, $T=\\{t\\}$, and $t$ produces a token
in $p$. Note that all places but $p$ are disconnected. Let
$\bm{m}_{\text{tgt}}\coloneqq\bm{0}$ and $\bm{m}_{\text{src}}$ be such that
$\bm{m}_{\text{src}}(p)=\bm{m}_{\text{src}}(q)=1$ and
$(\bm{m}_{\text{src}}(x_{1}),\ldots,\bm{m}_{\text{src}}(x_{n}))$ encodes an
(arbitrary) assignment that satisfies $\psi$. We claim that the following
formula $\varphi$ is a separator for
$(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})$ iff $\psi$ is a tautology:

$\varphi(\bm{m})\coloneqq(\bm{m}(p)\leq
0\land\bm{m}(q)>0)\lor(\bm{m}(p)>0\land\bm{m}(q)>0\land\psi^{\prime}(\bm{m})).$

As $\bm{m}_{\text{src}}\in\llbracket\varphi\rrbracket$ and
$\bm{m}_{\text{tgt}}\notin\llbracket\varphi\rrbracket$, it suffices to show
that $\varphi$ is forward invariant iff $\psi$ is a tautology

$\Rightarrow$) Let $(y_{1},\ldots,y_{m})\in\\{0,1\\}^{n}$. We show that
$\psi(y_{1},\ldots,y_{m})$ holds. Let $\bm{m}$ be such that $\bm{m}(p)=0$,
$\bm{m}(q)=1$ and $\bm{m}(x_{i})=y_{i}$ for every $i\in[1..m]$. We have
$\bm{m}\in\llbracket\varphi\rrbracket$ since the first disjunct is satisfied.
We can fire $t$ in $\bm{m}$ which leads to a marking $\bm{m}^{\prime}$ where
$\bm{m}^{\prime}(p)>0$, $\bm{m}^{\prime}(q)=1$ and
$\bm{m}^{\prime}(x_{i})=y_{i}$ for every $i\in[1..m]$. Since $\varphi$ is
forward invariant by assumption, we have
$\bm{m}^{\prime}\in\llbracket\varphi\rrbracket$. Since $\bm{m}^{\prime}(p)>0$
and $\bm{m}^{\prime}(q)>0$, this means that the second disjunct is satisfied.
In particular, this means that $\psi^{\prime}(\bm{m}^{\prime})$ holds, and
hence that $\psi(y_{1},\ldots,y_{m})$ holds.

$\Leftarrow$) Let $\bm{m}\in\llbracket\varphi\rrbracket$ and
$\bm{m}\xrightarrow{\alpha t}\bm{m}^{\prime}$. We have $\bm{m}(q)>0$. By
definition of $t$, we have $\bm{m}^{\prime}(p)>0$, and $\bm{m}^{\prime}$ equal
to $\bm{m}$ on all other places. Since $\psi$ is a tautology,
$\psi^{\prime}(\bm{m})$ holds. Thus,
$\bm{m}^{\prime}\in\llbracket\varphi\rrbracket$ holds as the second disjunct
is satisfied.

######  Remark 10.

The problem of determining whether a quantifier-free linear formula $\varphi$
is a separator for $(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})$ is in coNP.
Indeed, we can specify that a formula $\varphi$ separates
$(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})$ as follows:

$\varphi(\bm{m}_{\text{src}})\land\neg\varphi(\bm{m}_{\text{tgt}})\land\forall\bm{m}\geq\bm{0}\
\forall\alpha>0\bigwedge_{t\in
T}[\varphi(\bm{m})\land\bm{m}\geq\alpha\Delta_{t}^{-})\rightarrow\varphi(\bm{m}+\alpha\Delta_{t})].$

Membership follows since the universal fragment of linear arithmetic is in
coNP [Son85].

In the rest of the section, we introduce locally closed bi-separators, and
then, in Sections 5 and 6, we respectively prove that they satisfy the
following:

  * •

If $\bm{m}_{\text{src}}\not\xrightarrow{}^{*}\bm{m}_{\text{tgt}}$, then some
locally closed bi-separator for $(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})$
can be computed in polynomial time by solving at most $\mathcal{O}(|T|)$
linear programs;

  * •

Deciding whether a formula is a locally closed bi-separator is in NC.

###  4.1. Locally closed bi-separators

The most difficult part of checking that a formula $\varphi$ is a bi-separator
consists of checking that it is forward and backward invariant. Let us focus
on forward invariance, backward invariance being symmetric.

Recall the definition: for all markings
$\bm{m},\bm{m^{\prime}},\bm{m^{\prime\prime}}$ and every transition $t$: if
$(\bm{m},\bm{m}^{\prime})\in\llbracket\varphi\rrbracket$ and
$\bm{m}^{\prime}\xrightarrow{\alpha t}\bm{m}^{\prime\prime}$ then
$(\bm{m},\bm{m}^{\prime\prime})\in\llbracket\varphi\rrbracket$. Assume now
that $\varphi$ is in DNF, i.e., a disjunction of clauses
$\varphi=\varphi_{1}\lor\cdots\lor\varphi_{n}$. The forward invariance check
can be decomposed into $n$ smaller checks, one for each $i\in[1..n]$, of the
form: if $(\bm{m},\bm{m}^{\prime})\in\llbracket\varphi_{i}\rrbracket$, then
$(\bm{m},\bm{m}^{\prime\prime})\in\llbracket\varphi\rrbracket$. However, in
general the check _cannot_ be decomposed into _local_ checks of the form:
there exists $j\in[1..m]$ such that
$(\bm{m},\bm{m}^{\prime})\in\llbracket\varphi_{i}\rrbracket$ implies
$(\bm{m},\bm{m}^{\prime\prime})\in\llbracket\varphi_{j}\rrbracket$. Indeed,
while this property is sufficient for forward invariance, it is not necessary.
Intuitively, locally closed bi-separators are separators where invariance can
be established by local checks.

For the formal definition, we need to introduce some notations. Given a
transition $t$ and atomic propositions $\psi,\psi^{\prime}$, we say that
$\psi$ _$t$ -implies_ $\psi^{\prime}$, written
$\psi\leadsto_{t}\psi^{\prime}$, if
$(\bm{m},\bm{m}^{\prime})\in\llbracket\psi\rrbracket$ and
$\bm{m}^{\prime}\xrightarrow{\alpha t}\bm{m}^{\prime\prime}$ implies
$(\bm{m},\bm{m}^{\prime\prime})\in\llbracket\psi^{\prime}\rrbracket$. We
further say that a clause $\psi=\psi_{1}\land\cdots\land\psi_{m}$ _$t$
-implies_ a clause
$\psi^{\prime}=\psi_{1}^{\prime}\land\cdots\land\psi_{n}^{\prime}$, written
$\psi\leadsto_{t}\psi^{\prime}$, if for every $j\in[1..n]$, there exists
$i\in[1..m]$ such that $\psi_{i}\leadsto_{t}\psi_{j}^{\prime}$.

A linear formula $\varphi$ is _locally closed_ w.r.t. $\mathcal{N}=(P,T,F)$
if:

  * •

$\varphi=\varphi_{1}\lor\cdots\lor\varphi_{n}$ is quantifier-free, in DNF and
homogeneous,

  * •

for every $t\in T$ and every $i\in[1..n]$, there exists $j\in[1..n]$ s.t.
$\varphi_{i}\leadsto_{t}\varphi_{j}$,

  * •

for every $t\in T^{\mathsf{T}}$ and every $i\in[1..n]$, there exists
$j\in[1..n]$ s.t.
$\varphi_{i}^{\mathsf{T}}\leadsto_{t}\varphi_{j}^{\mathsf{T}}$.

Note that the definition is semantic. We make the straightforward but crucial
observation that:

######  Proposition 11.

Locally closed formulas are bi-invariant.

######  Proof 4.2.

Let $\varphi=\varphi_{1}\lor\cdots\lor\varphi_{n}$ be a locally closed
formula. We only consider the forward case; the other case is symmetric. Let
$(\bm{m},\bm{m}^{\prime})\in\llbracket\varphi\rrbracket$ and
$\bm{m}^{\prime}\xrightarrow{\alpha t}\bm{m}^{\prime\prime}$. Let $i\in[1..n]$
be such that $(\bm{m},\bm{m}^{\prime})\in\llbracket\varphi_{i}\rrbracket$.
Since $\varphi$ is locally closed, there exists $j\in[1..n]$ such that
$\varphi_{i}\leadsto_{t}\varphi_{j}$. For every atomic proposition
$\psi^{\prime}$ of $\varphi_{j}$, there exists an atomic proposition $\psi$ of
$\varphi_{i}$ such that $\psi\leadsto_{t}\psi^{\prime}$. Since each atomic
proposition of $\varphi_{i}$ is satisfied by $(\bm{m},\bm{m}^{\prime})$, we
obtain $(\bm{m},\bm{m}^{\prime\prime})\in\llbracket\varphi_{j}\rrbracket$.

Proposition 11 justifies the following definition:

A _locally closed bi-separator_ for
$(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})$ is a locally closed formula
$\varphi$ s.t.
$(\bm{m}_{\text{src}},\bm{m}_{\text{src}})\in\llbracket\varphi\rrbracket$,
$(\bm{m}_{\text{tgt}},\bm{m}_{\text{tgt}})\in\llbracket\varphi\rrbracket$ and
$(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})\notin\llbracket\varphi\rrbracket$.

Indeed, by Proposition 11, a locally closed bi-separator is a bi-separator, as
the bi-invariance condition of Definition 2.1 follows from local closedness.

##  5\. Constructing locally closed bi-separators

In this section, we prove that unreachability can always be witnessed by
locally closed bi-separators of polynomial size and computable in polynomial
time. The proof uses the results of Section 3.

######  Theorem 12.

If $\bm{m}_{\text{src}}\not\xrightarrow{}^{U^{*}}\bm{m}_{\text{tgt}}$, then
there is a locally closed bi-separator $\varphi$ for
$(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})$ w.r.t. $\mathcal{N}_{U}$. Further,
$\varphi=\bigvee_{1\leq i\leq n}\varphi_{i}$, where $n\leq 2|U|+1$ and each
$\varphi_{i}$ contains at most $2|U|+1$ atomic propositions. Moreover,
$\varphi$ is computable in polynomial time.

######  Proof 5.1.

We proceed by induction on $|U|$. First consider $U=\emptyset$. There must
exist $p\in P$ such that $\bm{m}_{\text{src}}(p)\neq\bm{m}_{\text{tgt}}(p)$.
Take
$\varphi(\bm{m},\bm{m}^{\prime})\coloneqq\bm{e}_{p}\bm{m}\leq\bm{e}_{p}\bm{m}^{\prime}$
or $-\bm{e}_{p}\bm{m}\leq-\bm{e}_{p}\bm{m}^{\prime}$, depending on whether
$\bm{m}_{\text{src}}(p)>\bm{m}_{\text{tgt}}(p)$ or
$\bm{m}_{\text{src}}(p)<\bm{m}_{\text{tgt}}(p)$.

Now, assume that $U\neq\emptyset$. We make a case distinction on whether the
system

$\exists\bm{x}\in\mathbb{R}_{+}^{T}:\bm{m}_{\text{src}}+\mathbf{F}\bm{x}=\bm{m}_{\text{tgt}}\land\mathrm{supp}(\bm{x})\subseteq
U\ .$

has a solution. Suppose first that it has no solution. By Proposition 7,
taking $S=\emptyset$ and $S^{\prime}=U$, there is a linear exclusion function
for $(\emptyset,U)$, i.e. a linear function $f$ satisfying (1)
$f(\bm{m}_{\text{src}})>f(\bm{m}_{\text{tgt}})$, and (2)
$\bm{m}\xrightarrow{u}\bm{m}^{\prime}$ implies $f(\bm{m})\leq
f(\bm{m}^{\prime})$ for all $u\in U$. (The first item holds due to Item 2 of
Definition 3.2 and $S=\emptyset$.) So we can take
$\varphi(\bm{m},\bm{m}^{\prime})\coloneqq(f(\bm{m})\leq f(\bm{m}^{\prime}))$.

Suppose now that the system has a solution $\bm{x}\in\mathbb{R}_{+}^{U}$. By
convexity, we can suppose that $\mathrm{supp}(\bm{x})\subseteq U$ is maximal.
Indeed, if $\bm{x}^{\prime}$ and $\bm{x}^{\prime\prime}$ are solutions, then
$(1/2)\bm{x}^{\prime}+(1/2)\bm{x}^{\prime\prime}$ is a solution with support
$\mathrm{supp}(\bm{x}^{\prime})\cup\mathrm{supp}(\bm{x}^{\prime\prime})$. Let
$U^{\prime}\coloneqq\mathrm{supp}(\bm{x})$. For every $t\in U\setminus
U^{\prime}$, consider the system of Proposition 7 with $S=\\{t\\}$ and
$S^{\prime}=U$. By maximality of $U^{\prime}\subseteq U$, none of these
systems has a solution. Consequently, for each $t\in U\setminus U^{\prime}$,
Proposition 7 yields a linear exclusion function for $(\\{t\\},U)$, i.e. a
linear function $f_{t}$ that satisfies:

  1. (3)

$f_{t}(\bm{m}_{\text{src}})\geq f_{t}(\bm{m}_{\text{tgt}})$,

  2. (4)

$\bm{m}\xrightarrow{u}\bm{m}^{\prime}$ implies $f_{t}(\bm{m})\leq
f_{t}(\bm{m}^{\prime})$ for all $u\in U$,

  3. (5)

either $f_{t}(\bm{m}_{\text{src}})>f_{t}(\bm{m}_{\text{tgt}})$, or
$\bm{m}\xrightarrow{t}\bm{m}^{\prime}$ implies
$f_{t}(\bm{m})<f_{t}(\bm{m}^{\prime})$.

If $f_{t}(\bm{m}_{\text{src}})>f_{t}(\bm{m}_{\text{tgt}})$ holds for some
$t\in U\setminus U^{\prime}$, then we are done by taking
$\varphi(\bm{m},\bm{m}^{\prime})\coloneqq(f_{t}(\bm{m})\leq
f_{t}(\bm{m}^{\prime}))$ as Item 4 ensures that $\varphi\leadsto_{u}\varphi$
for every $u\in U$. So assume it does not hold for any $t\in U\setminus
U^{\prime}$, i.e. assume that
$f_{t}(\bm{m}_{\text{src}})=f_{t}(\bm{m}_{\text{tgt}})$ holds, and the second
disjunct of Item 5 holds for all $t\in U\setminus U^{\prime}$. This is the
most involved case. Let

$\varphi_{\text{inv}}(\bm{m},\bm{m}^{\prime})\coloneqq\bigwedge_{\mathclap{t\in
U\setminus U^{\prime}}}(f_{t}(\bm{m})\leq f_{t}(\bm{m}^{\prime}))\ \text{ and
}\
\varphi_{t}(\bm{m},\bm{m^{\prime}})\coloneqq(f_{t}(\bm{m})<f_{t}(\bm{m}^{\prime})).$

Let $Q,R\subseteq P$ be respectively the maximal siphon and trap of
$\mathcal{N}_{U^{\prime}}$ such that $\bm{m}_{\text{src}}(Q)=0$ and
$\bm{m}_{\text{tgt}}(R)=0$ (well-defined by closure under union). Let
$U^{\prime\prime}\coloneqq U^{\prime}\setminus({{Q}^{\bullet}}\cup{\rm
Phys.~{}Rev.~{}E}{R})$. By Theorem 3 and Proposition 4,
${{Q}^{\bullet}}\cup{\rm Phys.~{}Rev.~{}E}{R}\neq\emptyset$. Thus,
$U^{\prime\prime}$ is a strict subset of $U^{\prime}$, and, by induction
hypothesis, there is a locally closed bi-separator w.r.t.
$\mathcal{N}_{U^{\prime\prime}}$ of the form $\psi=\bigvee_{1\leq i\leq
m}\psi_{i}$ that satisfies the claim for set $U^{\prime\prime}$. Let

$\varphi(\bm{m},\bm{m}^{\prime})\coloneqq\bigvee_{\mathclap{t\in U\setminus
U^{\prime}}}\varphi_{t}(\bm{m},\bm{m}^{\prime})\lor[\varphi_{\text{inv}}(\bm{m},\bm{m}^{\prime})\land\bm{m}(Q)+\bm{m}^{\prime}(R)>0]\lor{}\\\\[-12.0pt]
\bigvee_{\mathclap{1\leq i\leq
m}}[\varphi_{\text{inv}}(\bm{m},\bm{m}^{\prime})\land\bm{m}(R)+\bm{m}^{\prime}(Q)\leq
0\land\psi_{i}(\bm{m},\bm{m}^{\prime})].$

As
$(\bm{m}_{\text{src}},\bm{m}_{\text{src}})\in\llbracket\varphi_{\text{inv}}\rrbracket$
and $(\bm{m}_{\text{src}},\bm{m}_{\text{src}})\in\llbracket\psi\rrbracket$, we
have
$(\bm{m}_{\text{src}},\bm{m}_{\text{src}})\in\llbracket\varphi\rrbracket$.
Similarly,
$(\bm{m}_{\text{tgt}},\bm{m}_{\text{tgt}})\in\llbracket\varphi\rrbracket$. By
Item 3,
$(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})\notin\llbracket\bigvee_{t\in
U\setminus U^{\prime}}\varphi_{t}(\bm{m},\bm{m}^{\prime})\rrbracket$. Further,
$\bm{m}_{\text{src}}(Q)+\bm{m}_{\text{tgt}}(R)=0$ and
$(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})\notin\llbracket\psi\rrbracket$. So,
$(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})\notin\llbracket\varphi\rrbracket$.

The number of disjuncts of $\varphi$ is $|U\setminus U^{\prime}|+1+m$ and
hence at most

$\displaystyle|U\setminus U^{\prime}|+1+2|U^{\prime\prime}|+1$
$\displaystyle\leq(|U|-|U^{\prime\prime}|)+1+2|U^{\prime\prime}|+1$ (since
$U\supseteq U^{\prime}\supseteq U^{\prime\prime}$)
$\displaystyle=|U|+|U^{\prime\prime}|+2$ $\displaystyle\leq|U|+(|U|-1)+2$
(since $U^{\prime\prime}\subset U$) $\displaystyle=2|U|+1.$

The same bounds holds for the number of atomic propositions per disjunct.

It remains to show that $\varphi(\bm{m},\bm{m}^{\prime})$ is locally closed
w.r.t. $\mathcal{N}_{U}$. We only consider the forward case, as the backward
case is symmetric. Let
$(\bm{m},\bm{m}^{\prime})\in\llbracket\varphi\rrbracket$ and
$\bm{m}^{\prime}\xrightarrow{u}\bm{m}^{\prime\prime}$ for some $u\in U$. By
Item 4, $\varphi_{t}\leadsto_{u}\varphi_{t}$ holds for each $\varphi_{t}$.
Indeed, $f_{t}(\bm{m})<f_{t}(\bm{m}^{\prime})$ and
$\bm{m}^{\prime}\xrightarrow{u}\bm{m}^{\prime\prime}$ imply
$f_{t}(\bm{m})<f_{t}(\bm{m}^{\prime})\leq f_{t}(\bm{m}^{\prime\prime})$, and
hence $f_{t}(\bm{m})<f_{t}(\bm{m}^{\prime\prime})$. To handle the other
clauses, we make a case distinction on $u$.

  * •

_Case $u\in U\setminus U^{\prime}$._ Atomic proposition
$\theta=(f_{u}(\bm{m})\leq f_{u}(\bm{m}^{\prime}))$ of $\varphi_{\text{inv}}$
satisfies $\theta\leadsto_{u}\varphi_{u}$. Indeed, if $f_{u}(\bm{m})\leq
f_{u}(\bm{m}^{\prime})$ and
$\bm{m}^{\prime}\xrightarrow{u}\bm{m}^{\prime\prime}$, then we have
$f_{u}(\bm{m})<f_{u}(\bm{m}^{\prime})$ by Item 5.

  * •

_Case $u\in U^{\prime}$._ By Item 4, each atomic proposition $\theta$ of
$\varphi_{\text{inv}}$ satisfies $\theta\leadsto_{u}\theta$.

    * –

_Case $u\in{\rm Phys.~{}Rev.~{}E}{R}$._ We have
$\theta^{\prime}\leadsto_{u}(\bm{m}(Q)+\bm{m}^{\prime}(R)>0)$ for any atomic
proposition $\theta^{\prime}$, since
$\bm{m}^{\prime}\xrightarrow{u}\bm{m}^{\prime\prime}$ implies
$\bm{m}^{\prime\prime}(R)>0$ (regardless of $\theta^{\prime}$).

    * –

_Case $u\in{{Q}^{\bullet}}$._ If $\bm{m}^{\prime}(Q)\leq 0$, then $u$ is
disabled in $\bm{m}^{\prime}$. Thus, it only remains to handle
$\theta_{>0}\coloneqq(\bm{m}(Q)+\bm{m}^{\prime}(R)>0)$. Since $R$ is a trap of
$\mathcal{N}_{U^{\prime}}$, firing $u$ from $\bm{m}^{\prime}$ does not empty
$R$, and hence $\theta_{>0}\leadsto_{u}\theta_{>0}$.

    * –

_Case $u\in U^{\prime\prime}$._ Let $\theta_{\leq
0}\coloneqq(\bm{m}(R)+\bm{m}^{\prime}(Q)\leq 0)$ and
$\theta_{>0}\coloneqq(\bm{m}(Q)+\bm{m}^{\prime}(R)>0)$. Since $Q$ and $R$ are
respectively a siphon and trap of $\mathcal{N}_{U^{\prime}}$, we have
$\theta_{\leq 0}\leadsto_{u}\theta_{\leq 0}$ and
$\theta_{>0}\leadsto_{u}\theta_{>0}$. Moreover, by induction hypothesis, for
every $i\in[1..m]$, there exists $j\in[1..m]$ such that
$\psi_{i}\leadsto_{u}\psi_{j}$.

We conclude the proof by observing that it is constructive and can be turned
into Algorithm 1. The procedure works in polynomial time. Indeed, there are at
most $|U|$ recursive calls. Moreover, each set can be obtained in polynomial
time via either linear programming or maximal siphons/traps computations
[DE95].

Input: $\mathcal{N}=(P,T,F)$, $U\subseteq T$ and
$\bm{m}_{\text{src}},\bm{m}_{\text{tgt}}\in\mathbb{Q}_{+}^{P}$ s.t.
$\bm{m}_{\text{src}}\not\xrightarrow{}^{U^{*}}\bm{m}_{\text{tgt}}$

Output: A locally closed bi-separator w.r.t. $\mathcal{N}_{U}$

_bi-separator(_$U$_)_

if  _$U=\emptyset$_ then

pick $p\in P\text{ such that
}\bm{m}_{\text{src}}(p)\neq\bm{m}_{\text{tgt}}(p)$

return _$(\bm{a}\bm{m}\leq\bm{a}\bm{m}^{\prime})$ where
$\bm{a}\coloneqq\mathrm{sign}(\bm{m}_{\text{src}}(p)-\bm{m}_{\text{tgt}}(p))\cdot\bm{e}_{p}$_

else

$\mathmakebox[12pt][l]{\bm{b}}\coloneqq\bm{m}_{\text{tgt}}-\bm{m}_{\text{src}}$

$\mathmakebox[12pt][l]{X}\coloneqq\\{\bm{x}\in\mathbb{R}_{+}^{T}:\mathbf{F}\bm{x}=\bm{b},\mathrm{supp}(\bm{x})\subseteq
U\\}$

$\mathmakebox[12pt][l]{Y_{S}}\coloneqq\\{\bm{y}\in\mathbb{R}^{P}:\mathbf{F}^{\mathsf{T}}\bm{y}\geq_{U}\bm{0},\bm{b}^{\mathsf{T}}\bm{y}\leq
0,\bm{b}^{\mathsf{T}}\bm{y}<\sum_{s\in
S}(\mathbf{F}^{\mathsf{T}}\bm{y})_{s}\\}$

if  _$X=\emptyset$_ then

pick $\bm{y}\in Y_{\emptyset}$ and return
_$(\bm{y}^{\mathsf{T}}\bm{m}\leq\bm{y}^{\mathsf{T}}\bm{m}^{\prime})$_

else

$U^{\prime}\coloneqq\\{u\in U:\bm{x}(u)>0\text{ for some }\bm{x}\in X\\}$

for  _$t\in U\setminus U^{\prime}$_ do

pick $\bm{y}_{t}\in Y_{\\{t\\}}$;
$f_{t}(\bm{m})\coloneqq\bm{y}_{t}^{\mathsf{T}}\bm{m}$

if  _$f_{t}(\bm{m}_{\text{src}}) >f_{t}(\bm{m}_{\text{tgt}})$_ then return
_$(f_{t}(\bm{m}) <f_{t}(\bm{m}^{\prime}))$_

$Q\coloneqq$ largest siphon of $\mathcal{N}_{U^{\prime}}$ such that
$\bm{m}_{\text{src}}(Q)=0$

$R\coloneqq$ largest trap of $\mathcal{N}_{U^{\prime}}$ such that
$\bm{m}_{\text{tgt}}(R)=0$

$\varphi_{\text{inv}}\coloneqq\bigwedge_{t\in U\setminus
U^{\prime}}(f_{t}(\bm{m})\leq f_{t}(\bm{m}^{\prime}))$

$\psi_{1}\lor\cdots\lor\psi_{m}\coloneqq\textnormal{{bi-
separator(}}\textnormal{\emph{$U^{\prime}\setminus({{Q}^{\bullet}}\cup{\rm
Phys.~{}Rev.~{}E}{R})$}}\textnormal{{)}}$

return __ $\bigvee_{t\in U\setminus
U^{\prime}}\varphi_{t}(\bm{m},\bm{m}^{\prime})\lor[\varphi_{\text{inv}}(\bm{m},\bm{m}^{\prime})\land\bm{m}(Q)+\bm{m}^{\prime}(R)>0]\lor{}$

$\bigvee_{1\leq i\leq
m}[\varphi_{\text{inv}}(\bm{m},\bm{m}^{\prime})\land\bm{m}(R)+\bm{m}^{\prime}(Q)\leq
0\land\psi_{i}(\bm{m},\bm{m}^{\prime})]$

Algorithm 1 Construction of a locally closed bi-sep. for
$(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})$.

Let us apply the construction of Theorem 12 to the Petri net and the markings
of Example 3.2: $\bm{m}_{\text{src}}=\\{p_{1}\mapsto 2,p_{2}\mapsto
0,p_{3}\mapsto 0,p_{4}\mapsto 0\\}$ and
$\bm{m}_{\text{tgt}}\coloneqq\\{p_{1}\mapsto 0,p_{2}\mapsto 0,p_{3}\mapsto
1,p_{4}\mapsto 0\\}$. The locally closed bi-separator is the formula $\varphi$
below, where the colored arrows represent the relations
$\leadsto_{t_{1}},\ldots,\leadsto_{t_{4}}$:

As an example, consider transition $t_{4}$ and these atomic propositions
occurring within $\varphi$:

$\displaystyle\theta(\bm{m},\bm{m}^{\prime})$
$\displaystyle\coloneqq\bm{m}(p_{4})\leq\bm{m}^{\prime}(p_{4}),$
$\displaystyle\theta^{\prime}(\bm{m},\bm{m}^{\prime})$
$\displaystyle\coloneqq\bm{m}(p_{4})<\bm{m}^{\prime}(p_{4}).$

Given $(\bm{m},\bm{m}^{\prime})\in\llbracket\theta\rrbracket$ and
$\bm{m}^{\prime}\xrightarrow{\alpha t_{4}}\bm{m}^{\prime\prime}$, we must have
$\bm{m}^{\prime}(p_{4})<\bm{m}^{\prime\prime}(p_{4})$ since $t_{4}$ produces
in place $p_{4}$, and hence
$(\bm{m},\bm{m}^{\prime\prime})\in\llbracket\theta^{\prime}\rrbracket$. Thus,
by definition of $t_{4}$-implication, we have
$\theta\leadsto_{t_{4}}\theta^{\prime}$. This explains why the first clause of
$\varphi$ is $t_{4}$-implied by each clause of $\varphi$. Similar reasoning
yields the other $t_{i}$-implications, which shows that $\varphi$ is bi-
invariant.

Recall that since $\varphi$ is a locally closed bi-separator, taking
$\psi(\bm{m})\coloneqq\varphi(\bm{m}_{\text{src}},\bm{m})$ yields a forward
separator. Since
$\bm{m}_{\text{src}}(p_{2})=\bm{m}_{\text{src}}(p_{3})=\bm{m}_{\text{src}}(p_{4})=0$,
several atomic propositions trivially hold. After making these
simplifications, we obtain

$\displaystyle\psi(\bm{m})$ $\displaystyle\equiv\ $
$\displaystyle\bm{m}(p_{1})+\bm{m}(p_{2})>0\lor\bm{m}(p_{4})>0.$

Similarly, we obtain this backward separator
$\psi^{\prime}(\bm{m})\coloneqq\varphi(\bm{m},\bm{m}_{\text{tgt}})$:

$\displaystyle\psi^{\prime}(\bm{m})$ $\displaystyle\equiv\ $
$\displaystyle\bm{m}(p_{1})+\bm{m}(p_{2})=0\land\bm{m}(p_{3})\geq
1\land\bm{m}(p_{4})=0.$

The backward separator $\psi^{\prime}$ provides a much simpler proof of
$\bm{m}_{\text{src}}\not\xrightarrow{*}\bm{m}_{\text{tgt}}$ than the one of
Example 3.2. The proof goes as follows: $\psi^{\prime}$ is trivially backward
invariant, because markings that only mark $p_{3}$ do not backward-enable any
transition. In particular, since $\bm{m}_{\text{tgt}}$ only marks $p_{3}$, it
can only be reached from $\bm{m}_{\text{tgt}}$.

##  6\. Checking locally closed bi-separators is in NC

We show that the problem of deciding whether a given linear formula is a
locally closed bi-separator is in NC. To do so, we provide a characterization
of $\psi\leadsto_{t}\psi^{\prime}$ for homogeneous atomic propositions $\psi$
and $\psi^{\prime}$. We only focus on forward firability, as backward
firability can be expressed as forward firability in the transpose Petri net.
Recall that $\psi\leadsto_{t}\psi^{\prime}$ holds iff the following holds:

$\displaystyle(\bm{m},\bm{m}^{\prime})\in\llbracket\psi\rrbracket\text{ and
}\bm{m}^{\prime}\xrightarrow{\alpha t}\bm{m}^{\prime\prime}\text{ imply
}(\bm{m},\bm{m}^{\prime\prime})\in\llbracket\psi^{\prime}\rrbracket.$ (*)

Property (* ‣ 6) can be rephrased as:

$(\bm{m},\bm{m}^{\prime})\in\llbracket\psi\rrbracket\text{ and
}\bm{m}^{\prime}\geq\alpha\cdot\Delta_{t}^{-}\text{ imply
}(\bm{m},\bm{m}^{\prime}+\alpha\cdot\Delta_{t})\in\llbracket\psi^{\prime}\rrbracket.$

As we will see towards the end of the section, due to homogeneity of $\psi$
and $\psi^{\prime}$, it actually suffices to consider the case where
$\alpha=1$, which yields this reformulation:

$\underbrace{\\{(\bm{m},\bm{m}^{\prime})\in\llbracket\psi\rrbracket:\bm{m}^{\prime}\geq\Delta_{t}^{-}\\}}_{X}\subseteq\underbrace{\\{(\bm{m},\bm{m}^{\prime}):(\bm{m},\bm{m}^{\prime}+\Delta_{t})\in\llbracket\psi^{\prime}\rrbracket\\}}_{Y}.$

Therefore, testing $\psi\leadsto_{t}\psi^{\prime}$ amounts to the inclusion
check $X\subseteq Y$. Of course, if $X=\emptyset$, then this is trivial.
Hence, we will suppose that $X\neq\emptyset$, assuming for now that it can
somehow be tested efficiently. In the forthcoming Propositions 13 and 6.1, we
will provide necessary and sufficient conditions for $X\subseteq Y$ to hold.
In Proposition 14, we will show that these conditions are testable in NC.
Then, in Proposition 6.3, we will explain how to check whether
$X\neq\emptyset$ actually holds.

For $X\subseteq Y$, we can characterize the case of atomic propositions $\psi$
that use “$\leq$” (rather than “$<$”):

######  Proposition 13.

Let $\bm{a},\bm{a}^{\prime},\bm{l}\in\mathbb{R}^{n}$ and
$b^{\prime}\in\mathbb{R}$. Let
$X\coloneqq\\{\bm{x}\in\mathbb{R}^{n}:\bm{a}\bm{x}\leq
0\land\bm{x}\geq\bm{l}\\}$ and
$Y\coloneqq\\{\bm{x}\in\mathbb{R}^{n}:\bm{a}^{\prime}\bm{x}\leq b^{\prime}\\}$
be such that $X\neq\emptyset$. It is the case that $X\subseteq Y$ iff there
exists $\lambda\geq 0$ such that $\lambda\bm{a}\geq\bm{a}^{\prime}$ and
$-b^{\prime}\leq(\lambda\bm{a}-\bm{a}^{\prime})\bm{l}$.

######  Proof 6.1.

The _conical hull_ of a finite set $V$ is defined as

$\mathrm{conic}(V)\coloneqq\left\\{\sum_{\bm{v}\in
V}\lambda_{\bm{v}}\bm{v}:\lambda_{\bm{v}}\in\mathbb{R}_{+}\right\\}.$

We first state a generalization of Farkas’ lemma sometimes known as Haar’s
lemma (e.g. see [Sch86, p. 216]):

Let $\mathbf{A}\in\mathbb{R}^{m\times n}$, $\bm{b}\in\mathbb{R}^{m}$,
$\bm{a}^{\prime}\in\mathbb{R}^{n}$ and $b^{\prime}\in\mathbb{R}$ be such that
$\llbracket\mathbf{A}\bm{x}\leq\bm{b}\rrbracket\neq\emptyset$. It is the case
that
$\llbracket\mathbf{A}\bm{x}\leq\bm{b}\rrbracket\subseteq\llbracket\bm{a}^{\prime}\bm{x}\leq
b\rrbracket$ iff
$(\bm{a}^{\prime},b^{\prime})\in\mathrm{conic}(\\{(\bm{0},1)\\}\cup\\{(\mathbf{A}_{i},\bm{b}_{i}):i\in[1..m]\\})$.
---

We now prove the proposition. Let

$\mathbf{A}\coloneqq\begin{bmatrix}\bm{a}\\\ -\mathbf{I}\end{bmatrix}\text{
and }\bm{b}\coloneqq\begin{pmatrix}0\\\ -\bm{l}\end{pmatrix}.$

Note that $X=\llbracket\mathbf{A}\bm{x}\leq\bm{b}\rrbracket$. So, by Haar’s
lemma, we have $X\subseteq Y$ iff
$(\bm{a}^{\prime},b^{\prime})\in\mathrm{conic}(\\{(\bm{0},1)\\}\cup\\{(\mathbf{A}_{i},\bm{b}_{i}):i\in[1..m]\\})$.
Consequently, we have:

$\displaystyle X\subseteq Y$
$\displaystyle\iff\exists\lambda,\lambda_{1},\ldots,\lambda_{n}\geq
0:\bm{a}^{\prime}=\lambda\bm{a}-\sum_{i=1}^{n}\lambda_{i}\bm{e}_{i}\text{ and
}b^{\prime}\geq-\sum_{i=1}^{n}\lambda_{i}\bm{l}_{i}$
$\displaystyle\iff\exists\lambda\geq 0:\lambda\bm{a}\geq\bm{a}^{\prime}\text{
and }-b^{\prime}\leq(\lambda\bm{a}-\bm{a}^{\prime})\bm{l}.$

We now give the conditions for all four combinations of “$\leq$” and “$<$”:

proppropinclatomic Let $\bm{a},\bm{a}^{\prime}\in\mathbb{R}^{n}$,
$b^{\prime}\in\mathbb{R}$, $\bm{l}\geq\bm{0}$ and
${\sim},{\sim^{\prime}}\in\\{\leq,<\\}$. Let
$X_{\sim}\coloneqq\\{\bm{x}\geq\bm{l}:\bm{a}\bm{x}\sim\bm{0}\\}$ and
$Y_{\sim^{\prime}}\coloneqq\\{\bm{x}\in\mathbb{R}^{n}:\bm{a}^{\prime}\bm{x}\sim^{\prime}b^{\prime}\\}$
be such that $X_{\sim}\neq\emptyset$. It holds that $X_{\sim}\subseteq
Y_{\sim^{\prime}}$ iff there exists $\lambda\geq 0$ s.t.
$\lambda\bm{a}\geq\bm{a}^{\prime}$ and one of the following holds:

  1. (1)

${\sim^{\prime}}={\leq}$ and
$-b^{\prime}\leq(\lambda\bm{a}-\bm{a}^{\prime})\bm{l}$;

  2. (2)

${\sim}={\leq}$, ${\sim^{\prime}}={<}$, and
$-b^{\prime}<(\lambda\bm{a}-\bm{a}^{\prime})\bm{l}$;

  3. (3)

${\sim}={<}$, ${\sim^{\prime}}={<}$, and either
$-b^{\prime}<(\lambda\bm{a}-\bm{a}^{\prime})\bm{l}$ or
$-b^{\prime}=(\lambda\bm{a}-\bm{a}^{\prime})\bm{l}\land\lambda>0$.

######  Proof 6.2.

  1. (1)

If ${\sim}={\leq}$, then it follows immediately from Proposition 13. Thus,
assume ${\sim}={<}$. We claim that $X_{<}\subseteq Y_{\leq}$ iff
$X_{\leq}\subseteq Y_{\leq}$. The validity of this claim concludes the proof
of this case as we have handled ${\sim}={\leq}$ and as $X_{\leq}\supseteq
X_{<}\neq\emptyset$.

Let us show the claim. It is clear that $X_{<}\subseteq Y_{\leq}$ is implied
by $X_{\leq}\subseteq Y_{\leq}$. So, we only have to show direction from left
to right. For the sake of contradiction, suppose that $X_{<}\subseteq
Y_{\leq}$ and $X_{\leq}\not\subseteq Y_{\leq}$. Let $X_{=}\coloneqq
X_{\leq}\setminus X_{<}$. Note that $X_{=}\neq\emptyset$. Let $\bm{x}\in
X_{<}$ and $\bm{x}^{\prime}\in X_{=}\setminus Y_{\leq}$. We have
$\bm{x},\bm{x}^{\prime}\geq\bm{l}$, $\bm{a}\bm{x}<0$,
$\bm{a}\bm{x}^{\prime}=0$, $\bm{a}^{\prime}\bm{x}=c\leq b^{\prime}$ and
$\bm{a}^{\prime}\bm{x}^{\prime}=c^{\prime}>b^{\prime}$ for some
$c,c^{\prime}\in\mathbb{R}$. In particular, $b^{\prime}\in[c,c^{\prime})$. Let
$\epsilon\in(0,1]$ be such that $b^{\prime}<\epsilon
c+(1-\epsilon)c^{\prime}$. Let
$\bm{x}^{\prime\prime}\coloneqq\epsilon\bm{x}+(1-\epsilon)\bm{x}^{\prime}$.
Observe that $\bm{x}^{\prime\prime}\geq\bm{l}$. Moreover, we have:

$\displaystyle\bm{a}\bm{x}^{\prime\prime}$
$\displaystyle=\epsilon\bm{a}\bm{x}+(1-\epsilon)\bm{a}\bm{x}^{\prime}$
$\displaystyle=\epsilon\bm{a}\bm{x}$ $\displaystyle<0,$
$\displaystyle\bm{a}^{\prime}\bm{x}^{\prime\prime}$
$\displaystyle=\epsilon\bm{a}^{\prime}\bm{x}+(1-\epsilon)\bm{a}^{\prime}\bm{x}^{\prime}$
$\displaystyle=\epsilon c+(1-\epsilon)c^{\prime}$ $\displaystyle>b^{\prime}.$

Therefore, we have $\bm{x}^{\prime\prime}\in X_{<}$ and
$\bm{x}^{\prime\prime}\notin Y_{\leq}$, which is a contradiction.

  2. (2)

$\Rightarrow$) Since $X_{\leq}\subseteq Y_{<}$, the system
$\exists\bm{x}:\bm{x}\geq\bm{l}\land\bm{a}\bm{x}\leq
0\land\bm{a}^{\prime}\bm{x}\geq b^{\prime}$ has no solution. In matrix
notation, the system corresponds to $\exists\bm{x}:\mathbf{A}\bm{x}\leq\bm{c}$
where

$\mathbf{A}\coloneqq\begin{bmatrix}-\mathbf{I}\\\ \bm{a}\\\
-\bm{a}^{\prime}\end{bmatrix}\text{ and
}\bm{c}\coloneqq\begin{pmatrix}-\bm{l}\\\ 0\\\ -b^{\prime}\end{pmatrix}.$

By Farkas’ lemma (Lemma 1), $\mathbf{A}^{\mathsf{T}}\bm{y}=\bm{0}$ and
$\bm{c}^{\mathsf{T}}\bm{y}<0$ for some $\bm{y}\geq\bm{0}$. In other words,

$\exists\bm{z}\geq\bm{0},\lambda,\lambda^{\prime}\geq
0:\lambda\bm{a}-\lambda^{\prime}\bm{a}^{\prime}=\bm{z}\land-\lambda^{\prime}b^{\prime}<\bm{z}\bm{l}.$

Since $\bm{z}\geq\bm{0}$, we have
$\lambda\bm{a}\geq\lambda^{\prime}\bm{a}^{\prime}\land-\lambda^{\prime}b^{\prime}<(\lambda\bm{a}-\lambda^{\prime}\bm{a}^{\prime})\bm{l}$.
If $\lambda^{\prime}>0$, then we are done by dividing all terms by
$\lambda^{\prime}$. For the sake of contradiction, suppose that
$\lambda^{\prime}=0$. This means that $\lambda\bm{a}\geq\bm{0}$ and
$0<\lambda\bm{a}\bm{l}$. We necessarily have $\lambda>0$ and $\bm{a}\bm{l}>0$.
Let $\bm{x}\in X_{\leq}$. We have $0\geq\bm{a}\bm{x}\geq\bm{a}\bm{l}>0$, which
is a contradiction.

$\Leftarrow$) Let $\bm{x}\in X_{\leq}$. We have
$\bm{a}^{\prime}\bm{x}<b^{\prime}$ and hence $\bm{x}\in Y_{<}$ as desired,
since:

$\displaystyle-b^{\prime}$
$\displaystyle<(\lambda\bm{a}-\bm{a}^{\prime})\bm{l}$
$\displaystyle\leq(\lambda\bm{a}-\bm{a}^{\prime})\bm{x}$ (by
$(\lambda\bm{a}-\bm{a}^{\prime})\geq\bm{0}$ and $\bm{x}\geq\bm{l}\geq\bm{0}$)
$\displaystyle=\lambda\bm{a}\bm{x}-\bm{a}^{\prime}\bm{x}$
$\displaystyle\leq-\bm{a}^{\prime}\bm{x}$ $\displaystyle\text{(by $\lambda\geq
0$ and $\bm{a}\bm{x}\leq 0$)}.$

  3. (3)

$\Rightarrow$) Since $X_{<}\subseteq Y_{<}$, this system has no solution:
$\exists\bm{x}:\bm{x}\geq\bm{l}\land\bm{a}\bm{x}<0\land\bm{a}^{\prime}\bm{x}\geq
b^{\prime}$. The latter can be rephrased as $\exists\bm{x},y:y\geq
1\land\bm{x}\geq y\bm{l}\land\bm{a}\bm{x}\leq-1\land\bm{a}^{\prime}\bm{x}\geq
yb^{\prime}$. In matrix notation, this corresponds to
$\exists\bm{x}:\mathbf{A}\bm{x}\leq\bm{c}$ where

$\mathbf{A}\coloneqq\begin{bmatrix}-\mathbf{I}&\bm{l}^{\mathsf{T}}\ \\\
\bm{a}&0\\\ -\bm{a}^{\prime}&b^{\prime}\\\ \bm{0}&-1\end{bmatrix}\text{ and
}\bm{c}\coloneqq\begin{pmatrix}\bm{0}\\\ -1\\\ 0\\\ -1\\\ \end{pmatrix}.$

By Lemma 1, $\mathbf{A}^{\mathsf{T}}\bm{y}=\bm{0}$ and
$\bm{c}^{\mathsf{T}}\bm{y}<0$ for some $\bm{y}\geq\bm{0}$. In other words,

$\exists\bm{z}\geq\bm{0},\lambda,\lambda^{\prime},\lambda^{\prime\prime}\geq
0:-\bm{z}+\lambda\bm{a}-\lambda^{\prime}\bm{a}^{\prime}=\bm{0}\land\bm{z}\bm{l}+\lambda^{\prime}b^{\prime}-\lambda^{\prime\prime}=0\land-\lambda-\lambda^{\prime\prime}<0.$

Since $\bm{z}\geq\bm{0}$, $\lambda\geq 0$ and $\lambda^{\prime\prime}\geq 0$,
we have:

$\lambda\bm{a}\geq\lambda^{\prime}\bm{a}^{\prime}\land[(-\lambda^{\prime}b^{\prime}<(\lambda\bm{a}-\lambda^{\prime}\bm{a}^{\prime})\bm{l})\lor(-\lambda^{\prime}b^{\prime}=(\lambda\bm{a}-\lambda^{\prime}\bm{a}^{\prime})\bm{l}\land\lambda>0)].$

If $\lambda^{\prime}>0$, then we are done by dividing all terms by
$\lambda^{\prime}$. For the sake of contradiction, suppose that
$\lambda^{\prime}=0$. This means that $\lambda\bm{a}\geq\bm{0}$, and either
$0<\lambda\bm{a}\bm{l}$ or $0=\lambda\bm{a}\bm{\ell}\land\lambda>0$. We
necessarily have $\lambda>0$ and $\bm{a}\geq\bm{0}$. Let $\bm{x}\in X_{<}$. We
have $0>\bm{a}\bm{x}\geq\bm{a}\bm{l}\geq 0$, which is a contradiction.

$\Leftarrow$) Let $\bm{x}\in X_{<}$. If
$-b^{\prime}<(\lambda\bm{a}-\bm{a}^{\prime})\bm{l}$ holds, then we get
$\bm{x}\in Y_{<}$ as in Item 2. Otherwise, we have
$-b^{\prime}=(\lambda\bm{a}-\bm{a}^{\prime})\bm{l}$ and $\lambda>0$. Hence, we
have:

$\displaystyle-b^{\prime}$
$\displaystyle=(\lambda\bm{a}-\bm{a}^{\prime})\bm{l}$
$\displaystyle\leq(\lambda\bm{a}-\bm{a}^{\prime})\bm{x}$ (by
$(\lambda\bm{a}-\bm{a}^{\prime})\geq\bm{0}$ and $\bm{x}\geq\bm{l}\geq\bm{0}$)
$\displaystyle=\lambda\bm{a}\bm{x}-\bm{a}^{\prime}\bm{x}$
$\displaystyle<-\bm{a}^{\prime}\bm{x}$ $\displaystyle\text{(by $\lambda>0$ and
$\bm{a}\bm{x}<0$)}.$

Thus, $\bm{a}^{\prime}\bm{x}<b^{\prime}$ and hence $\bm{x}\in Y_{<}$ as
desired.

The conditions arising from Proposition 6.1 involve solving linear programs
with _one_ variable $\lambda$. It is easy to see that this problem is in NC:

######  Proposition 14.

Given $\bm{a},\bm{b}\in\mathbb{Q}^{n}$ and
$\bm{{\sim}}\in\\{{\leq},{<}\\}^{n}$, testing $\exists\lambda\geq
0:\bm{a}\lambda\bm{\sim}\bm{b}$ is in NC.

######  Proof 6.3.

Let $X_{i}\coloneqq\\{\lambda\geq
0:\bm{a}_{i}\lambda~{}\bm{{\sim}}_{i}~{}\bm{b}_{i}\\}$. Let “${}_{i}\langle$”
and “$\rangle_{i}$” denote “$[$” and “$]$” if $\bm{{\sim}}_{i}={\leq}$, and
“$($” and “$)$” otherwise. Each $X_{i}$ is an interval:

$X_{i}=\begin{cases}\emptyset&\text{if }\bm{a}_{i}=0\text{ and
}0\not\bm{\sim}_{i}\bm{b}_{i},\\\ [0,\bm{b}_{i}/\bm{a}_{i}\rangle_{i}&\text{if
}\bm{a}_{i}>0,\\\ {}_{i}\langle\bm{b}_{i}/\bm{a}_{i},+\infty)&\text{if
}\bm{a}_{i}<0\text{ and }\bm{b}_{i}\leq 0,\\\
[0,+\infty)&\text{otherwise}.\end{cases}$

We want to test whether $X_{1}\cap\cdots\cap X_{n}\neq\emptyset$. Since
arithmetic belongs to NC, it suffices to: (1) compute the left endpoint
$\ell_{i}$ and the right endpoint $r_{i}$ of each $X_{i}$ in parallel; (2)
compute $\ell\coloneqq\max(\ell_{1},\ldots,\ell_{n})$ and
$r\coloneqq\min(r_{1},\ldots,r_{n})$; and (3) accept iff $\ell<r$, or $\ell=r$
and each $X_{i}$ is closed on the left and the right.

Recall that at the beginning of the section we made the assumption that some
pair $(\bm{m},\bm{m}^{\prime})\in\llbracket\psi\rrbracket$ is such that
$\bm{m}^{\prime}$ enables a transition $t$. Checking whether this is actually
true has a cost. Fortunately, we provide a simple characterization of
enabledness which can checked in NC. Formally, we say that $\varphi$ _enables_
$t$ if there exists $(\bm{m},\bm{m}^{\prime})\in\llbracket\varphi\rrbracket$
such that $\bm{m}^{\prime}$ $\alpha$-enables $t$ for some $\alpha>0$. We have:

proppropCharacInv Let
$\varphi_{\sim}(\bm{m},\bm{m}^{\prime})\coloneqq\bm{a}\bm{m}\sim\bm{b}\bm{m}^{\prime}$
where $\bm{a},\bm{b}\in\mathbb{R}^{P}$. It is the case that

  1. (1)

$\varphi_{<}$ enables $u$ iff $\bm{a}\not\geq\bm{0}$ or
$\bm{b}\not\leq\bm{0}$, and

  2. (2)

$\varphi_{\leq}$ enables $u$ iff $\bm{b}\Delta_{u}^{-}\geq 0$ or
$(\bm{b}\Delta_{u}^{-}<0\land(\bm{a},-\bm{b})\not\geq(\bm{0},\bm{0}))$.

######  Proof 6.4.

  1. (1)

$\Rightarrow$) Since $\varphi_{<}$ enables $u$, we have
$\llbracket\varphi_{<}\rrbracket\neq\emptyset$. Let
$(\bm{m},\bm{m}^{\prime})\in\llbracket\varphi_{<}\rrbracket$. We have
$\bm{a}\bm{m}<\bm{b}\bm{m}^{\prime}$. It cannot be that $\bm{a}\geq\bm{0}$ and
$\bm{b}\leq\bm{0}$, as otherwise $\bm{a}\bm{m}\geq
0\geq\bm{b}\bm{m}^{\prime}$.

$\Leftarrow$) It suffices to give a pair
$(\bm{m},\bm{m}^{\prime})\in\llbracket\varphi_{<}\rrbracket$ such that
$\bm{m}^{\prime}\geq\Delta_{u}^{-}$. Informally, if $\bm{a}$ has a negative
value (resp. $\bm{b}$ has a positive value), then we can consider the pair
$(\bm{0},\Delta_{u}^{-})$ and “fix” the value on the left-hand-side (resp.
right-hand side) so that $\varphi_{<}$ is satisfied. More formally, if
$\bm{a}(p)<0$, then
$(k\bm{e}_{p},\Delta_{u}^{-})\in\llbracket\varphi_{<}\rrbracket$ with
$k\coloneqq(|\bm{b}\Delta_{u}^{-}|+1)/|\bm{a}(p)|$; if $\bm{b}(p)>0$, then
$(\bm{0},\Delta_{u}^{-}+k\bm{e}_{p})\in\llbracket\varphi_{<}\rrbracket$ with
$k\coloneqq(|\bm{b}\Delta_{u}^{-}|+1)/\bm{b}(p)$.

  2. (2)

$\Rightarrow$) Let
$(\bm{m},\bm{m}^{\prime})\in\llbracket\varphi_{\leq}\rrbracket$ be such that
$\bm{m}^{\prime}$ enables $u$. We have
$\bm{m}^{\prime}=\bm{x}+\alpha\Delta_{u}^{-}$ for some $\bm{x}\geq\bm{0}$ and
$\alpha>0$. Therefore,
$\bm{a}\bm{m}\leq\bm{b}\bm{x}+\alpha\bm{b}\Delta_{u}^{-}$. We assume that
$\bm{b}\Delta_{u}^{-}<0$, as we are otherwise trivially done. If
$\bm{a}\geq\bm{0}$ and $-\bm{b}\geq\bm{0}$, then we obtain a contradiction
since $\bm{a}\bm{m}\geq 0>\bm{b}\bm{x}+\alpha\bm{b}\Delta_{u}^{-}$.

$\Leftarrow$) It suffices to exhibit a pair
$(\bm{m},\bm{m}^{\prime})\in\llbracket\varphi_{\leq}\rrbracket$ such that
$\bm{m}^{\prime}\geq\Delta_{u}^{-}$. If $\bm{b}\Delta_{u}^{-}\geq 0$, then we
are done by taking $(\bm{0},\Delta_{u}^{-})$. Let us consider the second case
where $\bm{b}\Delta_{u}^{-}<0$ and $\bm{a}(p)<0\lor\bm{b}(p)>0$ for some $p\in
P$. Informally, we consider the pair $(\bm{0},\Delta_{u}^{-})$ and “fix” the
value on the left-hand-side or right-hand side depending on whether
$\bm{a}(p)<0$ or $\bm{b}(p)>0$. More formally, we are done by taking either
the pair $(k\bm{e}_{p},\Delta_{u}^{-})$ where
$k\coloneqq|\bm{b}\Delta_{u}^{-}|/|\bm{a}(p)|$, or the pair
$(\bm{0},\Delta_{u}^{-}+\ell\bm{e}_{p})$ where
$\ell\coloneqq|\bm{b}\Delta_{u}^{-}|/\bm{b}(p)$.

We can finally show that testing $\psi\leadsto_{t}\psi^{\prime}$ can be done
in NC, for atomic propositions $\psi$ and $\psi^{\prime}$. In turn, this
allows us to show that we can test in NC whether a linear formula is a locally
closed bi-separator.

######  Proposition 15.

Given a Petri net $\mathcal{N}$, a transition $t$ and homogeneous atomic
propositions $\psi$ and $\psi^{\prime}$, testing whether
$\psi\leadsto_{t}\psi^{\prime}$ can be done in NC.

######  Proof 6.5.

Recall that addition, subtraction, multiplication, division and comparison can
be done in NC. Note that, by Proposition 6.3, we can check whether $\psi$
enables $t$ in NC. If it does, then we must test whether
$(\bm{m},\bm{m}^{\prime})\in\llbracket\psi\rrbracket$ and
$\bm{m}^{\prime}\xrightarrow{\alpha t}\bm{m}^{\prime\prime}$ implies
$(\bm{m},\bm{m}^{\prime\prime})\in\llbracket\psi^{\prime}\rrbracket$. We claim
that this amounts to testing $X\subseteq Y$, where:

$\displaystyle X$
$\displaystyle\coloneqq\\{(\bm{m},\bm{m}^{\prime})\in\mathbb{R}_{+}^{P}\times\mathbb{R}_{+}^{P}:(\bm{m},\bm{m}^{\prime})\in\llbracket\psi\rrbracket\text{
and }(\bm{m},\bm{m}^{\prime})\geq(\bm{0},\Delta_{t}^{-})\\},$ $\displaystyle
Y$
$\displaystyle\coloneqq\\{(\bm{m},\bm{m}^{\prime})\in\mathbb{R}_{+}^{P}\times\mathbb{R}_{+}^{P}:(\bm{m},\bm{m}^{\prime}+\Delta_{t})\in\llbracket\psi^{\prime}\rrbracket\\}.$

Let us prove this claim.

$\Rightarrow$) Let $(\bm{m},\bm{m}^{\prime})\in X$. We have
$(\bm{m},\bm{m}^{\prime})\in\llbracket\psi\rrbracket$ and
$(\bm{m},\bm{m}^{\prime})\geq(\bm{0},\Delta_{t}^{-})$. Thus
$\bm{m}^{\prime}\xrightarrow{t}\bm{m}^{\prime}+\Delta_{t}$. By assumption,
$(\bm{m},\bm{m}^{\prime}+\Delta_{t})\in\llbracket\psi^{\prime}\rrbracket$, and
hence $(\bm{m},\bm{m}^{\prime})\in Y$.

$\Leftarrow$) Let $(\bm{m},\bm{m}^{\prime})\in\llbracket\psi\rrbracket$ and
$\bm{m}^{\prime}\xrightarrow{\alpha t}\bm{m}^{\prime\prime}$. We have
$\bm{m}^{\prime}\geq\alpha\Delta_{t}^{-}$ and
$\bm{m}^{\prime\prime}=\bm{m}^{\prime}+\alpha\Delta_{t}$. Let
$\bm{k}\coloneqq\bm{m}/\alpha$,
$\bm{k}^{\prime}\coloneqq\bm{m}^{\prime}/\alpha$ and
$\bm{k}^{\prime\prime}\coloneqq\bm{m}^{\prime\prime}/\alpha$. As $\alpha>0$
and $\psi$ is homogeneous, we have
$(\bm{k},\bm{k}^{\prime})\in\llbracket\psi\rrbracket$,
$(\bm{k},\bm{k}^{\prime})\geq(\bm{0},\Delta_{t}^{-})$ and
$\bm{k}^{\prime\prime}=\bm{k}^{\prime}+\Delta_{t}$. Thus,
$(\bm{k},\bm{k}^{\prime})\in X\subseteq Y$. By definition of $Y$, this means
that $(\bm{k},\bm{k}^{\prime\prime})\in\llbracket\psi^{\prime}\rrbracket$. By
homogeneity, we conclude that
$(\bm{m},\bm{m}^{\prime\prime})\in\llbracket\psi^{\prime}\rrbracket$.

Now that we have shown the claim, let us explain how to check whether
$X\subseteq Y$ in NC. Note that $X\neq\emptyset$ since $\psi$ enables $t$.
Thus, by Proposition 6.1, testing $X\subseteq Y$ amounts to solving a linear
program in one variable. For example, if
$\psi=(\bm{a}\cdot(\bm{m},\bm{m}^{\prime})\leq 0)$ and
$\psi^{\prime}=(\bm{a}^{\prime}\cdot(\bm{m},\bm{m}^{\prime})<0)$, then we must
check whether this system has a solution:

$\exists\lambda\geq
0:\lambda\bm{a}\geq\bm{a}^{\prime}\land\bm{a}^{\prime}\cdot(\bm{0},\Delta_{t})<(\lambda\bm{a}-\bm{a}^{\prime})\cdot(\bm{0},\Delta_{t}^{-}).$

Thus, by Proposition 14, testing $X\subseteq Y$ can be done in NC.

######  Theorem 16.

Given $\mathcal{N}=(P,T,F)$,
$\bm{m}_{\text{src}},\bm{m}_{\text{tgt}}\in\mathbb{Q}_{+}^{P}$ and a formula
$\varphi$, testing whether $\varphi$ is a locally closed bi-separator for
$(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})$ can be done in NC.

######  Proof 6.6.

Recall that $\varphi=\varphi_{1}\lor\cdots\lor\varphi_{n}$ must be in DNF with
homogeneous atomic propositions. As arithmetic belongs in NC and $\varphi$ is
in DNF, we can test whether
$(\bm{m}_{\text{src}},\bm{m}_{\text{src}})\in\llbracket\varphi\rrbracket$,
$(\bm{m}_{\text{tgt}},\bm{m}_{\text{tgt}})\in\llbracket\varphi\rrbracket$ and
$(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})\notin\llbracket\varphi\rrbracket$
in NC by evaluating $\varphi$ in parallel. We can further test whether
$\varphi$ is locally closed by checking the following (which is simply the
definition of “locally closed”):

$\left[\bigwedge_{\begin{subarray}{c}t\in T\\\
i\in[1..n]\end{subarray}}\bigvee_{j\in[1..n]}\bigwedge_{\psi\in\varphi_{i}}\bigvee_{\psi^{\prime}\in\varphi_{j}}\psi\leadsto_{t}\psi^{\prime}\right]\land\left[\bigwedge_{\begin{subarray}{c}t\in
T^{\mathsf{T}}\\\
i\in[1..n]\end{subarray}}\bigvee_{j\in[1..n]}\bigwedge_{\psi\in\varphi_{i}}\bigvee_{\psi^{\prime}\in\varphi_{j}}\psi^{\mathsf{T}}\leadsto_{t}\psi^{\prime\mathsf{T}}\right].$

By Proposition 15, each test $\psi\leadsto_{t}\psi^{\prime}$ can be carried in
NC. Therefore, we can perform all of them in parallel. Note that we do not
have to explicitly compute the transpose of transitions and formulas; we can
simply swap arguments.

######  Remark 17.

Testing whether $\varphi$ is locally closed is even simpler if the tester is
also given annotations indicating for every clause $\varphi_{i}$ and
transition $t$ which clause $\varphi_{j}$ is supposed to satisfy
$\varphi_{i}\leadsto_{t}\varphi_{j}$. This mapping is a byproduct of the
procedure to compute a locally closed bi-separator, and so comes at no cost.

##  7\. Bi-separators for set-to-set unreachability

In some applications, one does not have to prove unreachability of one
marking, but rather of a _set_ of markings, usually defined by means of some
simple linear constraints. Thus, we now consider the more general setting of
“set-to-set reachability”, i.e. queries of the form
$\exists\bm{m}_{\text{src}}\in A,\bm{m}_{\text{tgt}}\in
B:\bm{m}_{\text{src}}\xrightarrow{}^{*}\bm{m}_{\text{tgt}}$, which we denote
by $A\xrightarrow{}^{*}B$. We focus on the case where sets $A$ and $B$ are
described by conjunctions of atomic propositions; in other words, $A$ and $B$
are convex polytopes defined as intersections of half-spaces. In particular,
this includes “coverability” queries which are important in practice, i.e.
where $A$ is a singleton and $B$ is of the form
$\\{\bm{m}:\bm{m}\geq\bm{b}\\}$.

It follows from [BH17] that testing whether $A\not\xrightarrow{}^{*}B$ can be
done in polynomial time. In this work, we have shown that, whenever $A$ and
$B$ are singleton sets, we can validate a certificate for
$A\not\xrightarrow{}^{*}B$ in NC (and so with lower complexity). In the
general case where either $A$ or $B$ is not a singleton, we could proceed
similarly by constructing a (locally closed) bi-separator, as defined
previously, but with the natural generalization that
$(\bm{m}_{\text{src}},\bm{m}_{\text{src}})\in\llbracket\varphi\rrbracket$,
$(\bm{m}_{\text{tgt}},\bm{m}_{\text{tgt}})\in\llbracket\varphi\rrbracket$ and
$(\bm{m}_{\text{src}},\bm{m}_{\text{tgt}})\notin\llbracket\varphi\rrbracket$
_for every_ $\bm{m}_{\text{src}}\in A$ and $\bm{m}_{\text{tgt}}\in B$.

Unfortunately, as we will show in Section 7.1, checking that a given linear
formula is a (locally closed) bi-separator is coNP-hard. Nonetheless, in
Section 7.2, we will show that one can construct a locally closed bi-separator
on an _altered_ Petri net with a single source and target marking.

###  7.1. Hardness of checking set-to-set bi-separators

######  Proposition 18.

The problem of determining whether a given linear formula $\varphi$ is a
locally closed bi-separator for convex polytopes $(A,B)$ is coNP-hard, even if
(1) $A$ is a singleton and $B$ is of the form $\\{\bm{m}:\bm{m}\geq\bm{b}\\}$,
or (2) vice versa.

######  Proof 7.1 (Proof of (1)).

We give a reduction from the problem of determining whether a DNF boolean
formula $\psi=\bigvee_{j\in J}\psi_{j}(x_{1},\ldots,x_{m})$ is a tautology. As
in the proof of Proposition 9, we define $\psi_{j}^{\prime}$ as $\psi_{j}$ but
where literals are modified as follows: $x_{i}$ becomes $\bm{m}(x_{i})>0$, and
$\neg x_{i}$ becomes $\bm{m}(x_{i})\leq 0$.

Let $\mathcal{N}=(P,T,F)$ be the Petri net such that
$P\coloneqq\\{x_{1},\ldots,x_{m},y\\}$, $T\coloneqq\\{t\\}$, and $t$ consumes
and produces a token in $y$. Let

$\varphi(\bm{m},\bm{m}^{\prime})\coloneqq(\bm{m}^{\prime}(y)\leq
0)\lor\bigvee_{j\in J}[\psi_{j}^{\prime}(\bm{m})\land\bm{m}(y)>0].$

Let $A\coloneqq\\{\bm{0}\\}$ and
$B\coloneqq\\{\bm{m}_{\text{tgt}}\in\mathbb{R}_{+}^{P}:\bm{m}_{\text{tgt}}(y)\geq
1\\}$.

Note that $\varphi$ is homogeneous. Moreover, transition $t$ leaves markings
unchanged, i.e. $\bm{m}^{\prime}\xrightarrow{}\bm{m}^{\prime\prime}$ implies
$\bm{m}^{\prime\prime}=\bm{m}^{\prime}$, and likewise backward. Therefore, we
trivially have $\theta\leadsto_{t}\theta$ and
$\theta^{\mathsf{T}}\leadsto_{t}\theta^{\mathsf{T}}$ for every atomic
proposition $\theta$ of $\varphi$. Further observe that
$(\bm{0},\bm{0})\in\llbracket\varphi\rrbracket$ and
$(\bm{0},\bm{m}_{\text{tgt}})\notin\llbracket\varphi\rrbracket$ for every
$\bm{m}_{\text{tgt}}\in B$.

Consequently, $\varphi$ satisfies all of the properties of a locally closed
bi-separator for $(A,B)$, except possibly the requirement that
$(\bm{m}_{\text{tgt}},\bm{m}_{\text{tgt}})\in\llbracket\varphi\rrbracket$ for
every $\bm{m}_{\text{tgt}}\in B$. The latter holds iff $\psi$ is a tautology
(since $\varphi(\bm{m}_{\text{tgt}},\bm{m}_{\text{tgt}})\equiv\bigvee_{j\in
J}\varphi_{j}^{\prime}(\bm{m}_{\text{tgt}})$). Thus, we are done.

######  Proof 7.2 (Proof of (2).).

This follows immediately from the fact that $\varphi$ is a locally closed bi-
separator for $(A,B)$ in $\mathcal{N}$ iff $\varphi^{\mathsf{T}}$ is a locally
closed bi-separator for $(B,A)$ in $\mathcal{N}^{\mathsf{T}}$.

###  7.2. Certifying set-to-set unreachability

As shown in [BH17, Lem. 3.7], given an atomic proposition
$\psi=(\bm{a}\bm{x}\sim b)$, one can construct (in logarithmic space) a Petri
net $\mathcal{N}_{\psi}$ and some $\bm{y}\in\\{0,1\\}^{5}$ such that
$\psi(\bm{x})$ holds iff $(\bm{x},\bm{y})\xrightarrow{}^{*}(\bm{0},\bm{0})$ in
$\mathcal{N}_{\psi}$. The idea—depicted in Figure 2, which is adapted from
[BH17, Fig. 1])—is simply to cancel out positive and negative coefficients of
$\psi$. It is straightforward to adapt this construction to a conjunction
$\bigwedge_{1\leq i\leq k}\psi_{k}(\bm{x})$ of atomic propositions. Indeed, it
suffices to make $k$ copies of the gadget, but where places
$\\{p_{1},\ldots,p_{n}\\}$ and transitions $\\{t_{1},\ldots,t_{n}\\}$ are
shared. In this more general setting, $t_{i}$ consumes from $p_{i}$ and
simultaneously spawns the respective coefficient to each copy.

$x_{1}$$x_{2}$$\vdots$$x_{n}$$t_{1}$$t_{2}$$t_{n}$$p_{1}$$p_{2}$$p_{n}$$q_{\text{pos}}$$q_{\text{neg}}$$q_{\geq}$$q_{>}^{\prime}$$q_{>}$$a_{1}$$a_{2}$$|a_{n}|$$c$
Figure 2. Petri net for $\psi(\bm{x})=(a_{1}\cdot x_{1}+\cdots+a_{n}\cdot
x_{n}>c)$ where $a_{1},a_{2},c>0$ and $a_{n}<0$.

In summary, the following holds:

######  Proposition 19.

Given a conjunction of $k$ atomic propositions $\varphi$, it is possible to
construct, in logarithmic space, a Petri net $\mathcal{N}_{\varphi}$ and
$\bm{y}\in\\{0,1\\}^{5k}$ such that $\varphi(\bm{x})$ holds iff
$(\bm{x},\bm{y})\xrightarrow{}^{*}(\bm{0},\bm{0})$ in $\mathcal{N}_{\varphi}$.

With the previous construction in mind, we can reformulate any set-to-set
reachability query into a standard (marking-to-marking) reachability query.

######  Proposition 20.

Given a Petri net $\mathcal{N}$ and convex polytopes $A$ and $B$ described as
conjunctions of atomic propositions, one can construct, in logarithmic space,
a Petri net $\mathcal{N}^{\prime}$ and markings $\bm{m}_{\text{src}}$ and
$\bm{m}_{\text{tgt}}$ such that $A\xrightarrow{}^{*}B$ in $\mathcal{N}$ iff
$\bm{m}_{\text{src}}\xrightarrow{}^{*}\bm{m}_{\text{tgt}}$ in
$\mathcal{N}^{\prime}$.

######  Proof 7.3.

Let $\mathcal{N}=(P,T,(\mathbf{F}_{-},\mathbf{F}_{+}))$ where
$P=\\{p_{1},\ldots,p_{n}\\}$. Let us describe
$\mathcal{N}^{\prime}=(P^{\prime},T^{\prime},\allowbreak(\mathbf{F}_{-}^{\prime},\allowbreak\mathbf{F}_{+}^{\prime}))$
with the help of Figure 3. The Petri net $\mathcal{N}^{\prime}$ extends
$\mathcal{N}$ as follows:

  * •

we add transitions $\\{t_{1},\ldots,t_{n}\\}$ whose purpose is to
nondeterministically guess an initial marking of $\mathcal{N}$ in $P$, and
make a copy in $Q\coloneqq\\{q_{1},\ldots,q_{n}\\}$;

  * •

we add a net $\mathcal{N}_{A}=(P_{A},T_{A},F_{A})$, obtained from Proposition
19, to test whether the marking in $Q$ belongs to $A$; and we add a net
$\mathcal{N}_{B}=(P_{B},T_{B},F_{B})$, obtained from Proposition 19, to test
whether the marking in $P$ belongs to $B$.

$q_{1}$$q_{2}$$\cdots$$q_{n}$$p_{1}$$p_{2}$$\cdots$$p_{n}$$\in A$?$\in
B$?$t_{1}$$t_{2}$$\vdots$$t_{n}$$\mathcal{N}$ Figure 3. Reduction from set-to-
set reachability to (marking-to-marking) reachability.

The Petri net $\mathcal{N}^{\prime}$ is _intended_ to work sequentially as
follows:

  1. (1)

guess the initial marking $\bm{m}_{\text{src}}$ of $\mathcal{N}$;

  2. (2)

test whether $\bm{m}_{\text{src}}\in A$;

  3. (3)

execute $\mathcal{N}$ on $\bm{m}_{\text{src}}$ and reach a marking
$\bm{m}_{\text{tgt}}$; and

  4. (4)

test whether $\bm{m}_{\text{tgt}}\in B$.

If $\mathcal{N}^{\prime}$ follows this order, then it is straightforward to
see that $A\xrightarrow{}^{*}B$ in $\mathcal{N}$ iff
$(\bm{0},\bm{0},\bm{y},\bm{y}^{\prime})\xrightarrow{}^{*}(\bm{0},\bm{0},\bm{0},\bm{0})$
in $\mathcal{N}^{\prime}$, where $\bm{y}$ and $\bm{y}^{\prime}$ are obtained
from Proposition 19. However, $\mathcal{N}^{\prime}$ may interleave the
different phases.333It is tempting to implement a lock, but this only works
under discrete semantics. Nonetheless, this is not problematic, as any run of
$\mathcal{N}^{\prime}$ can be reordered in such a way that all four phases are
consecutive.

More formally, let
$(\bm{0},\bm{0},\bm{y},\bm{y}^{\prime})\xrightarrow{\sigma}(\bm{0},\bm{0},\bm{0},\bm{0})$
in $\mathcal{N}^{\prime}$. Note that $\Delta_{t_{i}}^{-}=\bm{0}$ for every
$i\in[1..n]$. Thus, we can reorder $\sigma$ so that

$(\bm{0},\bm{0},\bm{y},\bm{y}^{\prime})\xrightarrow{\alpha_{1}t_{1}\cdots\alpha_{n}t_{n}}(\bm{m}_{\text{src}},\bm{m}_{\text{src}},\bm{y},\bm{y}^{\prime})\xrightarrow{\sigma^{\prime}}(\bm{0},\bm{0},\bm{0},\bm{0})\text{
in }\mathcal{N}^{\prime},$

for some $\alpha_{1},\ldots,\alpha_{n}\in\mathbb{R}_{+}$, marking
$\bm{m}_{\text{src}}$, and firing sequence $\sigma^{\prime}$ whose support
does not contain any of $t_{1},\ldots,t_{n}$.

We have $\Delta_{t}^{-}(r)=0$ for every $t\in T_{A}$ and $r\notin Q\cup
P_{A}$. Furthermore, we have $\Delta_{t}^{+}(r)=0$ for every
$t\notin\\{t_{1},\ldots,t_{n}\\}$ and $r\in Q\cup P_{A}$. Thus, we can reorder
$\sigma^{\prime}$ into $\tau\tau^{\prime}$ so that

$(\bm{m}_{\text{src}},\bm{m}_{\text{src}},\bm{y},\bm{y}^{\prime})\xrightarrow{\tau}(\bm{0},\bm{m}_{\text{src}},\bm{0},\bm{y}^{\prime})\xrightarrow{\tau^{\prime}}(\bm{0},\bm{0},\bm{0},\bm{0})\text{
in }\mathcal{N}^{\prime},$

the support of $\tau$ only contains transitions from $T_{A}$, no transition
from $T_{A}$ occurs in the support of $\tau^{\prime}$.

We have $\Delta_{t}^{+}(r)=0$ for every $t\in T_{B}$ and $r\notin P_{B}$.
Therefore, we can reorder $\tau^{\prime}$ into
$\tau^{\prime\prime}\tau^{\prime\prime\prime}$ so that

$(\bm{0},\bm{m}_{\text{src}},\bm{0},\bm{y}^{\prime})\xrightarrow{\tau^{\prime\prime}}(\bm{0},\bm{m}_{\text{tgt}},\bm{0},\bm{y}^{\prime})\xrightarrow{\tau^{\prime\prime\prime}}(\bm{0},\bm{0},\bm{0},\bm{0})\text{
in }\mathcal{N}^{\prime},$

the support of $\tau^{\prime\prime}$ only contains transitions from $T$, no
transition from $T$ occurs in the support of $\tau^{\prime\prime\prime}$, and
$\bm{m}_{\text{tgt}}\in\mathbb{R}_{+}^{P}$.

Altogether, we obtain

$(\bm{m}_{\text{src}},\bm{y})\xrightarrow{\tau}(\bm{0},\bm{0})\text{ in
}\mathcal{N}_{A},\bm{m}_{\text{src}}\xrightarrow{\tau^{\prime}}\bm{m}_{\text{tgt}}\text{
in }\mathcal{N},\text{ and
}(\bm{m}_{\text{tgt}},\bm{y}^{\prime})\xrightarrow{\tau^{\prime\prime}}(\bm{0},\bm{0})\text{
in }\mathcal{N}_{B}.$

From this, we conclude that $\bm{m}_{\text{src}}\in A$,
$\bm{m}_{\text{tgt}}\in B$ and
$\bm{m}_{\text{src}}\xrightarrow{}^{*}\bm{m}_{\text{tgt}}$ in $\mathcal{N}$.

As a consequence of Proposition 20, combined with Theorems 12 and 16, we
obtain the following corollary:

######  Corollary 21.

A negative answer to a convex polytope query $A\xrightarrow{}^{*}B$ is
witnessed by a locally closed bi-separator, for an altered Petri net,
computable in polynomial time and checkable in NC.

##  8\. Conclusion

We have shown that continuous Petri nets admit locally closed bi-separators
that can be efficiently computed. These separators are succinct and very
efficiently checkable certificates of unreachability. In particular, checking
that a linear formula is a locally closed bi-separator is in NC, and only
requires to solve linear inequations in one variable over the nonnegative
reals. While this does not directly hold for the more general of set-to-set
reachability, we have shown that it can be extended to an altered Petri net
(in the case of convex polytopes).

Verification tools that have not been formally verified, or rely (as is
usually the case) on external packages for linear arithmetic, can apply our
results to provide certificates for their output. Further, our separators can
be used as explanations of why a certain marking is unreachable. Obtaining
minimal explanations is an interesting research avenue.

From a logical point of view, separators are very closely related to
interpolants for linear arithmetic, which are widely used in formal
verification to refine abstractions in the CEGAR approach [BZM08, RS10,
SPDA14, ABKS15]. We intend to explore whether they can constitute the basis of
a CEGAR approach for the verification of continuous Petri nets.

## Acknowledgment

We thank the anonymous referees of LMCS and FoSSaCS 2022 for their comments,
and in particular for suggesting a more intuitive definition of bi-separators.

## References

  * [ABKS15] Ernst Althaus, Björn Beber, Joschka Kupilas, and Christoph Scholl.  Improving interpolants for linear arithmetic.  In Proc. $\text{13}^{\text{th}}$ International on Automated Technology for Verification and Analysis (ATVA), pages 48–63, 2015.  doi:10.1007/978-3-319-24953-7_5.
  * [BEH+20] Michael Blondin, Javier Esparza, Martin Helfrich, Antonín Kucera, and Philipp J. Meyer.  Checking qualitative liveness properties of replicated systems with stochastic scheduling.  In Proc. $\text{32}^{\text{nd}}$ International Conference on Computer Aided Verification (CAV), volume 12225, pages 372–397, 2020.  doi:10.1007/978-3-030-53291-8_20.
  * [BFHH17] Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad.  The logical view on continuous Petri nets.  ACM Transactions on Computational Logic (TOCL), 18(3):24:1–24:28, 2017.  doi:10.1145/3105908.
  * [BH17] Michael Blondin and Christoph Haase.  Logics for continuous reachability in Petri nets and vector addition systems with states.  In Proc. $\text{32}^{nd}$ Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–12, 2017.  doi:10.1109/LICS.2017.8005068.
  * [BMTZ21] Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche.  Context-bounded verification of liveness properties for multithreaded shared-memory programs.  Proceedings of the ACM on Programming Languages (PACMPL), 5:1–31, 2021.  doi:10.1145/3434325.
  * [BZM08] Dirk Beyer, Damien Zufferey, and Rupak Majumdar.  Csisat: Interpolation for LA+EUF.  In Proc. $\text{20}^{\text{th}}$ International Conference on Computer Aided Verification (CAV), pages 304–308, 2008.  doi:10.1007/978-3-540-70545-1_29.
  * [CO21] Wojciech Czerwinski and Lukasz Orlikowski.  Reachability in vector addition systems is Ackermann-complete.  In Proc. $\text{62}^{\text{nd}}$ IEEE Annual Symposium on Foundations of Computer Science (FOCS), pages 1229–1240. IEEE, 2021.  doi:10.1109/FOCS52979.2021.00120.
  * [DA10] René David and Hassane Alla.  Discrete, Continuous, and Hybrid Petri nets.  Springer, second edition, 2010.
  * [DE95] Jorg Desel and Javier Esparza.  Free choice Petri nets.  Number 40. Cambridge University Press, 1995.
  * [EHJM20] Javier Esparza, Martin Helfrich, Stefan Jaax, and Philipp J. Meyer.  Peregrine 2.0: Explaining correctness of population protocols through stage graphs.  In Proc. $\text{18}^{\text{th}}$ International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 12302, pages 550–556, 2020.  doi:10.1007/978-3-030-59152-6_32.
  * [FH15] Estíbaliz Fraca and Serge Haddad.  Complexity analysis of continuous Petri nets.  Fundamenta Informaticae, 137(1):1–28, 2015.  doi:10.3233/FI-2015-1168.
  * [FMW+17] Yu Feng, Ruben Martins, Yuepeng Wang, Işil Dillig, and Thomas W. Reps.  Component-based synthesis for complex APIs.  In Proc. $\text{44}^{\text{th}}$ ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 599–612. ACM, 2017.  doi:10.1145/3009837.3009851.
  * [GS92] Steven M. German and A. Prasad Sistla.  Reasoning about systems with many processes.  Journal of the ACM, 39(3):675–735, 1992.  doi:10.1145/146637.146681.
  * [Ler12] Jérôme Leroux.  Vector addition systems reachability problem (A simpler solution).  In Turing-100 – The Alan Turing Centenary, volume 10, pages 214–228, 2012.  doi:10.29007/bnx2.
  * [Ler21] Jérôme Leroux.  The reachability problem for Petri nets is not primitive recursive.  In Proc. $\text{62}^{\text{nd}}$ IEEE Annual Symposium on Foundations of Computer Science (FOCS), pages 1241–1252. IEEE, 2021.  doi:10.1109/FOCS52979.2021.00121.
  * [LS19] Jérôme Leroux and Sylvain Schmitz.  Reachability in vector addition systems is primitive-recursive in fixed dimension.  In Proc. $34^{\text{th}}$ Symposium on Logic in Computer Science (LICS), pages 1–13, 2019.  doi:10.1109/LICS.2019.8785796.
  * [RS10] Andrey Rybalchenko and Viorica Sofronie-Stokkermans.  Constraint solving for interpolation.  Journal of Symbolic Computation, 45(11):1212–1233, 2010.  doi:10.1016/j.jsc.2010.06.005.
  * [Sch86] Alexander Schrijver.  Theory of Linear and Integer Programming.  John Wiley & Sons, 1986.
  * [Son85] Eduardo D. Sontag.  Real addition and the polynomial hierarchy.  Information Processing Letters, 20(3):115–120, 1985.
  * [SPDA14] Christoph Scholl, Florian Pigorsch, Stefan Disch, and Ernst Althaus.  Simple interpolants for linear arithmetic.  In Proc. Conference & Exhibition on Design, Automation & Test in Europe (DATE), pages 1–6, 2014.  doi:10.7873/DATE.2014.128.

##  Appendix A Missing proofs

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

Let $\mathcal{S}$ and $\mathcal{S}^{\prime}$ denote the two systems of the
proposition. We must show that $\mathcal{S}$ has no solution iff
$\mathcal{S}^{\prime}$ has a solution. First, we prove the following claim:

Claim: The system $\exists\bm{x}\geq\bm{0}:\mathbf{A}\bm{x}=\bm{b}\land
S\subseteq\mathrm{supp}(\bm{x})\subseteq S^{\prime}$ has a solution iff this
system has a solution: $\exists\bm{x}\geq\bm{0},y\geq
1:\mathbf{A}\bm{x}=y\bm{b}\land\bm{x}=_{\,\overline{V}}\bm{0}\land\bm{x}\geq_{U}\bm{1}$,
where $\bm{1}\coloneqq(1,\ldots,1)$.

Proof of the claim: $\Rightarrow$) Since $\bm{x}(t)>0$ for all $t\in S$, we
can pick $y\geq 1$ sufficiently large so that $y\bm{x}(t)\geq 1$ for every
$t\in S$. Let $\bm{x}^{\prime}\coloneqq y\bm{x}$. We have
$\mathbf{A}\bm{x}^{\prime}=y\mathbf{A}\bm{x}=y\bm{b}$ and
$\bm{x}^{\prime}=y\bm{x}\geq\bm{x}\geq\bm{0}$. Moreover,
$\bm{x}^{\prime}(t)=y\bm{x}(t)=0$ for every $t\notin S^{\prime}$, and
$\bm{x}^{\prime}(t)=y\bm{x}(t)\geq 1$ for every $t\in S$.

$\Leftarrow$) Let $\bm{x}^{\prime}\coloneqq\bm{x}/y$. We have
$\mathbf{A}\bm{x}^{\prime}=\bm{b}$. Moreover, for every $t\notin S^{\prime}$
it is the case that $\bm{x}^{\prime}(t)=(1/y)\bm{x}(t)t=0$ and for every
$ts\in S$ it is the case that $\bm{x}^{\prime}(t)=(1/y)\bm{x}(t)\geq 1/y>0$.
Hence, $S\subseteq\mathrm{supp}(\bm{x}^{\prime})\subseteq S^{\prime}$.

Now we proceed to prove the proposition. Let
$\mathbf{J}\in\mathbb{R}^{\overline{S^{\prime}}\times T}$ be the matrix that
contains $0$ everywhere except for $\mathbf{J}_{t,t}=1$ for all $t\notin
S^{\prime}$. Let $\bm{c}\in\mathbb{R}^{T}$ be such that $\bm{c}(t)=1$ for
every $t\in S$ and $\bm{c}(t)=0$ for every $t\notin S$. By the claim above,
the system $\mathcal{S}$ has a solution iff the system
$\exists\bm{x}^{\prime}:\mathbf{A}^{\prime}\bm{x}^{\prime}\leq\bm{b}^{\prime}$
has a solution, where

$\mathbf{A}^{\prime}\coloneqq\begin{pmatrix}\mathbf{A}&-\bm{b}\\\
-\mathbf{A}&\bm{b}\\\ \mathbf{J}&\bm{0}\\\ -\mathbf{I}&\bm{0}\\\
\bm{0}^{\mathsf{T}}&-1\end{pmatrix}\text{ and
}\bm{b}^{\prime}\coloneqq\begin{pmatrix}\bm{0}\\\ \bm{0}\\\ \bm{0}\\\
-\bm{c}\\\ -1\end{pmatrix}.$

By Lemma 1, the latter system has no solution iff the following has one:
$\exists\bm{z}\geq\bm{0}:(\mathbf{A}^{\prime})^{\mathsf{T}}\bm{z}=\bm{0}\land(\bm{b}^{\prime})^{\mathsf{T}}\bm{z}<0$.
We can rewrite the latter as follows:

$\displaystyle\exists\bm{z}\geq\bm{0}:(\mathbf{A}^{\prime})^{\mathsf{T}}\bm{z}=\bm{0}\land(\bm{b}^{\prime})^{\mathsf{T}}\bm{z}<0$
$\displaystyle\equiv\ $
$\displaystyle\exists(\bm{u},\bm{u}^{\prime},\bm{v},\bm{v}^{\prime},\alpha)\geq\bm{0}:\mathbf{A}^{\mathsf{T}}(\bm{u}-\bm{u}^{\prime})=\bm{v}^{\prime}-\mathbf{J}^{\mathsf{T}}\bm{v}\land\bm{b}^{\mathsf{T}}(\bm{u}^{\prime}-\bm{u})=\alpha\land-\bm{c}^{\mathsf{T}}\bm{v}^{\prime}-\alpha<0$
$\displaystyle\equiv\ $ $\displaystyle\exists\bm{y}\
\exists(\bm{v},\bm{v}^{\prime},\alpha)\geq\bm{0}:\mathbf{A}^{\mathsf{T}}\bm{y}=\bm{v}^{\prime}-\mathbf{J}^{\mathsf{T}}\bm{v}\land\bm{b}^{\mathsf{T}}\bm{y}=-\alpha\land-\alpha<\bm{c}^{\mathsf{T}}\bm{v}^{\prime}$
$\displaystyle\equiv\ $ $\displaystyle\exists\bm{y}\
\exists(\bm{v},\bm{v}^{\prime})\geq\bm{0}:\mathbf{A}^{\mathsf{T}}\bm{y}=\bm{v}^{\prime}-\mathbf{J}^{\mathsf{T}}\bm{v}\land\bm{b}^{\mathsf{T}}\bm{y}\leq
0\land\bm{b}^{\mathsf{T}}\bm{y}<\bm{c}^{\mathsf{T}}\bm{v}^{\prime}$
$\displaystyle\equiv\ $
$\displaystyle\exists\bm{y}:\mathbf{A}^{\mathsf{T}}\bm{y}\geq_{S^{\prime}}\bm{0}\land\bm{b}^{\mathsf{T}}\bm{y}\leq
0\land\bm{b}^{\mathsf{T}}\bm{y}<\sum_{s\in
S}(\mathbf{A}^{\mathsf{T}}\bm{y})_{s}.$

Note that the last equivalence holds since
$(\mathbf{J}^{\mathsf{T}}\bm{v})=_{S^{\prime}}\bm{0}$ and since
$\bm{c}^{\mathsf{T}}$ sums entries over $S$.