Uppsala University, Sweden Uppsala University, Sweden University of Edinburgh,
UK University of Edinburgh, UK University of Edinburgh,
UKhttps://orcid.org/0000-0001-5274-8190 Parosh Aziz Abdulla, Mohamed Faouzi
Atig, Radu Ciobanu, Richard Mayr and Patrick Totzke This work was supported by
the EPSRC, grant EP/M027651/1.

###### Acknowledgements.

Sven Schewe and Lijun Zhang 2 29th International Conference on Concurrency
Theory (CONCUR 2018) CONCUR 2018 CONCUR 2018 September 4–7, 2018 Beijing,
China 118 6

# Universal Safety for Timed Petri Nets is PSPACE-complete

Parosh Aziz Abdulla  ,  Mohamed Faouzi Atig  ,  Radu Ciobanu  ,  Richard Mayr
and  Patrick Totzke

###### Abstract.

A timed network consists of an arbitrary number of initially identical 1-clock
timed automata, interacting via hand-shake communication. In this setting
there is no unique central controller, since all automata are initially
identical. We consider the universal safety problem for such controller-less
timed networks, i.e., verifying that a bad event (enabling some given
transition) is impossible regardless of the size of the network.

This universal safety problem is dual to the existential coverability problem
for timed-arc Petri nets, i.e., does there exist a number $m$ of tokens, such
that starting with $m$ tokens in a given place, and none in the other places,
some given transition is eventually enabled.

We show that these problems are PSPACE-complete.

###### Key words and phrases:

timed networks, safety checking, Petri nets, coverability

###### 1991 Mathematics Subject Classification:

[500]Theory of computation Timed and hybrid models

###### category:

##  1\. Introduction

#### Background.

Timed-arc Petri nets (TPN) [4, 16, 3, 8, 13] are an extension of Petri nets
where each token carries one real-valued clock and transitions are guarded by
inequality constraints where the clock values are compared to integer bounds
(via strict or non-strict inequalities). The known models differ slightly in
what clock values newly created tokens can have, i.e., whether newly created
tokens can inherit the clock value of some input token of the transition, or
whether newly created tokens always have clock value zero. We consider the
former, more general, case.

Decision problems associated with the reachability analysis of (extended)
Petri nets include _Reachability_ (can a given marking reach another given
marking?) and _Coverability_ (can a given marking ultimately enable a given
transition?).

While Reachability is undecidable for all these TPN models [15], Coverability
is decidable using the well-quasi ordering approach of [1, 10] and complete
for the hyper-Ackermannian complexity class $F_{\omega^{\omega^{\omega}}}$
[12]. With respect to Coverability, TPN are equivalent [7] to (linearly
ordered) data nets [14].

The _Existential Coverability_ problem for TPN asks, for a given place $p$ and
transition $t$, whether there exists a number $m$ such that the marking
$M(m)\overset{\text{\tiny def}}{=}m\cdot\\{(p,\bm{0})\\}$ ultimately enables
$t$. Here, $M(m)$ contains exactly $m$ tokens on place $p$ with all clocks set
to zero and _no other tokens_. This problem corresponds to checking safety
properties in distributed networks of arbitrarily many (namely $m$) initially
identical timed processes that communicate by handshake. A negative answer
certifies that the ‘bad event’ of transition $t$ can never happen regardless
of the number $m$ of processes, i.e., the network is safe for any size. Thus
by checking existential coverability, one solves the dual problem of
_Universal Safety_. (Note that the $m$ timed tokens/processes are only
initially identical. They can develop differently due to non-determinacy in
the transitions.)

The corresponding problem for timed networks studied in [2] does not allow the
dynamic creation of new timed processes (unlike the TPN model which can
increase the number of timed tokens), but considers multiple clocks per
process (unlike our TPN with one clock per token).

The TPN model above corresponds to a distributed network without a central
controller, since initially there are no tokens on other places that could be
used to simulate one. Adding a central controller would make _Existential
Coverability_ polynomially inter-reducible with normal _Coverability_ and thus
complete for $F_{\omega^{\omega^{\omega}}}$ [12] (and even undecidable for
$>1$ clocks per token [2]).

Aminof et. al. [6] study the model checking problem of $\omega$-regular
properties for the controller-less model and in particular claim an
$\mathsf{EXPSPACE}$ upper bound for checking universal safety. However, their
result only holds for discrete time (integer-valued clocks) and they do not
provide a matching lower bound.

#### Our contribution.

We show that _Existential Coverability_ (and thus universal safety) is
decidable and $\mathsf{PSPACE}$-complete. This positively resolves an open
question from [2] regarding the decidability of universal safety in the
controller-less networks. Moreover, a symbolic representation of the set of
coverable configurations can be computed (using exponential space).

The $\mathsf{PSPACE}$ lower bound is shown by a reduction from the iterated
monotone Boolean circuit problem. (It does not follow directly from the
$\mathsf{PSPACE}$-completeness of the reachability problem in timed automata
of [5], due to the lack of a central controller.)

The main ideas for the $\mathsf{PSPACE}$ upper bound are as follows. First we
provide a logspace reduction of the Existential Coverability problem for TPN
to the corresponding problem for a syntactic subclass, non-consuming TPN. Then
we perform an abstraction of the real-valued clocks, similar to the one used
in [3]. Clock values are split into integer parts and fractional parts. The
integer parts of the clocks can be abstracted into a finite domain, since the
transition guards cannot distinguish between values above the maximal constant
that appears in the system. The fractional parts of the clock values that
occur in a marking are ordered sequentially. Then every marking can be
abstracted into a string where all the tokens with the $i$-th fractional clock
value are encoded in the $i$-th symbol in the string. Since token
multiplicities do not matter for existential coverability, the alphabet from
which these strings are built is finite. The primary difficulty is that the
length of these strings can grow dynamically as the system evolves, i.e., the
space of these strings is still infinite for a given TPN. We perform a forward
exploration of the space of reachable strings. By using an acceleration
technique, we can effectively construct a symbolic representation of the set
of reachable strings in terms of finitely many regular expressions. Finally,
we can check existential coverability by using this symbolic representation.

##  2\. Timed Petri Nets

We use ${\rm Nature}$ and ${\mathbb{R}}_{\geq 0}$ to denote the sets of
nonnegative integers and reals, respectively. For $n\in{\rm Nature}$ we write
$[{n}]$ for the set $\mathopen{}\mathclose{{}\left\\{0,\ldots,n}\right\\}$.

For a set ${\it A}$, we use ${{\it A}}^{*}$ to denote the set of words, i.e.
finite sequences, over ${\it A}$, and write $\varepsilon$ for the empty word.
If $R$ is a regular expression over ${\it A}$ then
$\mathcal{L}\mathopen{}\mathclose{{}\left(R}\right)\subseteq{\it A}^{*}$
denotes its language.

A _multiset_ over a set $X$ is a function $M:X\to\mathbb{N}$. The set
${X}^{\oplus}$ of all (finitely supported) multisets over $X$ is partially
ordered pointwise (by $\leq$). The multiset union of
$M,M^{\prime}\in{X}^{\oplus}$ is $(M\oplus M^{\prime})\in{X}^{\oplus}$ with
$(M\oplus M^{\prime})(\alpha)\overset{\text{\tiny
def}}{=}M(\alpha)+M^{\prime}(\alpha)$ for all $\alpha\in X$. If $M\geq
M^{\prime}$ then the multiset difference $(M\ominus M^{\prime})$ is the unique
$M^{\prime\prime}\in{X}^{\oplus}$ with $M=M^{\prime}\oplus M^{\prime\prime}$.
We will use a monomial representation and write for example
$(\alpha+\beta^{3})$ for the multiset $(\alpha\mapsto 1,\beta\mapsto 3)$. For
a multiset $M$ and a number $m\in\mathbb{N}$ we let $m\cdot M$ denote the
$m$-fold multiset sum of $M$. We further lift this to sets of numbers and
multisets on the obvious fashion, so that in particular $\mathbb{N}\cdot
S\overset{\text{\tiny def}}{=}\\{n\cdot M\mid n\in\mathbb{N},M\in S\\}$.

_Timed Petri nets_ are place/transition nets where each token carries a real
value, sometimes called its _clock value_ or _age_. Transition firing depends
on there being sufficiently many tokens whose value is in a specified
interval. All tokens produced by a transition either have age $0$, or inherit
the age of an input-token of the transition. To model time passing, all token
ages can advance simultaneously by the same (real-valued) amount.

######  Definition 1 (TPN).

A _timed Petri net_ (TPN)
$\mathcal{N}=(P,T,\mathit{Var},G,\mathit{Pre},\mathit{Post})$ consists of
finite sets of _places_ $P$, _transitions_ $T$ and _variables_ $\mathit{Var}$,
as well as functions $G,\mathit{Pre},\mathit{Post}$ defining transition
_guards_ , _pre_ – and _postconditions_ , as follows.

For every transition $t\in T$, the guard $G(t)$ maps variables to (open, half-
open or closed) intervals with endpoints in $\mathbb{N}\cup\\{\infty\\}$,
restricting which values variables may take. All numbers are encoded in unary.
The precondition $\mathit{Pre}(t)$ is a finite multiset over
$(P\times\mathit{Var})$. Let $\mathit{Var}(t)\subseteq\mathit{Var}$ be the
subset of variables appearing positively in $\mathit{Pre}(t)$. The
postcondition $\mathit{Post}(t)$ is then a finite multiset over
$(P\times(\\{0\\}\cup\mathit{Var}(t)))$, specifying the locations and clock
values of produced tokens. Here, the symbolic clock value is either $0$
(demanding a reset to age $0$), or a variable that appeared already in the
precondition.

A _marking_ is a finite multiset over $P\times{\mathbb{R}}_{\geq 0}$.

######  Example 2.

The picture below shows a place/transition representation of an TPN with four
places and one transition. $\mathit{Var}(t)=\\{x,y\\}$,
$\mathit{Pre}(t)=(p,x)^{2}+(q,y)$, $G(t)(x)=[0,5]$, $G(t)(y)=]1,2]$ and
$\mathit{Post}(t)=(r,y)^{3}+(s,0)$.

pt$0\leq x\leq 5$$1<y\leq 2$$t$$p$$q$$r$$s$$x^{2}$$y$$y^{3}$$0$

The transition $t$ consumes two tokens from place $p$, both of which have the
same clock value $x$ (where $0\leq x\leq 5$) and one token from place $q$ with
clock value $y$ (where $1<y\leq 2$). It produces three tokens on place $r$ who
all have the same clock value $y$ (where $y$ comes from the clock value of the
token read from $q$), and another token with value $0$ on place $s$.

There are two different binary step relations on markings: _discrete_ steps
$\longrightarrow_{t}$ which fire a transition $t$ as specified by the
relations $G,\mathit{Pre}$, and $\mathit{Post}$, and _time passing_ steps
$\longrightarrow_{d}$ for durations $d\in{\mathbb{R}}_{\geq 0}$, which simply
increment all clocks by $d$.

######  Definition 3 (Discrete Steps).

For a transition $t\in T$ and a variable evaluation
$\pi:\mathit{Var}\to{\mathbb{R}}_{\geq 0}$, we say that _$\pi$ satisfies
$G(t)$_ if $\pi(x)\in G(t)(x)$ holds for all $x\in\mathit{Var}$. By lifting
$\pi$ to multisets over $(P\times\mathit{Var})$ (respectively, to multisets
over $(P\times(\\{0\\}\cup\mathit{Var}))$ with $\pi(0)=0$) in the canonical
way, such an evaluation translates preconditions $\mathit{Pre}(t)$ and
$\mathit{Post}(t)$ into markings $\pi(\mathit{Pre}(t))$ and
$\pi(\mathit{Post}(t))$, where for all $p\in P$ and $c\in{\mathbb{R}}_{\geq
0}$,

$\displaystyle\pi(\mathit{Pre}(t))(p,c)\overset{\text{\tiny
def}}{=}\sum_{\pi(v)=c}\mathit{Pre}(t)(p,v)\qquad\text{and}\qquad\pi(\mathit{Post}(t))(p,c)\overset{\text{\tiny
def}}{=}\sum_{\pi(v)={c}}\mathit{Post}(t)(p,{v}).$

A transition $t\in T$ is called _enabled_ in marking $M$, if there exists an
evaluation $\pi$ that satisfies $G(t)$ and such that $\pi(\mathit{Pre}(t))\leq
M$. In this case, there is a discrete step $M\longrightarrow_{t}M^{\prime}$
from marking $M$ to $M^{\prime}$, defined as
$M^{\prime}=M\ominus\pi(\mathit{Pre}(t))\oplus\pi(\mathit{Post}(t)).$

######  Definition 4 (Time Steps).

Let $M$ be a marking and $d\in{\mathbb{R}}_{\geq 0}$. There is a time step
$M\longrightarrow_{d}M^{\prime}$ to the marking $M^{\prime}$ with
$M^{\prime}(p,{c})\overset{\text{\tiny def}}{=}M(p,{c}-{d})$ for ${c}\geq{d}$,
and $M^{\prime}(p,{c})\overset{\text{\tiny def}}{=}0$, otherwise. We also
refer to $M^{\prime}$ as $(M+d)$.

We write $\xrightarrow{}_{\textit{Time}}$ for the union of all timed steps,
$\xrightarrow{}_{\textit{Disc}}$ for the union of all discrete steps and
simply $\xrightarrow{}$ for
$\xrightarrow{}_{\textit{Disc}}\cup\xrightarrow{}_{\textit{Time}}{}$. The
transitive and reflexive closure of $\xrightarrow{}$ is $\xrightarrow{*}$.
$\mathit{Cover}\mathopen{}\mathclose{{}\left(M}\right)$ denotes the set of
markings $M^{\prime}$ for which there is an $M^{\prime\prime}\geq M^{\prime}$
with $M\xrightarrow{*}M^{\prime\prime}$.

We are interested in the _existential coverability problem_ ($\exists$COVER
for short), as follows.

Input: A TPN, an initial place $p$ and a transition $t$. Question: Does there
exist
$M\in\mathit{Cover}\mathopen{}\mathclose{{}\left(\mathbb{N}\cdot\\{(p,{0})\\}}\right)$
that enables $t$?

We show that this problem is $\mathsf{PSPACE}$-complete. Both lower and upper
bound will be shown (w.l.o.g., see Lemma 8) for the syntactic subclass of
_non-consuming_ TPN, defined as follows.

######  Definition 5.

A _timed Petri net_ $(P,T,\mathit{Var},G,\mathit{Pre},\mathit{Post})$ is _non-
consuming_ if for all $t\in T$, $p\in P$ and $x\in\mathit{Var}$ it holds that
both 1) $\mathit{Pre}(t)(p,x)\leq 1$, and 2)
$\mathit{Pre}(t)\leq\mathit{Post}(t)$.

In a non-consuming TPN, token multiplicities are irrelevant for discrete
transitions. Intuitively, having one token $(p,{c})$ is equivalent to having
an inexhaustible supply of such tokens.

The first condition is merely syntactic convenience. It asks that each
transition takes at most one token from each place. The second condition in
Definition 5 implies that for each discrete step
$M\longrightarrow_{t}M^{\prime}$ we have $M^{\prime}\geq M$. Therefore, once a
token $(p,{c})$ is present on a place $p$, it will stay there unchanged
(unless time passes), and it will enable transitions with $(p,{c})$ in their
precondition.

Wherever possible, we will from now on therefore allow ourselves to use the
set notation for markings, that is simply treat markings
$M\in{(P\times{\mathbb{R}}_{\geq 0})}^{\oplus}$ as sets
$M\subseteq(P\times{\mathbb{R}}_{\geq 0})$.

##  3\. Lower Bound

$\mathsf{PSPACE}$-hardness of $\exists$COVER does not follow directly from the
$\mathsf{PSPACE}$-completeness of the reachability problem in timed automata
of [5]. The non-consuming property of our TPN makes it impossible to fully
implement the control-state of a timed automaton. Instead our proof uses
multiple timed tokens and a reduction from the iterated monotone Boolean
circuit problem [11].

A depth-1 monotone Boolean circuit is a function
$F:\\{0,1\\}^{n}\to\\{0,1\\}^{n}$ represented by $n$ constraints: For every
$0\leq i<n$ there is a constraint of the form $i^{\prime}=j\otimes k,$ where
$0\leq j,k<n$ and $\otimes\in\\{\wedge,\vee\\}$, which expresses how the next
value of bit $i$ depends on the current values of bits $j$ and $k$. For every
bitvector $\bm{v}\in\\{0,1\\}^{n}$, the function $F$ then satisfies
$F(\bm{v})[i]\overset{\text{\tiny def}}{=}\bm{v}[j]\otimes\bm{v}[k]$. It is
$\mathsf{PSPACE}$-complete to check whether for a given vector
$\bm{v}\in\\{0,1\\}^{n}$ there exists a number $m\in\mathbb{N}$ such that
$F^{m}(\bm{v})[0]=1$.

Towards a lower bound for $\exists$COVER (Theorem 7) we construct a non-
consuming TPN as follows, for a given circuit. The main idea is to simulate
circuit constraints by transitions that reset tokens of age $1$ (encoding
$\bm{v}$) to fresh ones of age $0$ (encoding $F(\bm{v})$), and let time pass
by one unit to enter the next round.

$\mathit{True}_{j}$$\mathit{True}_{i}$$\mathit{True}_{k}$$\mathit{False}_{j}$$\mathit{False}_{i}$$\mathit{False}_{k}$$x=y=1$$i.B$$x=1$$i.L$$x=1$$i.R$$x$$y$$0$$x$$0$$x$$0$
Figure 1. The transitions $i.B,i.R$ and $i.L$ that simulate the update of bit
$i$ according to constraint $i^{\prime}=j\land k$. All transitions demand that
incoming tokens are of age exactly $1$ and only tokens of age $0$ are
produced.

For every bit $0\leq i<n$, the net contains two places $\mathit{True}_{i}$ and
$\mathit{False}_{i}$. A marking $M_{\bm{v}}\leq P\times{\mathbb{R}}_{\geq 0}$
is an _encoding_ of a vector $\bm{v}\in\\{0,1\\}^{n}$ if for every $0\leq i<n$
the following hold.

  1. (1)

$(\mathit{True}_{i},0)\in M_{\bm{v}}\iff\bm{v}[i]=1$.

  2. (2)

$(\mathit{False}_{i},0)\in M_{\bm{v}}\iff\bm{v}[i]=0$.

  3. (3)

If $(p,c)\in M_{\bm{v}}$ then $c=0$ or $c\geq 1$.

Note that in particular one cannot have both $(\mathit{True}_{i},0)$ and
$(\mathit{False}_{i},0)$ in $M_{\bm{v}}$. For every constraint
$i^{\prime}=j\land k$ we introduce three transitions, $i.L,i.R$, and $i.B$,
where

$\displaystyle\mathit{Pre}(i.B)$ $\displaystyle\overset{\text{\tiny
def}}{=}{(\mathit{True}_{j},x)+(\mathit{True}_{k},y)}$
$\displaystyle\mathit{Post}(i.B)\overset{\text{\tiny
def}}{=}\mathit{Pre}(i.B)+{(\mathit{True}_{i},0)}$
$\displaystyle\mathit{Pre}(i.L)$ $\displaystyle\overset{\text{\tiny
def}}{=}{(\mathit{False}_{j},x)}$
$\displaystyle\mathit{Post}(i.L)\overset{\text{\tiny
def}}{=}\mathit{Pre}(i.L)+(\mathit{False}_{i},0)$
$\displaystyle\mathit{Pre}(i.R)$ $\displaystyle\overset{\text{\tiny
def}}{=}{(\mathit{False}_{k},x)}$
$\displaystyle\mathit{Post}(i.R)\overset{\text{\tiny
def}}{=}\mathit{Pre}(i.R)+(\mathit{False}_{i},0)$

and the guard for all transitions is $G(x)=G(y)=1$. See Figure 1 for an
illustration. For disjunctions $i^{\prime}=j\lor k$ the transitions are
defined analogously, with $\mathit{True}$ and $\mathit{False}$ inverted. The
correctness proof of our construction rests on the following simple
observation.

######  Lemma 6.

If $F(\bm{v})=\bm{v}^{\prime}$ then for every encoding $M_{\bm{v}}$ of
$\bm{v}$, there exists an encoding $M_{\bm{v^{\prime}}}$ of $\bm{v}^{\prime}$
such that
$M_{\bm{v}}\longrightarrow_{1}\xrightarrow{*}_{\textit{Disc}}M_{\bm{v}^{\prime}}$.
Conversely, if
$M_{\bm{v}}\longrightarrow_{1}\xrightarrow{*}_{\textit{Disc}}M_{\bm{v}^{\prime}}$
for encodings $M_{\bm{v}}$ and $M_{\bm{v^{\prime}}}$ of $\bm{v}$ and
$\bm{v}^{\prime}$ respectively, then $F(\bm{v})=\bm{v^{\prime}}$.

###### Proof.

For the first part, we construct a sequence
$M_{0}\xrightarrow{}_{\textit{Disc}}M_{1}\xrightarrow{}_{\textit{Disc}}\dots\xrightarrow{}_{\textit{Disc}}M_{n-1}$
where $M_{0}\overset{\text{\tiny def}}{=}(M_{\bm{v}}+1)$ and every step
$M_{i-1}\xrightarrow{}_{\textit{Disc}}M_{i}$ adds tokens simulating the $i$th
constraint of $F$. Since the TPN is non-consuming, we will have that
$M_{i}\geq(M_{\bm{v}}+1)$, for all $i<n$. Consider now constraint
$i^{\prime}$, and assume w.l.o.g. that $i^{\prime}=j\land k$ (the other case
is analogous). There are two cases depending on $\bm{v^{\prime}}[i]$.

  1. (1)

Case $\bm{v^{\prime}}[i]=1$. By our assumption that
$F(\bm{v})=\bm{v^{\prime}}$ we know that $\bm{v}[j]=1$ and $\bm{v}[k]=1$. So
$(\mathit{True}_{j},1)\in(M_{\bm{v}}+1)\leq M_{i-1}$ and
$(\mathit{True}_{k},1)\in(M_{\bm{v}}+1)\leq M_{i-1}$. By construction of the
net, there is a transition $i.B$ with
$\mathit{Pre}(i.B)={(\mathit{True}_{j},1)+(\mathit{True}_{k},1)}$ and
$\mathit{Post}(i.B)=\mathit{Pre}(i.B)+{(\mathit{True}_{i},0)}$. This justifies
step $M_{i-1}\longrightarrow_{i.B}M_{i}$ and therefore that $(True_{i},0)\in
M_{i}\leq M_{n-1}$. Also notice that no marking reachable from $M_{0}$ using
only discrete steps can contain the token $(\mathit{False}_{i},0)$. This is
because these can only be produced by transitions requiring either
$(\mathit{False}_{j},1)$ or $(\mathit{False}_{k},1)$, which are not contained
in $M_{0}$ by assumption that $M_{\bm{v}}$ encodes $\bm{v}$. Therefore
$(\mathit{False}_{i},0)\notin M_{n-1}$.

  2. (2)

Case $\bm{v^{\prime}}[i]=0$. W.l.o.g., $\bm{v}[j]=0$. Therefore,
$(\mathit{False}_{j},1)\in(M_{\bm{v}}+1)\leq M_{i-1}$. By construction of the
net, there exists transition $i.L$ with
$\mathit{Pre}(i.L)={(\mathit{False}_{j},1)}$ and
$\mathit{Post}(i.L)=\mathit{Pre}(i.L)+{(\mathit{False}_{i},0)}$. This
justifies the step $M_{i-1}\longrightarrow_{i.L}M_{i}$, with $(False_{i},0)\in
M_{i}\leq M_{n-1}$. Notice again that no marking reachable from $M_{0}$ using
only discrete steps can contain the token $(\mathit{True}_{i},0)$. This is
because these can only be produced by transitions $i.B$, requiring both
$(\mathit{True}_{j},1),(\mathit{True}_{k},1)\in M_{0}$, contradicting our
assumptions. Hence, $(\mathit{True}_{i},0)\notin M_{n-1}$.

We conclude that the constructed marking $M_{n-1}$ is an encoding of
$\bm{v^{\prime}}$.

For the other part of the claim, assume that there exist markings $M_{\bm{v}}$
and $M_{\bm{v^{\prime}}}$ which are encodings of vectors $\bm{v}$ and
$\bm{v^{\prime}}$, respectively, with
$M_{\bm{v}}\longrightarrow_{1}\xrightarrow{*}_{\textit{Disc}}M_{\bm{v^{\prime}}}$.
We will show that $F(\bm{v})=\bm{v}^{\prime}$. Recall that
$F(\bm{v})[i]\overset{\text{\tiny def}}{=}\bm{v}[j]\otimes\bm{v}[k]$, where
$0\leq j,k<n$ and $\otimes\in\\{\wedge,\vee\\}$. We will show for each $i<n$
that $\bm{v}^{\prime}[i]=\bm{v}[j]\otimes\bm{v}[k]$. Again, consider the
constraint $i^{\prime}$, and assume w.l.o.g. that $i^{\prime}=j\land k$ (the
other case is analogous). There are two cases.

  1. (1)

Case $\bm{v^{\prime}}[i]=1$. By definition of a marking encoding, we have that
$(\mathit{True}_{i},0)\in M_{\bm{v}}$. By construction, there is a transition
$i.B$ with $\mathit{Pre}(i.B)={(\mathit{True}_{j},1)+(\mathit{True}_{k},1)}$
and $\mathit{Post}(i.B)=\mathit{Pre}(i.B)+{(\mathit{True}_{i},0)}$. By
assumption, it holds that
$(M_{\bm{v}}+1)\xrightarrow{*}_{\textit{Disc}}M_{\bm{v}}^{\prime}$, where
$M_{\bm{v}}\longrightarrow_{1}(M_{\bm{v}}+1)$. Note that
$(\mathit{True}_{j},1)\in(M_{\bm{v}}+1)$ and
$(\mathit{True}_{k},1)\in(M_{\bm{v}}+1)$. Hence, we have that $\bm{v}[j]=1$
and $\bm{v}[k]=1$, and therefore that
$F(\bm{v})[i]=\bm{v^{\prime}}[i]=\bm{v}[j]\land\bm{v}[k]$.

  2. (2)

Case $\bm{v^{\prime}}[i]=0$. Then $(\mathit{False}_{i},0)\in M_{\bm{v}}$ and,
since this token can only be produced by transitions $i.L$ or $i.R$, either
$(\mathit{False}_{j},1)\in(M_{\bm{v}}+1)$ or
$(\mathit{False}_{k},1)\in(M_{\bm{v}}+1)$.

Therefore $(\mathit{False}_{j},0)\in(M_{\bm{v}})$ or
$(\mathit{False}_{k},0)\in(M_{\bm{v}})$ and because $M_{\bm{v}}$ is an
encoding of $\bm{v}$, this means that either $\bm{v}[j]=0$ or $\bm{v}[k]=0$.
Therefore, $F(\bm{v^{\prime}})[i]=\bm{v}[j]\land\bm{v}[k]=0$. ∎

######  Theorem 7.

$\exists$COVER is $\mathsf{PSPACE}$-hard for non-consuming TPN.

###### Proof.

For a given monotone Boolean circuit, define a non-consuming TPN as above. By
induction on $m\in\mathbb{N}$ using Lemma 6, we derive that there exists
$m\in\mathbb{N}$ with $F^{m}(\bm{v})=\bm{v}^{\prime}$ and
$\bm{v}^{\prime}[0]=1$ if, and only if, there exists encodings $M_{\bm{v}}$ of
$\bm{v}$ and $M_{\bm{v^{\prime}}}$ of $\bm{v^{\prime}}$, with
$M_{\bm{v}}\xrightarrow{*}M_{\bm{v}^{\prime}}$. Moreover, if there is a
marking $M$ such that $M_{\bm{v}}\xrightarrow{*}M$ and $0\in{\it frac}(M)$,
where $M$ contains a token of age $0$, then $M\leq M_{\bm{v^{\prime}}}$ for
some encoding $M_{\bm{v}^{\prime}}$ of a vector
$\bm{v^{\prime}}=F^{m}(\bm{v})$. This means that it suffices to add one
transition $t$ with $\mathit{Pre}(t)=(\mathit{True}_{0},0)$ whose enabledness
witnesses the existence of a reachable encoding $M_{\bm{v}^{\prime}}$
containing a token $(\mathit{True}_{0},0)$. By the properties above, there
exists $m\in\mathbb{N}$ with $F^{m}(\bm{v})=\bm{v}^{\prime}$ and
$\bm{v}^{\prime}[0]=1$ iff
$M_{\bm{v}}\xrightarrow{*}M_{\bm{v}^{\prime}}\xrightarrow{t}$. ∎

This lower bound holds even for discrete time TPN, e.g. [9], because the proof
uses only timed steps with duration $d=1$.

##  4\. Upper Bound

We start by observing that we can restrict ourselves, without loss of
generality, to non-consuming TPN (Definition 5) for showing the upper bound.
Intuitively, since we start with an arbitrarily high number of tokens anyway,
it does not matter how many of them are consumed by transitions during the
computation, since some always remain.

######  Lemma 8.

The $\exists$COVER problem for TPN logspace-reduces to the $\exists$COVER
problem for non-consuming TPN. That is, for every TPN $\mathcal{N}$ and for
every place $p$ and transition $t$ of $\mathcal{N}$, one can construct, using
logarithmic space, a non-consumimg TPN $\mathcal{N}^{\prime}$ together with a
place $p^{\prime}$ and transition $t^{\prime}$ of $\mathcal{N}^{\prime}$, so
that there exists
$M\in\mathit{Cover}_{\mathcal{N}}\mathopen{}\mathclose{{}\left(\mathbb{N}\cdot\\{(p,{0})\\}}\right)$
enabling $t$ in $\mathcal{N}$ if and only if there exists
$M^{\prime}\in\mathit{Cover}_{\mathcal{N}^{\prime}}\mathopen{}\mathclose{{}\left(\mathbb{N}\cdot\\{(p^{\prime},0)\\}}\right)$
that enables $t^{\prime}$ in $\mathcal{N}^{\prime}$.

###### Proof.

First notice that the first condition in Definition 5, that asks that every
transition takes at most one token each place, is merely a syntactic
convenience. A net satisfying this condition can be constructed by adding a
few extra places and intermediate transitions to first distribute tokens to
those extra places for the original transition to consume.

So let’s assume w.l.o.g., that $\mathcal{N}$ satisfies this condition and let
$\mathcal{N}^{\prime}$ be the non-consuming variant derived from $\mathcal{N}$
where for all transitions $T$,
$\mathit{Post}_{\mathcal{N}^{\prime}}(t)\overset{\text{\tiny
def}}{=}\mathit{Post}_{\mathcal{N}}(t)\oplus\mathit{Pre}_{\mathcal{N}}(t)$.
Notice that then, for every discrete step $M\longrightarrow_{t}M^{\prime}$ we
have that $M\leq M^{\prime}$. We prove the following claim.

######  Claim 8.1.

_For every place $p$ and transition $t$ of $\mathcal{N}$ there exists
$M\in\mathit{Cover}_{\mathcal{N}}(\mathbb{N}\cdot\\{(p,{0}\\})$ enabling $t$
in $\mathcal{N}$ if, and only if there exists
$M^{\prime}\in\mathit{Cover}_{\mathcal{N}^{\prime}}(\mathbb{N}\cdot\\{(p,0)\\})$
that enables $t$ in $\mathcal{N}^{\prime}$. _

The “$\mathcal{N}\to\mathcal{N}^{\prime}$” direction follows from the
observation that the pointwise ordering $\leq$ on markings, is a simulation:
If $M\xrightarrow{}N$ and $M^{\prime}\geq M$ then there exists an
$N^{\prime}\geq N$ with $M^{\prime}\xrightarrow{}N^{\prime}$. For the other
direction, suppose there exists a witnessing path

$m\cdot\\{(p,{0})\\}\leavevmode\nobreak\ =\leavevmode\nobreak\
M_{0}\xrightarrow{}M_{1}\xrightarrow{}M_{2}\xrightarrow{}\cdots\xrightarrow{}M_{k}\xrightarrow{t}$

of length $k$ in $\mathcal{N}^{\prime}$. We can inductively derive a
witnessing path in $\mathcal{N}$ backwards, again using the fact that $\leq$
is a simulation. First note that if $M^{\prime}$ enables $t$, then every
$m^{\prime}\cdot M^{\prime}$ with $m^{\prime}>0$ enables $t$, (in both nets).
Suppose $M_{i}\xrightarrow{\rho}$ is a path of length $(k-i)$ that ends in a
$t$-transition. By the simulation property, there is such a path from every
$m\cdot M_{i}$, $m>0$. Further, there must exist markings
$M^{\prime}_{i-1}\in\ \downarrow\\!{(}\mathbb{N}\cdot M_{i-1})$ and
$M^{\prime}_{i}\in\ \downarrow\\!{(}\mathbb{N}\cdot M_{i})$ such that
$M^{\prime}_{i-1}\xrightarrow{}M^{\prime}_{i}$. It suffices to pick
$M^{\prime}_{i-1}\overset{\text{\tiny def}}{=}B\cdot M_{i-1}$, where
$B\in\mathbb{N}$ is the maximal cardinality of any multiset $\mathit{Pre}(t)$
(This number is itself bounded by $\lvert
P\rvert\cdot\lvert\mathit{Var}\rvert$ by our assumption on $\mathit{Pre}(t)$).
We conclude that in $\mathcal{N}$ there is a path ending in a $t$-transition
and starting in marking $(B\cdot k)\cdot M_{0}$, which is in
$\mathbb{N}\cdot\\{(p,{0})\\}$. ∎

###  4.1. Region Abstraction

We recall a constraint system called regions defined for timed automata [5].
The version for TPN used here is similar to the one in [3].

Consider a fixed, nonconsuming TPN
$\mathcal{N}=(P,T,\mathit{Var},G,\mathit{Pre},\mathit{Post})$. Let
$c_{\mathit{max}}$ be the largest finite value appearing in transition guards
$G$. Since different tokens with age $>c_{\mathit{max}}$ cannot be
distinguished by transition guards, we consider only token ages below or equal
to $c_{\mathit{max}}$ and treat the integer parts of older tokens as equal to
$c_{\mathit{max}}+1$. Let ${\it int}(c)\overset{\text{\tiny
def}}{=}\min\\{c_{\mathit{max}}+1,\lfloor{c}\rfloor\\}$ and ${\it
frac}(c)\overset{\text{\tiny def}}{=}c-\lfloor{c}\rfloor$ for a real value
$c\in{\mathbb{R}}_{\geq 0}$. We will work with an abstraction of TPN markings
as words over the alphabet $\Sigma\overset{\text{\tiny
def}}{=}2^{P\times[{c_{\mathit{max}}+1}]}$. Each symbol $X\in\Sigma$
represents the places and integer ages of tokens for a particular fractional
value.

######  Definition 9.

Let $M\subseteq P\times{\mathbb{R}}_{\geq 0}$ be a marking and let ${\it
frac}(M)\overset{\text{\tiny def}}{=}\\{{\it frac}(c)\mid(p,c)\in M\\}$ be the
set of fractional clock values that appear in $M$.

Let $S\subset[0,1[$ be a finite set of real numbers with $0\in S$ and ${\it
frac}(M)\subseteq S$ and let $f_{0},f_{1},\dots,f_{n}$, be an enumeration of
$S$ so that $f_{i-1}<f_{i}$ for all $i\leq n$. The _$S$ -abstraction_ of $M$
is

$\mathit{abs}_{S}(M)\overset{\text{\tiny def}}{=}x_{0}x_{1}\dots
x_{n}\in\Sigma^{*}$

where $x_{i}\overset{\text{\tiny def}}{=}\\{(p,{\it int}(c))\mid(p,c)\in
M\land{\it frac}(c)=f_{i}\\}$ for all $i\leq n$. We simply write
$\mathit{abs}(M)$ for the shortest abstraction, i.e. with respect to
$S=\\{0\\}\cup{\it frac}(M)$.

######  Example 10.

The abstraction of marking $M=\\{(p,2.1),(q,2.2),(p,5.1),(q,5.1)\\}$ is
$\mathit{abs}(M)=\emptyset\leavevmode\nobreak\
\\{(p,2),(p,5),(q,5)\\}\leavevmode\nobreak\ \\{(q,2)\\}$. The first symbol is
$\emptyset$, because $M$ contains no token with an integer age (i.e., no token
whose age has fractional part $0$). The second and third symbols represent
sets of tokens with fractional values $0.1$ and $0.2$, respectively.

Clocks with integer values play a special role in the behavior of TPN, because
the constants in the transition guards are integers. Thus we always include
the fractional part $0$ in the set $S$ in Definition 9.

We use a special kind of regular expressions over $\Sigma$ to represent
coverable sets of TPN markings as follows.

######  Definition 11.

A regular expression $E$ over $\Sigma$ represents the downward-closed set of
TPN markings covered by one that has an abstraction in the language of $E$:

$[\\![E]\\!]\overset{\text{\tiny def}}{=}\\{N\mid\exists M\exists
S.\leavevmode\nobreak\ M\geq
N\land\mathit{abs}_{S}(M)\in\mathcal{L}\mathopen{}\mathclose{{}\left(E}\right)\\}.$

An expression is _simple_ if it is of the form $E=x_{0}x_{1}\dots x_{k}$ where
for all $i\leq k$ either $x_{i}\in\Sigma$ or $x_{i}={y_{i}}^{*}$ for some
$y_{i}\in\Sigma$. In the latter case we say that $x_{i}$ _carries a star_.
That is, a simple expression is free of Boolean combinators and uses only
concatenation and Kleene star. We will write $\hat{x}_{i}$ to denote the
symbol in $\Sigma$ at position $i$: it is $x_{i}$ if $x_{i}\in\Sigma$ and
$y_{i}$ otherwise.

######  Remark 12.

Notice that for all simple expressions $\alpha,\beta$ so that
$\lvert\alpha\rvert>0$, we have that
$[\\![\alpha\emptyset\beta]\\!]=[\\![\alpha\beta]\\!]$. However, unless
$\alpha$ has length $0$ or is of the form $\alpha=\emptyset\alpha^{\prime}$,
we have $[\\![\emptyset\alpha]\\!]\neq[\\![\alpha]\\!]$. This is because a
marking $M$ that contains a token $(p,c)$ with ${\it frac}(c)=0$ has the
property that all abstractions $\mathit{abs}_{S}(M)=x_{0}\dots x_{k}$ of $M$
have $x_{0}\neq\emptyset$.

The following lemmas express the effect of TPN transitions at the level of the
region abstraction. Lemmas 13 and 15 state that maximally firing of discrete
transitions (the relation $\xrightarrow{*}_{\textit{Disc}}$) is computable and
monotone. Lemmas 16 and 17 state how to represent timed-step successor
markings.

######  Lemma 13.

For every non-consuming TPN $\mathcal{N}$ there are polynomial time computable
functions $f:\Sigma\times\Sigma\times\Sigma\to\Sigma$ and
$g:\Sigma\times\Sigma\times\Sigma\to\Sigma$ with the following properties.

  1. (1)

$f$ and $g$ are monotone (w.r.t. subset ordering) in each argument.

  2. (2)

$f(\alpha,\beta,x)\supseteq x$ and $g(\alpha,\beta,x)\supseteq x$ for all
$\alpha,\beta,x\in\Sigma$.

  3. (3)

Suppose that $E=x_{0}x_{1}\dots x_{k}$ is a simple expression,
$\alpha\overset{\text{\tiny def}}{=}x_{0}$ and $\beta\overset{\text{\tiny
def}}{=}\bigcup_{i>0}\hat{x}_{i}$, and
$E^{\prime}=x^{\prime}_{0}x^{\prime}_{1}\dots x^{\prime}_{k}$ is the derived
expression defined by conditions:

    1. (a)

$x_{0}^{\prime}\overset{\text{\tiny def}}{=}f(\alpha,\beta,x_{0})$,

    2. (b)

$x_{i}^{\prime}\overset{\text{\tiny def}}{=}g(\alpha,\beta,\hat{x}_{i})^{*}$
for $i>0$,

    3. (c)

$x_{i}^{\prime}$ carries a star iff $x_{i}$ does.

Then $[\\![E^{\prime}]\\!]=\\{M^{\prime\prime}\mid\exists M\in[\\![E]\\!]\land
M\xrightarrow{*}_{\textit{Disc}}M^{\prime}\geq M^{\prime\prime}\\}$.

A proof of this statement is in the appendix. It is essentially due to the
monotonicity of discrete transition firing in TPN and the fact that
iteratively firing transitions must saturate due to the nonconsuming
semantics. We first prove it only for star-free expressions $E$ in condition 3
(Lemma 25) and then generalize to all simple expressions by induction.

######  Definition 14.

We will write $\mathit{SAT}(E)\overset{\text{\tiny def}}{=}E^{\prime}$ for the
successor expression $E^{\prime}$ of $E$ guaranteed by Lemma 13. I.e.,
$\mathit{SAT}(E)$ is the saturation of $E$ by maximally firing discrete
transitions.

Notice that by definition it holds that
$[\\![E]\\!]\subseteq[\\![\mathit{SAT}(E)]\\!]\subseteq\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![E]\\!]}\right)$,
and consequently also that
$\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![\mathit{SAT}(E)]\\!]}\right)=\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![E]\\!]}\right)$.

######  Lemma 15.

Suppose that $X=x_{0}x_{1}\dots x_{k}$ is a simple expression of length $k+1$
with $\mathit{SAT}(X)=x^{\prime}_{0}x^{\prime}_{1}\dots x^{\prime}_{k}$ and
$x_{0},x^{\prime}_{0}\in\Sigma$. Let
$Y=y_{0}\alpha_{1}y_{1}\alpha_{2}\dots\alpha_{k}y_{k}$ be a simple expression
with
$\mathit{SAT}(Y)=y^{\prime}_{0}\alpha^{\prime}_{1}y^{\prime}_{1}\alpha^{\prime}_{2}\dots\alpha^{\prime}_{k}y^{\prime}_{k}$
and $y_{0},y^{\prime}_{0}\in\Sigma$.

If $\hat{x}_{i}\subseteq\hat{y}_{i}$ for all $i\leq k$ then
$\hat{x}^{\prime}_{i}\subseteq\hat{y}^{\prime}_{i}$ for all $i\leq k$.

###### Proof.

The assumption of the lemma provides that $\alpha_{x}\overset{\text{\tiny
def}}{=}x_{0}\subseteq\alpha_{y}\overset{\text{\tiny def}}{=}y_{0}$ and
$\beta_{x}\overset{\text{\tiny def}}{=}\bigcup_{k\geq
i>0}\hat{x}_{i}\subseteq\beta_{y}\overset{\text{\tiny def}}{=}\bigcup_{k\geq
i>0}\hat{y}_{i}$. Therefore, by Item 1 of Lemma 13, we get that

$x^{\prime}_{0}=f(\alpha_{x},\beta_{x},x_{0})\quad\subseteq\quad
f(\alpha_{y},\beta_{y},y_{0})=y^{\prime}_{0}$

and similarly, for all $k\geq i\geq 0$, that
$\hat{x}^{\prime}_{i}=g(\alpha_{x},\beta_{x},\hat{x}_{i})\leavevmode\nobreak\
\subseteq\leavevmode\nobreak\
g(\alpha_{y},\beta_{y},\hat{y}_{i})=\hat{y}^{\prime}_{i}.$ ∎

For $x\in\Sigma$ we write $(x+1)\overset{\text{\tiny def}}{=}\\{(p,{\it
int}(n+1))\mid(p,n)\in x\\}$ for the symbol where token ages are incremented
by $1$.

######  Lemma 16.

$[\\![\emptyset E]\\!]=\\{M^{\prime}\mid\exists M\in[\\![E]\\!]\land
M\longrightarrow_{d}M^{\prime}\land d<1-\max(frac(M))\\}$.

###### Proof.

_“ $\supseteq$”_: Suppose that $M$ is a non-empty marking in $[\\![E]\\!]$,
$d<1-\max({\it frac}(M))$ and $M\longrightarrow_{d}M^{\prime}$. The assumption
on $d$ implies that for every token $(p,c)\in M$ we have ${\it int}(c)={\it
int}(c+d)$. In other words, the integral part of the token age remained the
same. Therefore $(p,{\it int}(c))=(p,{\it int}(c+d))\in M^{\prime}$. Also from
the assumption on $d$ we get that

${\it frac}(M^{\prime})=\\{x+d\mid x\in{\it frac}(M)\\}$

Recall that $\mathit{abs}(M)=\mathit{abs}_{S}(M)$ and
$\mathit{abs}(M^{\prime})=\mathit{abs}_{S^{\prime}}(M^{\prime})$ for the sets
$S\overset{\text{\tiny def}}{=}\\{0\\}\cup{\it frac}(M)$ and
$S^{\prime}\overset{\text{\tiny def}}{=}\\{0\\}\cup{\it frac}(M^{\prime})$.
Clearly, $0\notin{\it frac}(M^{\prime})$. There are two cases:

  1. (1)

$0\in{\it frac}(M)$. Then
$\mathit{abs}(M^{\prime})=\emptyset\mathit{abs}(M)\in\mathcal{L}\mathopen{}\mathclose{{}\left(\emptyset
E}\right)$, and consequently, $M^{\prime}\in[\\![\emptyset E]\\!]$.

  2. (2)

$0\notin{\it frac}(M)$. Then
$\mathit{abs}(M^{\prime})=\mathit{abs}(M)=\emptyset
w\in\mathcal{L}\mathopen{}\mathclose{{}\left(E}\right)$. Suppose that
$E=x_{0}\alpha$, i.e., $E$ has $x_{0}\in\Sigma$ as its leftmost symbol, and
$w\in\mathcal{L}\mathopen{}\mathclose{{}\left(\alpha}\right)$. If
$x_{0}=\emptyset$ then $[\\![E]\\!]=[\\![\emptyset E]\\!]$ and thus
$\mathit{abs}(M^{\prime})\in[\\![\emptyset E]\\!]$. Otherwise, if
$x_{0}\neq\emptyset$ then
$x_{0}w\in\mathcal{L}\mathopen{}\mathclose{{}\left(E}\right)$ and
$x_{0}w=\mathit{abs}(M^{\prime\prime})$ for some marking $M^{\prime\prime}\geq
M^{\prime}$. So again, $M^{\prime}\in[\\![\emptyset E]\\!]$.

_“ $\subseteq$”_: W.l.o.g., pick a non-empty marking
$M^{\prime}\in[\\![\emptyset E]\\!]$. If $E$ has $\emptyset$ as its leftmost
symbol, then $[\\![\emptyset E]\\!]=[\\![E]\\!]$ and the claim follows using
$d=0$, since then $M^{\prime}\in[\\![E]\\!]$. So suppose that $E$ does not
start with $\emptyset$. Note that by Definition 9, there are no tokens in the
marking $M^{\prime}$ whose clocks have fractional value zero. Let

$d\overset{\text{\tiny def}}{=}\min({\it frac}(M^{\prime}))$

be the minimal fractional clock value among the tokens of $M^{\prime}$ and
based on this, define $M\overset{\text{\tiny def}}{=}\\{(p,c-d)\mid(p,c)\in
N^{\prime}\\}$. By construction of $M$ we get $M\longrightarrow_{d}M^{\prime}$
and also that $\max({\it frac}(M))=\max({\it frac}(M^{\prime}))-d<1$.
Therefore that $1-\max({\it frac}(M))<1-d$. Finally, observe that ${\it
frac}(M)=\\{x-d\mid x\in{\it frac}(M^{\prime})\\}$ and $0\in{\it frac}(M)$. It
follows that $\mathit{abs}(M^{\prime})=\emptyset\mathit{abs}(M)$ and therefore
that $\mathit{abs}(M)\in\mathcal{L}\mathopen{}\mathclose{{}\left(E}\right)$
and $M\in[\\![E]\\!]$. This means that $M^{\prime}$ is included in the set on
the right in the claim. ∎

######  Lemma 17.

Let $\alpha z$ be a simple expression where $\hat{z}=z\in\Sigma$ (the
rightmost symbol is not starred). Then, $[\\![(z+1)\alpha]\\!]$ contains a
marking $N$ if, and only if, there exists markings $N^{\prime}\geq N$ and $M$,
and a set $S\subseteq[0,1[$ so that

  1. (1)

$\lvert S\rvert=\lvert\alpha z\rvert$

  2. (2)

$\mathit{abs}_{S}(M)\in\mathcal{L}\mathopen{}\mathclose{{}\left(\alpha
z}\right)$

  3. (3)

$M\longrightarrow_{d}N^{\prime}$ for $d=1-\max(S)$.

###### Proof.

Suppose markings $N,N^{\prime},M$, a set $S\subseteq[0,1[$ and
$d\in{\mathbb{R}}_{\geq 0}$ so that the conditions 1 to 3 are satisfied. Let
$S^{\prime}\overset{\text{\tiny def}}{=}\\{0\\}\cup\\{s+d\mid s\in
S\setminus\\{d\\}\\}$. Then, $\lvert S^{\prime}\rvert=\lvert S\rvert$ and
$\mathit{abs}_{S^{\prime}}(N^{\prime})\in\mathcal{L}\mathopen{}\mathclose{{}\left((z+1)\alpha}\right)$,
which witnesses that $N\in[\\![(z+1)\alpha]\\!]$.

Conversely, let $N\in[\\![(z+1)\alpha]\\!]$ be a non-empty marking. If
$\lvert\alpha\rvert=0$, then $N\in[\\![(z+1)]\\!]$ and so
$\mathit{abs}_{S}(N)\in\mathcal{L}\mathopen{}\mathclose{{}\left((z+1)}\right)$
for $S\overset{\text{\tiny def}}{=}{\it frac}(N)=\\{0\\}$. This means that
$M\longrightarrow_{1}N=(M+1)$ for a marking $M$ with
$\mathit{abs}_{S}(M)\in\mathcal{L}\mathopen{}\mathclose{{}\left(z}\right)=\mathcal{L}\mathopen{}\mathclose{{}\left(\alpha
z}\right)$.

If $\lvert\alpha\rvert>0$, pick some marking $N^{\prime}\geq N$ and set
$S^{\prime}$ so that $\mathit{abs}_{S^{\prime}}(N^{\prime})=(z+1)w$, for some
word $w\in\mathcal{L}\mathopen{}\mathclose{{}\left(\alpha}\right)$. Then we
must have that $\lvert S^{\prime}\rvert=\lvert(z+1)\alpha\rvert>1$ and so
$d\overset{\text{\tiny def}}{=}\min(S^{\prime}\setminus\\{0\\})$ exists. Let
$S\overset{\text{\tiny def}}{=}\\{s-d\mid s\in S^{\prime}\\}\cup\\{1-d\\}$ and
$M$ be the unique marking with $M\longrightarrow_{d}N^{\prime}$. Notice that
$1-d=\max(S)$. It follows that
$\mathit{abs}_{S}(M)=wz\in\mathcal{L}\mathopen{}\mathclose{{}\left(\alpha
z}\right)$. ∎

We will often use the following simple fact, which is a direct consequence of
Lemma 17.

######  Corollary 18.

$[\\![(z+1)\alpha]\\!]\subseteq\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![\alpha
z]\\!]}\right)$.

Finally, the following lemma will be the basis for our exploration algorithm.

######  Lemma 19.

Let $\alpha x_{0}^{*}$ be a simple expression with $\mathit{SAT}(\alpha
x_{0}^{*})=\alpha x_{0}^{*}$. Then
$\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![\alpha
x_{0}^{*}]\\!]}\right)=[\\![\alpha
x_{0}^{*}]\\!]\cup\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![(x_{0}+1)\alpha
x_{0}^{*}]\\!]}\right)$.

###### Proof.

For the right to left inclusion notice that $[\\![\alpha
x_{0}^{*}]\\!]\subseteq\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![\alpha
x_{0}^{*}]\\!]}\right)$ trivially holds. For the rest, we have
$[\\![(x_{0}+1)\alpha
x_{0}^{*}]\\!]\subseteq\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![\alpha
x_{0}^{*}]\\!]}\right)$ by Corollary 18, and therefore
$\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![(x_{0}+1)\alpha
x_{0}^{*}]\\!]}\right)\leavevmode\nobreak\ \subseteq\leavevmode\nobreak\
\mathit{Cover}\mathopen{}\mathclose{{}\left(\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![\alpha
x_{0}^{*}]\\!]}\right)}\right)=\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![\alpha
x_{0}^{*}]\\!]}\right)$. For the left to right inclusion, we equivalently show
that

$\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![\alpha
x_{0}^{*}]\\!]}\right)\setminus[\\![\alpha
x_{0}^{*}]\\!]\subseteq\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![(x_{0}+1)\alpha
x_{0}^{*}]\\!]}\right)$ (1)

Using the assumption that $\mathit{SAT}(\alpha x_{0}^{*})=\alpha x_{0}^{*}$,
the set on the left contains everything coverable from $[\\![\alpha
x_{0}^{*}]\\!]$ by a sequence that starts with a (short) time step. It can
therefore be written as

$\mathit{Cover}\mathopen{}\mathclose{{}\left(\\{N_{1}\mid\exists
N_{0}\in[\\![\alpha x_{0}^{*}]\\!]\land N_{0}\longrightarrow_{d}N_{1}\land
0<d<1-\max(frac(N_{0}))\\}}\right).$

By Lemma 16 and because $[\\![\emptyset\alpha]\\!]\subseteq[\\![X\alpha]\\!]$
for all $X\in\Sigma$ and $\alpha\in\Sigma^{*}$, we conclude that indeed,
$\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![\alpha
x_{0}^{*}]\\!]}\right)\setminus[\\![\alpha x_{0}^{*}]\\!]\leavevmode\nobreak\
\subseteq\leavevmode\nobreak\
\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![\emptyset\alpha
x_{0}^{*}]\\!]}\right)\subseteq\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![(x_{0}+1)\alpha
x_{0}^{*}]\\!]}\right)$. ∎

###  4.2. Acceleration

We propose an acceleration procedure based on unfolding expressions according
to Lemma 19 (interleaved with saturation steps to guarantee its premise) and
introducing new Kleene stars to keep the length of intermediate expressions
bounded. This procedure (depicted in Algorithm 1), is used to characterize an
initial subset of the coverability set.

1:a simple expression $S_{0}=x_{1}x_{0}^{*}$ (of length 2 and with last symbol
starred)

2:simple expressions $S_{1},S_{i}$ and $R$, of lengths 2, 4, and 2,
respectively.

3:$S_{1}\overset{\text{\tiny
def}}{=}x_{1}^{1}(x_{0}^{1})^{*}=\mathit{SAT}(x_{1}x_{0}^{*})$

4:$S_{2}\overset{\text{\tiny
def}}{=}x_{2}^{2}x_{1}^{2}(x_{0}^{2})^{*}=\mathit{SAT}((x_{0}^{1}+1)S_{1})$

5:$S_{3}\overset{\text{\tiny
def}}{=}x_{3}^{3}x_{2}^{3}x_{1}^{3}(x_{0}^{3})^{*}=\mathit{SAT}((x_{0}^{2}+1)S_{2})$

6:$i\leftarrow 3$

7:repeat

8:
$x_{i+1}^{i+1}x_{i}^{i+1}x_{i-1}^{i+1}x_{1}^{i+1}(x_{0}^{i+1})^{*}\overset{\text{\tiny
def}}{=}\mathit{SAT}((x_{0}^{i}+1)S_{i})$

9: $S_{i+1}\overset{\text{\tiny
def}}{=}x_{i+1}^{i+1}(x_{i}^{i+1})^{*}x_{1}^{i+1}(x_{0}^{i+1})^{*}$

10: $i\leftarrow i+1$

11:until $S_{i}=S_{i-1}$

12:$R\overset{\text{\tiny def}}{=}(x_{1}^{i}+1)(x_{i-1}^{i})^{*}$

13:return $S_{1},S_{i},R$

Algorithm 1 Accelerate pt$x_{0}^{*}$$x_{1}$ start $(x_{0}^{1})^{*}$$x_{1}^{1}$
$S_{1}=\mathit{SAT}(x_{1}x_{0}^{*})$
$(x_{0}^{1})^{*}$$x_{1}^{1}$$(x_{0}^{1}+1)$ $(x_{0}^{1}+1)S_{1}$
$(x_{0}^{2})^{*}$$x_{1}^{2}$$x_{2}^{2}$
$S_{2}=\mathit{SAT}((x_{0}^{1}+1)S_{1})$
$(x_{0}^{2})^{*}$$x_{1}^{2}$$x_{2}^{2}$$(x_{0}^{2}+1)$ $(x_{0}^{2}+1)S_{2}$
$(x_{0}^{3})^{*}$$x_{1}^{3}$$x_{2}^{3}$$x_{3}^{3}$
$S_{3}=\mathit{SAT}((x_{0}^{2}+1)S_{2})$
$(x_{0}^{3})^{*}$$x_{1}^{3}$$x_{2}^{3}$$x_{3}^{3}$$(x_{0}^{3}+1)$
$(x_{0}^{3}+1)S_{3}$
$(x_{0}^{4})^{*}$$x_{1}^{4}$$x_{2}^{4}$$x_{3}^{4}$$x_{4}^{4}$
$\mathit{SAT}((x_{0}^{3}+1)S_{3})$
$(x_{0}^{4})^{*}$$x_{1}^{4}$$(x_{3}^{4})^{*}$$x_{4}^{4}$ $S_{4}$
$(x_{0}^{4})^{*}$$x_{1}^{4}$$(x_{3}^{4})^{*}$$x_{4}^{4}$$(x_{0}^{4}+1)$
$(x_{0}^{4}+1)S_{4}$
$(x_{0}^{5})^{*}$$x_{1}^{5}$$(x_{3}^{5})^{*}$$x_{4}^{5}$$x_{5}^{5}$
$\mathit{SAT}((x_{0}^{4}+1)S_{4})$
$(x_{0}^{5})^{*}$$x_{1}^{5}$$(x_{4}^{5})^{*}$$x_{5}^{5}$ $S_{5}$
$\vdots$$\vdots$$\vdots$$\vdots$$\vdots$ $\vdots$ line 1: 2: 3: 6: 7: 6: 7:
Figure 2. A Run of Algorithm 1 (initial steps). The column on the left
indicates the line of code, the middle depicts the current expression and the
column on the right recalls its origin. Gray bars indicate that the respective
symbols are equal. Arrows denote (set) inclusion between symbols. The gray
vertical arrows indicate inclusions due to saturation (Lemma 13), as claimed
in item 1 of Lemma 20. Red and blue arrows indicate derived inclusions (as
stated in Lemma 20).

Given a length-2 simple expression $S_{0}$ where the rightmost symbol is
starred, the algorithm will first saturate (Definition 14, in line 1), and
then alternatingly rotate a copy of the rightmost symbol (Lemma 17), and
saturate the result (see lines 2, 3, 6). Since each such round extends the
length of the expression by one, we additionally collapse them (in line 7) by
adding an extra Kleene star to the symbol at the second position. The crucial
observation for the correctness of this procedure is that the subsumption step
in line 7 does not change the cover sets of the respective expressions.

Observe that Algorithm 1 is well defined because the $\mathit{SAT}(S_{i})$ are
computable by Lemma 13. Termination is guaranteed by the following simple
observation.

######  Lemma 20.

Let $x_{j}^{i}\in\Sigma$ be the symbols computed by Algorithm 1. Then

  1. (1)

$x_{j}^{i+1}\supseteq x_{j}^{i}$, for all $i>j\geq 0$.

  2. (2)

$x_{i}^{i}\supseteq x_{i-1}^{i-1}$ and $x_{i}^{i+1}\supseteq x_{i-1}^{i}$, for
all $i\geq 3$.

###### Proof.

The first item is guaranteed by Point 2 of Lemma 13. In particular this means
that $x_{0}^{i+1}\supseteq x_{0}^{i}$ and therefore that
$(x_{0}^{i+1}+1)\supseteq(x_{0}^{i}+1)$ for all $i\geq 0$ (indicated as red
arrows in Figure 2). The second item now follows from this observation by
Lemma 15. ∎

######  Lemma 21 (Termination).

Algorithm 1 terminates with $i\leq 4\cdot\lvert
P\rvert\cdot(c_{\mathit{max}}+1)$.

###### Proof.

From Lemma 20 we deduce that for all $i\geq 2$, the expression $S_{i+1}$ is
point-wise larger than or equal to $S_{i}$ with respect to the subset ordering
on symbols. The claim now follows from the observation that all expressions
$S_{i\geq 3}$ have length $4$ and that every symbol $x_{i}\in\Sigma$ can only
increase at most $\lvert P\rvert\cdot(c_{\mathit{max}}+1)$ times. ∎

######  Lemma 22 (Correctness).

Suppose that $S_{1},S_{\ell},R$ be the expressions computed by Algorithm 1
applied to the simple expression $x_{1}x_{0}^{*}$. Then
$\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![x_{1}x_{0}^{*}]\\!]}\right)=[\\![S_{1}]\\!]\cup[\\![S_{\ell}]\\!]\cup\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![R]\\!]}\right)$.

###### Proof.

Let $S_{1},\ldots S_{\ell}$ denote the expressions defined in lines 1,2,3, and
7 of the algorithm. That is, $\ell$ is the least index $i$ such that
$S_{i+1}=S_{i}$. We define a sequence $E_{i}$ of expressions inductively,
starting with $E_{1}\overset{\text{\tiny def}}{=}S_{1}$ and if
$E_{i}=e_{i}^{i}e_{i-1}^{i}\dots e_{0}^{i}$, we let
$E_{i+1}\overset{\text{\tiny
def}}{=}e_{i+1}^{i+1}e_{i}^{i+1}e_{i-1}^{i+1}\dots
e_{0}^{i+1}\overset{\text{\tiny
def}}{=}\mathit{SAT}((\hat{e}_{0}^{i}+1)E_{i})$. Here, the superscript
indicates the position of a symbol and not iteration. This is the sequence of
expressions resulting from unfolding Lemma 19, interleaved with saturation
steps, just in line 6 of the algorithm. That is, the expressions $E_{i}$ are
_not_ collapsed (line 7) and instead grow in length with $i$. Still,
$E_{1}=S_{1}$, $E_{2}=S_{2}$ and $E_{2}=S_{3}$, but $E_{4}\neq S_{4}$, because
the latter is the result of applying the subsumption step of line $7$ in our
algorithm. Notice that
$\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![x_{1}x_{0}^{*}]\\!]}\right)=\mathopen{}\mathclose{{}\left(\bigcup_{k-1\geq
i\geq
1}[\\![E_{i}]\\!]}\right)\cup\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![E_{k}]\\!]}\right)$
holds for all $k\in\mathbb{N}$. We will use that

$\bigcup_{i\geq 2}[\\![E_{i}]\\!]=\bigcup_{i\geq
2}[\\![S_{i}]\\!]=[\\![S_{\ell}]\\!].$ (2)

We start by observing that for all $i,j\in\mathbb{N}$ it holds that
$e_{j}^{i}=x_{j}^{i}$. For $i\leq 3$ this holds trivially by definition of
$E_{i}=S_{i}$. For larger $i$, this can be seen by induction using Lemma 13.
Towards the first equality in Equation 2, let $S_{i}^{j}$ be the expression
resulting from $S_{i}=x_{i}^{i}({x_{i-1}^{i}})^{*}x_{1}^{i}({x_{0}^{i}})^{*}$
by unfolding the first star $j$ times. That is, $S_{i}^{j}\overset{\text{\tiny
def}}{=}x_{i}^{i}({x_{i-1}^{i}})^{(j)}x_{1}^{i}(x_{0}^{i})^{*}$, where the
superscript $(j)$ denotes $j$-fold concatenation. Clearly,
$[\\![S_{i}]\\!]=\bigcup_{j\geq 0}[\\![S_{i}^{j}]\\!]$ and so the
$\supseteq$-direction of the first equality in Equation 2 follows by

$\displaystyle[\\![S_{i}^{j}]\\!]=[\\![x_{i}^{i}({x_{i-1}^{i}})^{(j)}x_{1}^{i}(x_{0}^{i})^{*}]\\!]$
$\displaystyle\subseteq[\\![x_{i+j}^{i+j}\mathopen{}\mathclose{{}\left({x_{i+j-1}^{i+j}}{x_{i+j-2}^{i+j}}\ldots{x_{i}^{i+j}}}\right)x_{1}^{i+1}(x_{0}^{i+1})^{*}]\\!]$
$\displaystyle\subseteq[\\![x_{i+j}^{i+j}\mathopen{}\mathclose{{}\left({x_{i+j-1}^{i+j}}{x_{i+j-2}^{i+j}}\ldots{x_{i}^{i+j}}}\right)\mathopen{}\mathclose{{}\left({x_{i-1}^{i+j}}\ldots{x_{2}^{i+j}}}\right)x_{1}^{i+1}(x_{0}^{i+j})^{*}]\\!]$
$\displaystyle=[\\![E_{i+j}]\\!],$

where the first inclusion is due to Lemma 20. The same helps for the other
direction:

$[\\![E_{i}]\\!]=[\\![x_{i}^{i}x_{i-1}^{i}x_{i-2}^{i}\dots
x_{2}^{i}x_{1}^{i}x_{0}^{i}]\\!]\subseteq[\\![x_{i}^{i}{(x_{i-1}^{i})}^{(i-2)}x_{1}^{i}x_{0}^{i}]\\!]=[\\![S_{i}^{i-2}]\\!]=[\\![S_{i}]\\!],$
(3)

which completes the proof of the first equality in Equation 2. The second
equality holds because $[\\![S_{i}]\\!]\subseteq[\\![S_{i+1}]\\!]$ for all
$i\geq 2$, by Lemma 20, and by definition of $S_{\ell}=S_{\ell+1}$. As a next
step we show that

$\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![S_{\ell}]\\!]}\right)=[\\![S_{\ell}]\\!]\cup\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![R]\\!]}\right)$
(4)

First observe that
$[\\![R]\\!]=[\\![(x_{1}^{\ell}+1){(x_{\ell-1}^{\ell})}^{*}]\\!]=[\\![(x_{1}^{\ell}+1)x_{\ell}^{\ell}{(x_{\ell-1}^{\ell})}^{*}]\\!]$
and consequently,

$\displaystyle\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![R]\\!]}\right)$
$\displaystyle=\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![(x_{1}^{\ell}+1)x_{\ell}^{\ell}{(x_{\ell-1}^{\ell})}^{*}]\\!]}\right)$
$\displaystyle\subseteq\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![x_{\ell}^{\ell}{(x_{\ell-1}^{\ell})}^{*}x_{1}^{\ell}]\\!]}\right)$
$\displaystyle\subseteq\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![x_{\ell}^{\ell}{(x_{\ell-1}^{\ell})}^{*}x_{1}^{\ell}{(x_{0}^{\ell})}^{*}]\\!]}\right)=\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![S_{\ell}]\\!]}\right)$

where the first equation follows by Corollary 18 and the second because
$\mathcal{L}\mathopen{}\mathclose{{}\left(x_{\ell}^{\ell}{(x_{\ell-1}^{\ell})}^{*}x_{1}^{\ell}}\right)\subseteq\mathcal{L}\mathopen{}\mathclose{{}\left(x_{\ell}^{\ell}{(x_{\ell-1}^{\ell})}^{*}x_{1}^{\ell}{(x_{0}^{\ell})}^{*}}\right)$.
For the left to right inclusion in Equation 4, consider a marking
$M\in\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![S_{\ell}]\\!]}\right)\setminus[\\![S_{\ell}]\\!]$.
We show that
$M\in\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![R]\\!]}\right)$. Recall
that $\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![S_{\ell}]\\!]}\right)$
consists of all those markings $M$ so that there exists a finite path

$M_{0}\xrightarrow{*}_{\textit{Disc}}M^{\prime}_{0}\xrightarrow{d_{1}}_{\textit{Time}}M_{1}\xrightarrow{*}_{\textit{Disc}}M^{\prime}_{1}\xrightarrow{d_{2}}_{\textit{Time}}M_{2}\dots
M^{\prime}_{k-1}\xrightarrow{*}_{\textit{Disc}}M_{k}$

alternating between timed and (sequences of) discrete transition steps, with
$M_{0}\in[\\![S_{\ell}]\\!]$, $M_{k}\geq M$ and all $d_{i}\leq\max({\it
frac}(M^{\prime}_{i}))$.

By our choice of $M$, there must be a first expression in the sequence which
is not a member of $[\\![S_{\ell}]\\!]$. Since
$[\\![\mathit{SAT}(S_{\ell})]\\!]=[\\![S_{\ell}]\\!]$, we can assume an index
$i>0$ so that $M_{i}\notin[\\![S_{\ell}]\\!]$ but
$M^{\prime}_{i-1}\in[\\![S_{\ell}]\\!]$ that is, the step that takes us out of
$[\\![S_{\ell}]\\!]$ is a timed step.

Because $[\\![S_{\ell}]\\!]=\bigcup_{i\geq 2}[\\![S_{i}]\\!]$, it must hold
that
$M^{\prime}_{i-1}\in[\\![S_{j}]\\!]=[\\![x_{j}^{j}(x_{j-1}^{j})^{*}x_{1}^{j}(x_{0}^{j})^{*}]\\!]$
for some index $j\geq 2$. We claim that it already holds that

$M^{\prime}_{i-1}\in[\\![x_{j}^{j}{(x_{j-1}^{j})}^{*}x_{1}^{j}]\\!].$ (5)

Suppose not. If $d_{i}<\max({\it frac}(M^{\prime}_{i-1}))$ then
$M_{i}\in[\\![\emptyset S_{j}]\\!]\subseteq[\\![S_{j}]\\!]$ by Lemma 16,
contradiction. Otherwise, if $d_{i}=\max({\it frac}(M^{\prime}_{i-1}))$,
notice that every abstraction
$\mathit{abs}_{S}(M^{\prime}_{i-1})\in\mathcal{L}\mathopen{}\mathclose{{}\left(S_{j}}\right)$
must have $\lvert S\rvert=4$. So by Lemma 17,
$M_{i}\in[\\![(x_{0}^{j}+1)S_{j}]\\!]$. But then again

$[\\![(x_{0}^{j}+1)S_{j}]\\!]\subseteq[\\![\mathit{SAT}((x_{0}^{j}+1)S_{j})]\\!]\subseteq[\\![S_{j+1}]\\!],$
(6)

contradicting our assumption that $M_{i}\notin[\\![S_{\ell}]\\!]$. Therefore
Equation 5 holds. By Lemma 17 we derive that
$M_{i}\in[\\![(x_{1}^{j}+1)x_{j}^{j}(x_{j-1}^{j})^{*}]\\!]=[\\![(x_{1}^{j}+1)(x_{j-1}^{j})^{*}]\\!]\subseteq[\\![(x_{1}^{\ell}+1)(x_{\ell-1}^{\ell})^{*}]\\!]=[\\![R]\\!]$.
This concludes the proof of Equation 4.

Notice that by Lemma 19 we have that

$\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![x_{1}x_{0}^{*}]\\!]}\right)=[\\![\mathit{SAT}(x_{1}x_{0}^{*})]\\!]\cup\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![\mathit{SAT}(x_{1}x_{0}^{*})]\\!]}\right)=[\\![S_{1}]\\!]\cup\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![S_{1}]\\!]}\right).$
(7)

Analogously, we get for every $i\geq 1$ that

$\displaystyle\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![E_{i}]\\!]}\right)=[\\![\mathit{SAT}(E_{i})]\\!]\cup\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![\mathit{SAT}((x^{i}_{0}+1)E_{i})]\\!]}\right)=[\\![E_{i}]\\!]\cup\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![E_{i+1}]\\!]}\right)$
(8)

This used Lemma 19 and the fact that $\mathit{SAT}(E_{i})=E_{i}$ by
construction. Using Equation 8 and that
$[\\![E_{i}]\\!]\subseteq[\\![E_{i+1}]\\!]$ for $i\geq 2$, we deduce

$\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![S_{1}]\\!]}\right)=\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![E_{1}]\\!]}\right)=[\\![E_{1}]\\!]\cup\mathopen{}\mathclose{{}\left(\bigcup_{i\geq
2}\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![E_{i}]\\!]}\right)}\right).$
(9)

Finally we can conclude the desired result as follows.

$\displaystyle\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![x_{1}x_{0}^{*}]\\!]}\right)$
$\displaystyle\overset{\text{\tiny(\ref{eq:acc:EisSunr1})}}{=}[\\![S_{1}]\\!]\cup\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![S_{1}]\\!]}\right)\overset{\text{\tiny(\ref{eq:acc:3})}}{=}[\\![S_{1}]\\!]\cup\mathit{Cover}\mathopen{}\mathclose{{}\left(\bigcup_{i\geq
2}[\\![E_{i}]\\!]}\right)$
$\displaystyle\overset{\text{\tiny(\ref{eq:acc:EisS})}}{=}[\\![S_{1}]\\!]\cup\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![S_{\ell}]\\!]}\right)$
$\displaystyle\overset{\text{\tiny(\ref{eq:acc:Rconnection})}}{=}[\\![S_{1}]\\!]\cup[\\![S_{\ell}]\\!]\cup\mathit{Cover}\mathopen{}\mathclose{{}\left([\\![R]\\!]}\right)\qed$

###  4.3. Main Result

The following theorem summarizes our main claims regarding the $\exists$COVER
problem.

######  Theorem 23.

Consider an instance of $\exists$COVER with ${\cal
N}=(P,T,\mathit{Var},G,\mathit{Pre},\mathit{Post})$ a non-consuming TPN where
$c_{\mathit{max}}$ is the largest constant appearing in the transition guards
$G$ encoded in unary, and let $p$ be an initial place and $t$ be a transition.

  1. (1)

The number of different simple expressions of length $m$ is
$B(m)\overset{\text{\tiny def}}{=}2^{(\lvert
P\rvert\cdot(c_{\mathit{max}}+2)\cdot m)+m}$.

  2. (2)

It is possible to compute a symbolic representation of the set of markings
coverable from some marking in the initial set $\mathbb{N}\cdot\\{(p,{0})\\}$,
as a finite set of simple expressions. I.e., one can compute simple
expressions $S_{1},\dots,S_{\ell}$ s.t. $\bigcup_{1\leq
i\leq\ell}[\\![S_{i}]\\!]=\mathit{Cover}\mathopen{}\mathclose{{}\left(\mathbb{N}\cdot\\{(p,{0})\\}}\right)$
and where $\ell\leq 3\cdot B(2)$. Each of the $S_{i}$ has length either $2$ or
$4$.

  3. (3)

Checking if there exists
$M\in\mathit{Cover}\mathopen{}\mathclose{{}\left(\mathbb{N}\cdot\\{(p,0)\\}}\right)$
with $M\longrightarrow_{t}$ can be done in $\mathcal{O}(\lvert P\rvert\cdot
c_{\mathit{max}})$ deterministic space.

###### Proof.

For Item 1 note that a simple expression is described by a word where some
symbols have a Kleene star. There are $\lvert\Sigma\rvert^{m}$ different words
of length $m$ and $2^{m}$ possibilities to attach stars to symbols. Since the
alphabet is $\Sigma\overset{\text{\tiny
def}}{=}2^{P\times[{c_{\mathit{max}}+1}]}$ and
$\lvert[{c_{\mathit{max}}+1}]\rvert=c_{\mathit{max}}+2$, the result follows.

Towards Item 2, we can assume w.l.o.g. that our TPN is non-consuming by Lemma
8, and thus the region abstraction introduced in Section 4.1 applies. In
particular, the initial set of markings $\mathbb{N}\cdot\\{(p,{0})\\}$ is
represented exactly by the expression $S_{0}\overset{\text{\tiny
def}}{=}\\{(p,0)\\}\emptyset^{*}$ where $\emptyset\in\Sigma$ is the symbol
corresponding to the empty set. That is, we have
$[\\![S_{0}]\\!]=\mathbb{N}\cdot\\{(p,{0})\\}$ and thus
$\mathit{Cover}([\\![S_{0}]\\!])=\mathit{Cover}(\mathbb{N}\cdot\\{(p,{0})\\})$.

The claimed expressions $S_{i}$ are the result of iterating Algorithm 1 until
a previously seen expression is revisited. Starting at $i=0$ and
$S_{0}\overset{\text{\tiny def}}{=}\\{(p,0)\\}\emptyset^{*}$, each round will
set $S_{i+1},S_{i+2}$ and $S_{i+3}$ to the result of applying Algorithm 1 to
$S_{i}$, and increment $i$ to $i+3$.

Notice that then all $S_{i}$ are simple expressions of length $2$ or $4$ and
that in particular, all expressions with index divisible by $3$ are of the
form $ab^{*}$ for $a,b\in\Sigma$. Therefore after at most $B(2)$ iterations,
an expression $S_{\ell}$ is revisited (with $\ell\leq 3B(2)$). Finally, an
induction using Lemma 22 provides that $\bigcup_{1\leq
i\leq\ell}[\\![S_{i}]\\!]=\mathit{Cover}\mathopen{}\mathclose{{}\left(\mathbb{N}\cdot\\{(p,{0})\\}}\right)$.

Towards Item 3, we modify the above algorithm for the $\exists$COVER problem
with the sliding window technique. The algorithm is the same as above where
instead of recording all the expressions $S_{1},\dots,S_{\ell}$, we only store
the most recent ones and uses them to decide whether the transition $t$ is
enabled. If the index $i$ reaches the maximal value of $3\cdot B(2)$ we return
unsuccessfully.

The bounded index counter uses $\mathcal{O}(\log(B(2)))$ space; Algorithm 1
uses space $\mathcal{O}(\log(B(5)))$ because it stores only simple expressions
of length $\leq 5$. The space required to store the three expressions
resulting from each application of Algorithm 1 is
$\mathcal{O}(3\cdot\log(B(4)))$. For every encountered simple expression we
can check in logarithmic space whether the transition $t$ is enabled by some
marking in its denotation. Altogether the space used by our new algorithm is
bounded by $\mathcal{O}(\log(B(5)))$. By Item 1, this is
$\mathcal{O}(|P|\cdot(c_{\mathit{max}}+2))=\mathcal{O}(\lvert P\rvert\cdot
c_{\mathit{max}})$. ∎

######  Corollary 24.

The $\exists$COVER problem for TPN is $\mathsf{PSPACE}$-complete.

###### Proof.

The $\mathsf{PSPACE}$ lower bound was shown in Theorem 7. The upper bound
follows from Lemma 8 and Item 3 of Theorem 23. ∎

##  5\. Conclusion and Future Work

We have shown that _Existential Coverability_ (and its dual of universal
safety) is $\mathsf{PSPACE}$-complete for TPN with one real-valued clock per
token. This implies the same complexity for checking safety of arbitrarily
large timed networks without a central controller. The absence of a central
controller makes a big difference, since the corresponding problem _with_ a
central controller is complete for $F_{\omega^{\omega^{\omega}}}$ [12].

It remains an open question whether these positive results for the controller-
less case can be generalized to multiple real-valued clocks per token. In the
case _with_ a controller, safety becomes undecidable already for two clocks
per token [2].

Another question is whether our results can be extended to more general
versions of timed Petri nets. In our version, clock values are either
inherited, advanced as time passes, or reset to zero. However, other versions
of TPN allow the creation of output-tokens with new non-deterministically
chosen non-zero clock values, e.g., the timed Petri nets of [3, 4] and the
read-arc timed Petri nets of [8].

## References

  * [1] Parosh Aziz Abdulla, Karlis Čerāns, Bengt Jonsson, and Yih-Kuen Tsay.  Algorithmic analysis of programs with well quasi-ordered domains.  Information and Computation, 160(1–2):109–127, 2000.
  * [2] Parosh Aziz Abdulla, Johann Deneux, and Pritha Mahata.  Multi-clock timed networks.  In Annual IEEE Symposium on Logic in Computer Science (LICS), pages 345–354, 2004.
  * [3] Parosh Aziz Abdulla, Pritha Mahata, and Richard Mayr.  Dense-timed Petri nets: Checking Zenoness, token liveness and boundedness.  Logical Methods in Computer Science, 3(1), 2007.
  * [4] Parosh Aziz Abdulla and Aletta Nylén.  Timed Petri nets and BQOs.  In International Conference on Application and Theory of Petri Nets (ICATPN), volume 2075 of LNCS, pages 53–70. Springer, 2001.
  * [5] R. Alur and D. L. Dill.  A theory of timed automata.  Theoretical Computer Science, 126(2):183–235, 1994.
  * [6] Benjamin Aminof, Sasha Rubin, Florian Zuleger, and Francesco Spegni.  Liveness of parameterized timed networks.  In International Colloquium on Automata, Languages and Programming (ICALP), volume 9135 of LNCS, 2015.
  * [7] Rémi Bonnet, Alain Finkel, Serge Haddad, and Fernando Rosa-Velardo.  Comparing Petri data nets and timed Petri nets.  Technical Report LSV-10-23, LSV Cachan, 2010.
  * [8] Patricia Bouyer, Serge Haddad, and Pierre-Alain Reynier.  Timed Petri nets and timed automata: On the discriminating power of Zeno sequences.  In International Colloquium on Automata, Languages and Programming (ICALP), pages 420–431. Springer, 2006.
  * [9] David de Frutos Escrig, Valentín Valero Ruiz, and Olga Marroquín Alonso.  Decidability of properties of timed-arc Petri nets.  In International Conference on Application and Theory of Petri Nets (ICATPN), volume 1825 of LNCS, pages 187–206. Springer, 2000.
  * [10] Alain Finkel and Philippe Schnoebelen.  Well-structured transition systems everywhere!  Theoretical Computer Science, 256(1–2):63–92, 2001.
  * [11] Eric Goles, Pedro Montealegre, Ville Salo, and Ilkka Törmä.  PSPACE-completeness of majority automata networks.  Theoretical Computer Science, 609(1):118 – 128, 2016.
  * [12] Serge Haddad, Sylvain Schmitz, and Philippe Schnoebelen.  The ordinal recursive complexity of timed-arc Petri nets, data nets, and other enriched nets.  In Annual IEEE Symposium on Logic in Computer Science (LICS), pages 355–364, 2012.
  * [13] Lasse Jacobsen, Morten Jacobsen, Mikael H. Møller, and Jiří Srba.  Verification of timed-arc Petri nets.  In International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM), volume 6543 of LNCS, pages 46–72, 2011.
  * [14] Ranko Lazić, Tom Newcomb, Joël Ouaknine, A.W. Roscoe, and James Worrell.  Nets with tokens which carry data.  Fundamenta Informaticae, 88(3):251–274, 2008.
  * [15] Valentin Valero Ruiz, Fernando Cuartero Gomez, and David de Frutos Escrig.  On non-decidability of reachability for timed-arc Petri nets.  In International Workshop on Petri Nets and Performance Models. IEEE Computer Society, 1999.
  * [16] Jiří Srba.  Timed-arc Petri nets vs. networks of timed automata.  In International Conference on Application and Theory of Petri Nets (ICATPN), volume 3536 of LNCS, pages 385–402. Springer, 2005.

##  Appendix A Proof of Lemma 13

######  Lemma 25.

For every non-consuming TPN $\mathcal{N}$ there are polynomial time computable
functions $f:\Sigma\times\Sigma\times\Sigma\to\Sigma$ and
$g:\Sigma\times\Sigma\times\Sigma\to\Sigma$ with the following properties.

  1. (1)

$f$ and $g$ are monotone (w.r.t. subset ordering) in each argument.

  2. (2)

$f(\alpha,\beta,x)\supseteq x$ and $g(\alpha,\beta,x)\supseteq x$ for all
$\alpha,\beta,x\in\Sigma$.

  3. (3)

For every word $w=x_{0}x_{1}\dots x_{k}$ over $\Sigma$,
$\alpha\overset{\text{\tiny def}}{=}x_{0}$ and $\beta\overset{\text{\tiny
def}}{=}\bigcup_{i>0}x_{i}$, and
$w^{\prime}\overset{\text{\tiny
def}}{=}f(\alpha,\beta,x_{0})g(\alpha,\beta,x_{1})\dots g(\alpha,\beta,x_{k})$
we have $[\\![w^{\prime}]\\!]=\\{M^{\prime\prime}\mid\exists
M\in[\\![w]\\!]\land M\xrightarrow{*}_{\textit{Disc}}M^{\prime}\geq
M^{\prime\prime}\\}$.

###### Proof.

(Sketch). It suffices to show the existence of such functions $f_{t}$ and
$g_{t}$ for individual transitions $t\in T$ and $\longrightarrow_{t}$ instead
of $\xrightarrow{*}_{\textit{Disc}}$. The functions $f$ and $g$ can then be
obtained by iterated applications of $f_{t}$ and $g_{t}$ (for all transitions
$t$) until convergence. (In addition to expanding $x$, the results of each
application $f_{t}$ and $g_{t}$ are also added to $\alpha$ and $\beta$,
respectively.) This works, because the functions $f_{t}$ and $g_{t}$ are
monotone and operate on the finite domain/range $\Sigma$. Since we have a
polynomial number of transitions, and each symbol in $\Sigma$ can increase (by
strict subset ordering) at most $\lvert P\rvert\cdot(c_{\mathit{max}}+1)$
times, the number of iterations is polynomial. Moreover, the properties of
Item 1, Item 2 and Item 3 carry over directly from $f_{t}$ and $g_{t}$ to $f$
and $g$, respectively.

Now we consider the definitions and properties of the functions $f_{t}$ and
$g_{t}$ for a particular transition $t$. Given a variable evaluation
$\pi:\mathit{Var}\to{\mathbb{R}}_{\geq 0}$, we define the functions $\pi_{0}$
and $\pi_{>0}$ from sets over $(P\times\mathit{Var})$ to sets over
$(P\times\mathbb{N})$ as follows. Intuitively, they cover the parts of the
assignment $\pi$ with zero/nonzero fractional values, respectively. Let
$\pi_{0}(S)\overset{\text{\tiny def}}{=}\\{(p,c)\,|\,(p,y)\in S\ \wedge\
\pi(y)=c\in\mathbb{N}\\}$ and $\pi_{>0}(S)\overset{\text{\tiny
def}}{=}\\{(p,c)\,|\,(p,y)\in S\ \wedge\ \lfloor\pi(y)\rfloor=c\ \wedge\ {\it
frac}(\pi(y))>0\\}$. The definitions are lifted to multisets in the
straightforward way.

Now let $t$ be a transition. We say that $(\alpha,\beta)$ enables $t$ iff
$\exists\pi:\mathit{Var}\to{\mathbb{R}}_{\geq 0}$ such that $\pi(y)\in
G(t)(y)$ for all variables $y$ and $\pi_{0}(\mathit{Pre}(t))\subseteq\alpha$
and $\pi_{>0}(\mathit{Pre}(t))\subseteq\beta$. Thus if
$\mathit{abs}(M)=x_{0}x_{1}\dots x_{n}$ then $M$ enables $t$ iff
$(x_{0},\bigcup_{i>0}x_{i})$ enables $t$, since all transition guards in
$G(t)$ are intervals bounded by integers (i.e., $t$ cannot distinguish between
different nonzero fractional values). Moreover, enabledness can be checked in
polynomial time (choose integers for the part in $\alpha$ and rationals with
fractional part $1/2$ for the part in $\beta$).

In the case where $(\alpha,\beta)$ does not enable $t$ we just let
$g_{t}(\alpha,\beta,x)\overset{\text{\tiny def}}{=}x$ and
$f_{t}(\alpha,\beta,x)\overset{\text{\tiny def}}{=}x$. The conditions above
are trivially satisfied in this case.

In the case where $(\alpha,\beta)$ enables $t$, let
$g_{t}(\alpha,\beta,x)\overset{\text{\tiny def}}{=}x\cup\gamma$ where $\gamma$
is defined as follows. We have $(p,c)\in\gamma$ iff there is a
$(p,y)\in\mathit{Post}(t)$ and $(q,y)\in\mathit{Pre}(t)$ such that $(q,c)\in
x$. Similarly, let $f_{t}(\alpha,\beta,x)\overset{\text{\tiny
def}}{=}x\cup\gamma$ where $\gamma$ is defined as follows. We have
$(p,c)\in\gamma$ iff either (1) there is a $(p,y)\in\mathit{Post}(t)$ and
$(q,y)\in\mathit{Pre}(t)$ such that $(q,c)\in x$, or (2) $c=0$ and there is a
$(p,0)\in\mathit{Post}(t)$. All these conditions can be checked in polynomial
time. Item 1 and Item 2 follow directly from the definition.

Towards Item 3, we show
$[\\![w^{\prime}]\\!]\supseteq\\{M^{\prime\prime}\mid\exists
M\in[\\![w]\\!]\land M\longrightarrow_{t}M^{\prime}\geq M^{\prime\prime}\\}$.
(The proof of the reverse inclusion $\subseteq$ is similar.) Let
$w=x_{0}x_{1}\dots x_{k}$, $\alpha\overset{\text{\tiny def}}{=}x_{0}$,
$\beta\overset{\text{\tiny def}}{=}\bigcup_{i>0}x_{i}$ such that
$(\alpha,\beta)$ enables $t$ and $w^{\prime}\overset{\text{\tiny
def}}{=}f_{t}(\alpha,\beta,x_{0})g_{t}(\alpha,\beta,x_{1})\dots
g_{t}(\alpha,\beta,x_{k})$. If $M\in[\\![w]\\!]$ and
$M\longrightarrow_{t}M^{\prime}$ then $M^{\prime}\geq M$ since $\mathcal{N}$
is non-consuming. We show that every additional token $(p,u)\in
M^{\prime}\ominus M$ is included in $[\\![w^{\prime}]\\!]$. (This implies the
inclusion above, since $M^{\prime}\ominus M\geq M^{\prime\prime}\ominus M$.)
For every additional token $(p,u)\in M^{\prime}\ominus M$ there are two cases.

  * •

Assume ${\it frac}(u)>0$. Then the token $(p,u)$ must have inherited its clock
value from some token $(q,u)\in M$ via a variable $y$ specified in the
Pre/Post of $t$ (since discrete transitions cannot create new fractional parts
of clock values). This case is covered by $\gamma$ in the definition of
$g_{t}$ above. In particular, if $(q,u)\in M$ was abstracted to $x_{i}$ in $w$
then $(p,u)\in M^{\prime}$ is abstracted to $g_{t}(\alpha,\beta,x_{i})$ in
$w^{\prime}$.

  * •

Assume ${\it frac}(u)=0$. Then there are two cases. In the first case the
token $(p,u)$ inherited its clock value from some token $(q,u)\in M$ via a
variable $y$ specified in the Pre/Post of $t$. This case is covered by part
(1) of $\gamma$ in the definition of $f_{t}$ above. In particular, $(q,u)\in
M$ was abstracted to $x_{0}$ in $w$, because ${\it frac}(u)=0$. Thus $(p,u)\in
M^{\prime}$ is abstracted to $f_{t}(\alpha,\beta,x_{0})$ in $w^{\prime}$. In
the second case the token $(p,u)$ got its clock value via a clock-reset to
zero. This case is covered by part (2) of $\gamma$ in the definition of
$f_{t}$ above. In particular, in this case we must have $u=0$, and $(p,0)\in
M^{\prime}$ was abstracted to $f_{t}(\alpha,\beta,x_{0})$ in $w^{\prime}$.

It follows that $\mathit{abs}(M^{\prime})\leq w^{\prime}$, i.e., by the
ordering on symbols in $\Sigma$, every letter in $\mathit{abs}(M^{\prime})$ is
smaller than the corresponding letter in $w^{\prime}$. Thus
$M^{\prime}\in[\\![w^{\prime}]\\!]$. Since $M^{\prime}\geq M^{\prime\prime}$
and $[\\![w^{\prime}]\\!]$ is downward closed, we also have
$M^{\prime\prime}\in[\\![w^{\prime}]\\!]$ as required. ∎

See 13

###### Proof.

Let $f$ and $g$ be the functions from Lemma 25, which immediately yields Item
1 and Item 2. Towards Item 3, consider all words $w$ in $\mathcal{L}(E)$ that
contain each starred symbol in $E$ at least once. (The other cases are
irrelevant for $[\\![E]\\!]$ since they are subsumed by monotonicity.) For
each such word $w$, the $\alpha,\beta$ derived from $w$ in Lemma 25 are the
same as the $\alpha,\beta$ derived from $E$ in Item 3. If $x_{i}$ in $E$
carries a star then $w$ contains a corresponding nonempty subsequence
$x_{i}\dots x_{i}$. We apply Lemma 25 to each such $w$ to obtain the
corresponding $w^{\prime}$. The word $w^{\prime}$ then contains the
corresponding subsequence $g(\alpha,\beta,x_{i})\dots g(\alpha,\beta,x_{i})$.
Let $E^{\prime}$ then be defined as in Item 3, i.e., by applying functions to
the symbols and keeping the stars at the same symbols as in $E$. By Lemma 25,
this is computable in polynomial time. We have
$\mathcal{L}(E^{\prime})=\bigcup_{w\in\mathcal{L}(E)}\\{w^{\prime}\\}$. Thus
$[\\![E^{\prime}]\\!]=\bigcup_{w\in\mathcal{L}(E)}[\\![w^{\prime}]\\!]=\bigcup_{w\in\mathcal{L}(E)}\\{M^{\prime\prime}\mid\exists
M\in[\\![w]\\!]\land M\xrightarrow{*}_{\textit{Disc}}M^{\prime}\geq
M^{\prime\prime}\\}=\\{M^{\prime\prime}\mid\exists M\in[\\![E]\\!]\land
M\xrightarrow{*}_{\textit{Disc}}M^{\prime}\geq M^{\prime\prime}\\}$ for Item 3
as required. ∎