---
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.
author:
- Parosh Aziz Abdulla
- Mohamed Faouzi Atig
- Radu Ciobanu
- Richard Mayr
- Patrick Totzke
bibliography:
- 'main.bib'
title: 'Universal Safety for Timed Petri Nets is PSPACE-complete'
---

Introduction {#sec:intro}
============

##### Background.

Timed-arc Petri nets (TPN) [@AA2001; @S2005; @AMM07; @BHR2006; @JJMS2011] 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 [@RVCE1999], Coverability is decidable using the well-quasi ordering approach of [@ACJT2000; @FS2001] and complete for the hyper-Ackermannian complexity class $F_{\omega^{\omega^\omega}}$ [@HSS2012]. With respect to Coverability, TPN are equivalent [@BFHR2010] to (linearly ordered) data nets [@LNORW2008].

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{\tinydef}}{=}}}m\cdot\{(p,{\boldsymbol{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 [@ADM2004] 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}}$ [@HSS2012] (and even undecidable for $>1$ clocks per token [@ADM2004]).

Aminof et. al. [@ARZS2015] 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 [@ADM2004] 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 [@AD:1994], 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 [@AMM07]. 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.

Timed Petri Nets
================

We use ${{\mathbb N}}$ and ${{\mathbb R}_{\geq 0}}$ to denote the sets of nonnegative integers and reals, respectively. For $n\in{{\mathbb N}}$ we write ${[{n}]}$ for the set ${{\mathopen{}\mathclose\bgroup\originalleft}\{0,\ldots,n{\aftergroup\egroup\originalright}\}}$.

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\bgroup\originalleft}(R{\aftergroup\egroup\originalright})}\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 $\le$). The multiset union of $M,M'\in{{X}^\oplus}$ is $(M\oplus M')\in{{X}^\oplus}$ with $(M\oplus M')(\alpha){{\overset{\text{\tinydef}}{=}}}M(\alpha)+M'(\alpha)$ for all $\alpha\in X$. If $M\ge M'$ then the multiset difference $(M\ominus M')$ is the unique $M''\in{{X}^\oplus}$ with $M=M'\oplus M''$. We will use a monomial representation and write for example $(\alpha + \beta^3)$ for the multiset $(\alpha\mapsto1, \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{\tinydef}}{=}}}\{n\cdot M\mid n\in {\mathbb{N}}, M\in S\}$.

\[sec:model\] *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.

\[def:MTPN\] 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}}$.

\[ex-mtpn\] 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)$.

\(t) \[transition, label=above:[$t$]{},align=left\] [$0\le x \le 5$\
$1 < y \le 2$ ]{}; (p) \[above left=of t,place, label=left:[$p$]{}\] ; (q) \[below left=of t,place, label=left:[$q$]{}\] ; (r) \[above right=of t,place, label=right:[$r$]{}\] ; (s) \[below right=of t,place, label=right:[$s$]{}\] ;

\(p) edge node\[above right, pos=0.3\][$x^2$]{} (t); (q) edge node\[below right, pos=0.3\][$y$]{} (t); (t) edge node\[above\][$y^3$]{} (r); (t) edge node\[above\][$0$]{} (s);

The transition $t$ consumes two tokens from place $p$, both of which have the same clock value $x$ (where $0 \le x \le 5$) and one token from place $q$ with clock value $y$ (where $1 < y \le 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$.

\[def:mtpn:dsteps\] 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}}$, $$\begin{aligned}
        \pi({\mathit{Pre}}(t))(p,c){{\overset{\text{\tinydef}}{=}}}\sum_{\pi(v)=c} {\mathit{Pre}}(t)(p,v)
        \qquad
        \text{and}
        \qquad
        \pi({\mathit{Post}}(t))(p,c){{\overset{\text{\tinydef}}{=}}}\sum_{\pi(v)={c}} {\mathit{Post}}(t)(p,{v}).
    \end{aligned}$$ 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))\le M$. In this case, there is a discrete step $M{\longrightarrow_{t}}M'$ from marking $M$ to $M'$, defined as $
        M' = M \ominus \pi({\mathit{Pre}}(t)) \oplus \pi({\mathit{Post}}(t)).
        $

\[def:mtpn:tsteps\] Let $M$ be a marking and $d\in {{\mathbb R}_{\geq 0}}$. There is a time step $M{\longrightarrow_{d}}M'$ to the marking $M'$ with $M'(p,{c}){{\overset{\text{\tinydef}}{=}}}M(p,{c}-{d})$ for ${c}\ge{d}$, and $M'(p,{c}){{\overset{\text{\tinydef}}{=}}}0$, otherwise. We also refer to $M'$ 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\bgroup\originalleft}(M{\aftergroup\egroup\originalright})}$ denotes the set of markings $M'$ for which there is an $M''\ge M'$ with $M{\xrightarrow{*}}M''$.

We are interested in the *existential coverability problem* ([$\exists$COVER ]{} for short), as follows.

[ ]{}

We show that this problem is [$\mathsf{PSPACE}$]{}-complete. Both lower and upper bound will be shown (w.l.o.g., see \[lem:mtpn:wlog\]) for the syntactic subclass of *non-consuming* TPN, defined as follows.

\[def:nonconsuming\] 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) \le 1$, and 2) ${\mathit{Pre}}(t) \le {\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 \[def:nonconsuming\] implies that for each discrete step $M{\longrightarrow_{t}}M'$ we have $M' \ge 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}})$.

Lower Bound {#sec:lowerbound}
===========

[$\mathsf{PSPACE}$]{}-hardness of [$\exists$COVER ]{}does not follow directly from the [$\mathsf{PSPACE}$]{}-completeness of the reachability problem in timed automata of [@AD:1994]. 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 [@GMST2016].

A depth-1 monotone Boolean circuit is a function $F:\{0,1\}^n \to \{0,1\}^n$ represented by $n$ constraints: For every $0\le i < n$ there is a constraint of the form $i'=j \otimes k,$ where $0\le 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 ${\boldsymbol{v}}\in\{0,1\}^n$, the function $F$ then satisfies $F({\boldsymbol{v}})[i]{{\overset{\text{\tinydef}}{=}}}{\boldsymbol{v}}[j]\otimes {\boldsymbol{v}}[k]$. It is [$\mathsf{PSPACE}$]{}-complete to check whether for a given vector ${\boldsymbol{v}}\in\{0,1\}^n$ there exists a number $m\in{\mathbb{N}}$ such that $F^m({\boldsymbol{v}})[0]=1$.

Towards a lower bound for [$\exists$COVER ]{} (\[thm:LB\]) 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 ${\boldsymbol{v}}$) to fresh ones of age $0$ (encoding $F({\boldsymbol{v}})$), and let time pass by one unit to enter the next round.

(Tj) \[place, label=right:[$\mathit{True}_j$]{}\] ; (Ti) \[place, below=of Tj, label=right:[$\mathit{True}_{i}$]{}\] ; (Tk) \[place, below=of Ti, label=right:[$\mathit{True}_{k}$]{}\] ; (Fj) \[place, right=of Tj, label=left:[$\mathit{False}_j$]{}\] ; (Fi) \[place, right=of Ti, label=left:[$\mathit{False}_{i}$]{}\] ; (Fk) \[place, right=of Tk, label=left:[$\mathit{False}_{k}$]{}\] ;

(iB) \[transition, left=of Ti, label=left:[$i.B$]{}\] [$x=y=1$]{}; (iL) \[transition, right=of Fj, label=right:[$i.L$]{}\] [$x=1$]{}; (iR) \[transition, right=of Fk, label=right:[$i.R$]{}\] [$x=1$]{}; (Tj) edge node\[above\][$x$]{} (iB); (Tk) edge node\[above\][$y$]{} (iB); (iB) edge node\[above\][$0$]{} (Ti);

(Fj) edge node\[above\][$x$]{} (iL); (iL) edge node\[above\][$0$]{} (Fi);

(iL) edge node\[above\] (Fj); (iR) edge node\[above\][ ]{}(Fk); (iB) edge node\[above\](Tj); (iB) edge node\[above\](Tk);

(Fk) edge node\[above\][$x$]{} (iR); (iR) edge node\[above\][$0$]{} (Fi);

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

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

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

3.  If $(p,c)\in M_{{\boldsymbol{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_{{\boldsymbol{v}}}$. For every constraint $i'=j\land k$ we introduce three transitions, $i.L, i.R$, and $i.B$, where $$\begin{aligned}
        {\mathit{Pre}}(i.B) &{{\overset{\text{\tinydef}}{=}}}{({\mathit{True}_{j}},x) + ({\mathit{True}_{k}},y)}
        &&
        {\mathit{Post}}(i.B) {{\overset{\text{\tinydef}}{=}}}{\mathit{Pre}}(i.B) + {({\mathit{True}_{i}},0)}\\
        {\mathit{Pre}}(i.L) &{{\overset{\text{\tinydef}}{=}}}{({\mathit{False}_{j}},x)}
        &&
        {\mathit{Post}}(i.L) {{\overset{\text{\tinydef}}{=}}}{\mathit{Pre}}(i.L) + ({\mathit{False}_{i}},0)\\
        {\mathit{Pre}}(i.R) &{{\overset{\text{\tinydef}}{=}}}{({\mathit{False}_{k}},x)}
        &&
        {\mathit{Post}}(i.R) {{\overset{\text{\tinydef}}{=}}}{\mathit{Pre}}(i.R) + ({\mathit{False}_{i}},0)
    \end{aligned}$$ and the guard for all transitions is $G(x)=G(y)=1$. See \[fig:LB\] for an illustration. For disjunctions $i'=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]{}[claimone]{}\[claim1\] If $F({\boldsymbol{v}})={\boldsymbol{v}}'$ then for every encoding $M_{{\boldsymbol{v}}}$ of ${\boldsymbol{v}}$, there exists an encoding $M_{{\boldsymbol{v'}}}$ of ${\boldsymbol{v}}'$ such that $M_{{\boldsymbol{v}}}{\longrightarrow_{1}}{{\xrightarrow{*}_{\textit{Disc}}}}M_{{\boldsymbol{v}}'}$. Conversely, if $M_{{\boldsymbol{v}}}{\longrightarrow_{1}}{{\xrightarrow{*}_{\textit{Disc}}}}M_{{\boldsymbol{v}}'}$ for encodings $M_{{\boldsymbol{v}}}$ and $M_{{\boldsymbol{v'}}}$ of ${\boldsymbol{v}}$ and ${\boldsymbol{v}}'$ respectively, then $F({\boldsymbol{v}}) = {\boldsymbol{v'}}$.

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{\tinydef}}{=}}}(M_{{\boldsymbol{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\ge (M_{{\boldsymbol{v}}}+1)$, for all $i<n$. Consider now constraint $i'$, and assume w.l.o.g. that $i' = j \land k$ (the other case is analogous). There are two cases depending on ${\boldsymbol{v'}}[i]$.

1.  Case ${\boldsymbol{v'}}[i]=1$. By our assumption that $F({\boldsymbol{v}})={\boldsymbol{v'}}$ we know that ${\boldsymbol{v}}[j] =1$ and ${\boldsymbol{v}}[k] =1$. So $({\mathit{True}_{j}},1) \in (M_{{\boldsymbol{v}}}+1) \le M_{i-1}$ and $({\mathit{True}_{k}},1) \in (M_{{\boldsymbol{v}}}+1) \le 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\le 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_{{\boldsymbol{v}}}$ encodes ${\boldsymbol{v}}$. Therefore $({\mathit{False}_{i}},0)\notin M_{n-1}$.

2.  Case ${\boldsymbol{v'}}[i]=0$. W.l.o.g., ${\boldsymbol{v}}[j] =0$. Therefore, $({\mathit{False}_{j}},1) \in (M_{{\boldsymbol{v}}}+1) \le 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\le 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 ${\boldsymbol{v'}}$.

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

1.  Case ${\boldsymbol{v'}}[i]=1$. By definition of a marking encoding, we have that $({\mathit{True}_{i}},0)\in M_{{\boldsymbol{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_{{\boldsymbol{v}}}+1) {{\xrightarrow{*}_{\textit{Disc}}}} M_{{\boldsymbol{v}}}'$, where $M_{{\boldsymbol{v}}}{\longrightarrow_{1}} (M_{{\boldsymbol{v}}}+1)$. Note that $({\mathit{True}_{j}},1)\in (M_{{\boldsymbol{v}}}+1)$ and $({\mathit{True}_{k}},1)\in (M_{{\boldsymbol{v}}}+1)$. Hence, we have that ${\boldsymbol{v}}[j]=1$ and ${\boldsymbol{v}}[k]=1$, and therefore that $F({\boldsymbol{v}})[i] = {\boldsymbol{v'}}[i] = {\boldsymbol{v}}[j] \land {\boldsymbol{v}}[k]$.

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

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

\[thm:LB\] [$\exists$COVER ]{} is [$\mathsf{PSPACE}$]{}-hard for non-consuming TPN.

For a given monotone Boolean circuit, define a non-consuming TPN as above. By induction on $m\in{\mathbb{N}}$ using \[claim1\], we derive that there exists $m\in{\mathbb{N}}$ with $F^m({\boldsymbol{v}})={\boldsymbol{v}}'$ and ${\boldsymbol{v}}'[0]=1$ if, and only if, there exists encodings $M_{{\boldsymbol{v}}}$ of ${\boldsymbol{v}}$ and $M_{{\boldsymbol{v'}}}$ of ${\boldsymbol{v'}}$, with $M_{{\boldsymbol{v}}}{\xrightarrow{*}} M_{{\boldsymbol{v}}'}$. Moreover, if there is a marking $M$ such that $M_{{\boldsymbol{v}}}{\xrightarrow{*}} M$ and $0\in {{\it frac}(M)}$, where $M$ contains a token of age $0$, then $M\le M_{{\boldsymbol{v'}}}$ for some encoding $M_{{\boldsymbol{v}}'}$ of a vector ${\boldsymbol{v'}}=F^m({\boldsymbol{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_{{\boldsymbol{v}}'}$ containing a token $({\mathit{True}_{0}},0)$. By the properties above, there exists $m\in{\mathbb{N}}$ with $F^m({\boldsymbol{v}})={\boldsymbol{v}}'$ and ${\boldsymbol{v}}'[0]=1$ iff $M_{{\boldsymbol{v}}}{\xrightarrow{*}}M_{{\boldsymbol{v}}'}{\xrightarrow{t}}$.

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

Upper Bound {#sec:upperbound}
===========

We start by observing that we can restrict ourselves, without loss of generality, to non-consuming TPN (\[def:nonconsuming\]) 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]{}[lemnonconsuming]{} \[lem:mtpn:wlog\] \[lem:nonconsuming\] 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}}'$ together with a place $p'$ and transition $t'$ of ${\mathcal{N}}'$, so that there exists $M\in{\mathit{Cover}_{{\mathcal{N}}}{\mathopen{}\mathclose\bgroup\originalleft}({\mathbb{N}}\cdot\{(p,{0})\}{\aftergroup\egroup\originalright})}$ enabling $t$ in ${\mathcal{N}}$ if and only if there exists $M'\in{\mathit{Cover}_{{\mathcal{N}}'}{\mathopen{}\mathclose\bgroup\originalleft}({\mathbb{N}}\cdot\{(p',0)\}{\aftergroup\egroup\originalright})}$ that enables $t'$ in ${\mathcal{N}}'$.

First notice that the first condition in \[def:nonconsuming\], 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}}'$ be the non-consuming variant derived from ${\mathcal{N}}$ where for all transitions $T$, ${\mathit{Post}}_{{\mathcal{N}}'}(t){{\overset{\text{\tinydef}}{=}}}{\mathit{Post}}_{\mathcal{N}}(t)\oplus{\mathit{Pre}}_{\mathcal{N}}(t)$. Notice that then, for every discrete step $M {\longrightarrow_{t}}M'$ we have that $M \leq M'$. We prove the following claim.

*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'\in{\mathit{Cover}_{{\mathcal{N}}'}({\mathbb{N}}\cdot\{(p,0)\})}$ that enables $t$ in ${\mathcal{N}}'$.*

The “${\mathcal{N}}\to{\mathcal{N}}'$” direction follows from the observation that the pointwise ordering $\le$ on markings, is a simulation: If $M{\xrightarrow{}}N$ and $M'\ge M$ then there exists an $N'\ge N$ with $M'{\xrightarrow{}}N'$. For the other direction, suppose there exists a witnessing path $$m\cdot\{(p,{0})\}~=~M_0{\xrightarrow{}}M_1{\xrightarrow{}}M_2{\xrightarrow{}}\cdots{\xrightarrow{}}M_k{\xrightarrow{t}}$$ of length $k$ in ${\mathcal{N}}'$. We can inductively derive a witnessing path in ${\mathcal{N}}$ backwards, again using the fact that $\le$ is a simulation. First note that if $M'$ enables $t$, then every $m'\cdot M'$ with $m'>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'_{i-1}\in\ {\downarrow\!{(}}{\mathbb{N}}\cdot M_{i-1})$ and $M'_{i}\in\ {\downarrow\!{(}}{\mathbb{N}}\cdot M_{i})$ such that $M'_{i-1}{\xrightarrow{}} M'_{i}$. It suffices to pick $M'_{i-1}{{\overset{\text{\tinydef}}{=}}}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 ${{\lvertP\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})\}$.

Region Abstraction {#sec:regionabs}
------------------

We recall a constraint system called regions defined for timed automata [@AD:1994]. The version for TPN used here is similar to the one in [@AMM07].

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{\tinydef}}{=}}}\min\{{c_\mathit{max}}+1, \lfloor{c}\rfloor\}$ and ${{\it frac}(c)} {{\overset{\text{\tinydef}}{=}}}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{\tinydef}}{=}}}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.

\[oneclock:abstr\] Let $M\subseteq P {\times}{{\mathbb R}_{\geq 0}}$ be a marking and let ${{\it frac}(M)} {{\overset{\text{\tinydef}}{=}}}\{{{\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\le n$. The *$S$-abstraction* of $M$ is $${\mathit{abs}_{S}(M)} {{\overset{\text{\tinydef}}{=}}}x_0x_1\dots x_n \in \Sigma^*$$ where $x_i {{\overset{\text{\tinydef}}{=}}}\{(p,{{\it int}(c)}) \mid (p,c)\in M \land {{\it frac}(c)}=f_i\}$ for all $i\le n$. We simply write ${\mathit{abs}_{}(M)}$ for the shortest abstraction, i.e. with respect to $S=\{0\}\cup{{\it frac}(M)}$.

The abstraction of marking $M = \{(p,2.1),(q,2.2),(p,5.1),(q,5.1)\}$ is ${\mathit{abs}_{}(M)}=\emptyset~\{(p,2),(p,5),(q,5)\}~\{(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 \[oneclock:abstr\].

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

\[expression:def\] 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{\tinydef}}{=}}}\{N\mid \exists M \exists S.~
    M\ge N \land {\mathit{abs}_{S}(M)}\in{{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}(E{\aftergroup\egroup\originalright})}\}.$$

An expression is *simple* if it is of the form $E = x_0x_1\dots x_{k}$ where for all $i\le 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.

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'$, 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. state that maximally firing of discrete transitions (the relation ${\xrightarrow{*}_{\textit{Disc}}}$) is computable and monotone. state how to represent timed-step successor markings.

[lemma]{}[lemdiscall]{} \[lem:discall\] \[lem:monotonicity\] 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.  \[lem:discall-ad1\] $f$ and $g$ are monotone (w.r.t. subset ordering) in each argument.

2.  \[lem:discall-ad2\] $f(\alpha, \beta, x) \supseteq x$ and $g(\alpha, \beta, x) \supseteq x$ for all $\alpha,\beta,x \in \Sigma$.

3.  \[lem:discall-ad3\] Suppose that $E=x_0x_1\dots x_k$ is a simple expression, $\alpha {{\overset{\text{\tinydef}}{=}}}x_0$ and $\beta {{\overset{\text{\tinydef}}{=}}}\bigcup_{i>0} \hat{x}_i$, and $E' = x'_0x'_1\dots x'_k$ is the derived expression defined by conditions:

    1.  $x_0' {{\overset{\text{\tinydef}}{=}}}f(\alpha,\beta,x_0)$,

    2.  $x_i' {{\overset{\text{\tinydef}}{=}}}g(\alpha,\beta,\hat{x}_i)^*$ for $i>0$,

    3.  $x_i'$ carries a star iff $x_i$ does.

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

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 (\[lem:discall-starfree\]) and then generalize to all simple expressions by induction.

\[def:discall\] We will write ${\mathit{SAT}(E)} {{\overset{\text{\tinydef}}{=}}}E'$ for the successor expression $E'$ of $E$ guaranteed by \[lem:discall\]. 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\bgroup\originalleft}({[\![E]\!]}{\aftergroup\egroup\originalright})}$, and consequently also that ${\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![{\mathit{SAT}(E)}]\!]}{\aftergroup\egroup\originalright})}={\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![E]\!]}{\aftergroup\egroup\originalright})}$.

\[lem:simulation\] Suppose that $X=x_0x_1\dots x_k$ is a simple expression of length $k+1$ with ${\mathit{SAT}(X)}=x'_0x'_1\dots x'_k$ and $x_0,x'_0\in\Sigma$. Let $Y=y_0\alpha_1y_1\alpha_2\dots \alpha_k y_k$ be a simple expression with ${\mathit{SAT}(Y)}=y'_0\alpha'_1y'_1\alpha'_2\dots \alpha'_k y'_k$ and $y_0,y'_0\in\Sigma$.

If $\hat{x}_i \subseteq \hat{y}_i$ for all $i\le k$ then $\hat{x}'_i 
    \subseteq
    \hat{y}'_i 
    $ for all $i\le k$.

The assumption of the lemma provides that $\alpha_x{{\overset{\text{\tinydef}}{=}}}x_0 \subseteq \alpha_y{{\overset{\text{\tinydef}}{=}}}y_0$ and $\beta_x{{\overset{\text{\tinydef}}{=}}}\bigcup_{k\ge i>0}\hat{x}_i \subseteq \beta_y{{\overset{\text{\tinydef}}{=}}}\bigcup_{k\ge i>0}\hat{y}_i$. Therefore, by \[lem:discall-ad1\] of \[lem:discall\], we get that $$x'_0 = f(\alpha_x,\beta_x,x_0)
    \quad\subseteq\quad
    f(\alpha_y,\beta_y,y_0)
    =y'_0$$ and similarly, for all $k\ge i\ge 0$, that $\hat{x}'_i = g(\alpha_x,\beta_x,\hat{x}_i)
    ~\subseteq~
    g(\alpha_y,\beta_y,\hat{y}_i)
    = \hat{y}'_i.
    $

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

[lemma]{}[lemepsilonsteps]{} \[lem:epsilonsteps\] $
    {[\![\emptyset E]\!]} = 
    \{M' \mid \exists M \in {[\![E]\!]} \land M{\longrightarrow_{d}}M' \land d < 1-\max(frac(M))\}
    $.

*“$\supseteq$”*: Suppose that $M$ is a non-empty marking in ${[\![E]\!]}$, $d<1-\max({{\it frac}(M)})$ and $M{\longrightarrow_{d}}M'$. 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'$. Also from the assumption on $d$ we get that $${{\it frac}(M')}= \{x+d \mid x \in {{\it frac}(M)}\}$$ Recall that ${\mathit{abs}_{}(M)}={\mathit{abs}_{S}(M)}$ and ${\mathit{abs}_{}(M')}={\mathit{abs}_{S'}(M')}$ for the sets $S{{\overset{\text{\tinydef}}{=}}}\{0\}\cup {{\it frac}(M)}$ and $S'{{\overset{\text{\tinydef}}{=}}}\{0\}\cup {{\it frac}(M')}$. Clearly, $0\notin {{\it frac}(M')}$. There are two cases:

1.  $0\in{{\it frac}(M)}$. Then ${\mathit{abs}_{}(M')}=\emptyset{\mathit{abs}_{}(M)}\in {{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}(\emptyset E{\aftergroup\egroup\originalright})}$, and consequently, $M'\in{[\![\emptyset E]\!]}$.

2.  $0\notin{{\it frac}(M)}$. Then ${\mathit{abs}_{}(M')}={\mathit{abs}_{}(M)}=\emptyset w\in {{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}(E{\aftergroup\egroup\originalright})}$. 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\bgroup\originalleft}(\alpha{\aftergroup\egroup\originalright})}$. If $x_0=\emptyset$ then ${[\![E]\!]}={[\![\emptyset E]\!]}$ and thus ${\mathit{abs}_{}(M')}\in{[\![\emptyset E]\!]}$. Otherwise, if $x_0\neq\emptyset$ then $x_0w\in{{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}(E{\aftergroup\egroup\originalright})}$ and $x_0w={\mathit{abs}_{}(M'')}$ for some marking $M''\ge M'$. So again, $M'\in{[\![\emptyset E]\!]}$.

*“$\subseteq$”*: W.l.o.g., pick a non-empty marking $M'\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'\in{[\![E]\!]}$. So suppose that $E$ does not start with $\emptyset$. Note that by \[oneclock:abstr\], there are no tokens in the marking $M'$ whose clocks have fractional value zero. Let $$d{{\overset{\text{\tinydef}}{=}}}\min({{\it frac}(M')})$$ be the minimal fractional clock value among the tokens of $M'$ and based on this, define $M {{\overset{\text{\tinydef}}{=}}}\{ (p,c-d)\mid (p,c)\in N' \} $. By construction of $M$ we get $M{\longrightarrow_{d}}M'$ and also that $\max({{\it frac}(M)}) = \max({{\it frac}(M')})-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')} \}$ and $0\in{{\it frac}(M)}$. It follows that ${\mathit{abs}_{}(M')}=\emptyset{\mathit{abs}_{}(M)}$ and therefore that ${\mathit{abs}_{}(M)}\in {{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}(E{\aftergroup\egroup\originalright})}$ and $M\in{[\![E]\!]}$. This means that $M'$ is included in the set on the right in the claim.

[lemma]{}[lemnonstarrotation]{}\[oneclock:rota\] \[lem:nonstarrotation\] 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'\ge N$ and $M$, and a set $S\subseteq [0,1[$ so that

1.  ${{\lvertS\rvert}} = {{\lvert\alpha z\rvert}}$

2.  ${\mathit{abs}_{S}(M)}\in {{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}(\alpha z{\aftergroup\egroup\originalright})}$

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

Suppose markings $N,N',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'{{\overset{\text{\tinydef}}{=}}}\{0\}\cup \{s+d\mid s\in S\setminus\{d\}\}$. Then, ${{\lvertS'\rvert}}={{\lvertS\rvert}}$ and ${\mathit{abs}_{S'}(N')} \in{{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}((z+1)\alpha{\aftergroup\egroup\originalright})}$, 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\bgroup\originalleft}((z+1){\aftergroup\egroup\originalright})}$ for $S{{\overset{\text{\tinydef}}{=}}}{{\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\bgroup\originalleft}(z{\aftergroup\egroup\originalright})}={{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}(\alpha z{\aftergroup\egroup\originalright})}$.

If ${{\lvert\alpha\rvert}} >0$, pick some marking $N'\ge N$ and set $S'$ so that ${\mathit{abs}_{S'}(N')}=(z+1)w$, for some word $w\in{{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}(\alpha{\aftergroup\egroup\originalright})}$. Then we must have that ${{\lvertS'\rvert}}={{\lvert(z+1)\alpha\rvert}}>1$ and so $d{{\overset{\text{\tinydef}}{=}}}\min(S'\setminus\{0\})$ exists. Let $S{{\overset{\text{\tinydef}}{=}}}\{s-d\mid s\in S'\}\cup\{1-d\}$ and $M$ be the unique marking with $M{\longrightarrow_{d}}N'$. Notice that $1-d=\max(S)$. It follows that ${\mathit{abs}_{S}(M)}=wz\in{{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}(\alpha z{\aftergroup\egroup\originalright})}$.

We will often use the following simple fact, which is a direct consequence of \[lem:nonstarrotation\].

\[cor:nonstarrotation\] ${[\![(z+1)\alpha]\!]}
    \subseteq {\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![\alpha z]\!]}{\aftergroup\egroup\originalright})}$.

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

[lemma]{}[lemaccstep]{} \[lem:accstep\] Let $\alpha x_0^*$ be a simple expression with ${\mathit{SAT}(\alpha x_0^*)}=\alpha x_0^*$. Then $
    {\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![\alpha x_0^*]\!]}{\aftergroup\egroup\originalright})} = 
    {[\![\alpha x_0^*]\!]}
    \cup {\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![(x_0+1)\alpha x_0^*]\!]}{\aftergroup\egroup\originalright})}$.

For the right to left inclusion notice that ${[\![\alpha x_0^*]\!]} \subseteq {\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![\alpha x_0^*]\!]}{\aftergroup\egroup\originalright})}$ trivially holds. For the rest, we have $
    {[\![(x_0+1)\alpha x_0^*]\!]}
    \subseteq
    {\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![\alpha x_0^*]\!]}{\aftergroup\egroup\originalright})}
    $ by \[cor:nonstarrotation\], and therefore ${\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![(x_0+1)\alpha x_0^*]\!]}{\aftergroup\egroup\originalright})}
    ~\subseteq~
    {\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![\alpha x_0^*]\!]}{\aftergroup\egroup\originalright})}{\aftergroup\egroup\originalright})}
    =
    {\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![\alpha x_0^*]\!]}{\aftergroup\egroup\originalright})}
    $. For the left to right inclusion, we equivalently show that $${\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![\alpha x_0^*]\!]}{\aftergroup\egroup\originalright})} \setminus
    {[\![\alpha x_0^*]\!]}
    \subseteq
    {\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![(x_0+1)\alpha x_0^*]\!]}{\aftergroup\egroup\originalright})}$$ 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\bgroup\originalleft}(
    \{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))
    \}
    {\aftergroup\egroup\originalright})}.$$ By \[lem:epsilonsteps\] and because ${[\![\emptyset\alpha]\!]}\subseteq {[\![X\alpha]\!]}$ for all $X\in \Sigma$ and $\alpha\in\Sigma^*$, we conclude that indeed, $
    {\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![\alpha x_0^*]\!]}{\aftergroup\egroup\originalright})} \setminus
    {[\![\alpha x_0^*]\!]}
    ~\subseteq~
    {\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![\emptyset\alpha x_0^*]\!]}{\aftergroup\egroup\originalright})}
    \subseteq
    {\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![(x_0+1)\alpha x_0^*]\!]}{\aftergroup\egroup\originalright})}
    $.

Acceleration
------------

We propose an acceleration procedure based on unfolding expressions according to \[lem:accstep\] (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 \[alg:inner\_loop\]), is used to characterize an initial subset of the coverability set.

a simple expression $S_0 = x_1x_0^*$ (of length 2 and with last symbol starred) simple expressions $S_1, S_i$ and $R$, of lengths 2, 4, and 2, respectively.

$S_1 {{\overset{\text{\tinydef}}{=}}}x_1^1(x_0^1)^*= {\mathit{SAT}(x_1x_0^*)}$ $S_2 {{\overset{\text{\tinydef}}{=}}}x_2^2x_1^2(x_0^2)^*= {\mathit{SAT}((x_0^1+1)S_1)}$ $S_3 {{\overset{\text{\tinydef}}{=}}}x_3^3x_2^3x_1^3(x_0^3)^*= {\mathit{SAT}((x_0^2+1)S_2)}$ $i\gets 3$

$x_{i+1}^{i+1}x_{i}^{i+1}x_{i-1}^{i+1}x_1^{i+1}(x_0^{i+1})^*{{\overset{\text{\tinydef}}{=}}}{\mathit{SAT}((x_0^{i}+1)S_{i})}$ $S_{i+1} {{\overset{\text{\tinydef}}{=}}}x_{i+1}^{i+1}(x_{i}^{i+1})^*x_1^{i+1}(x_0^{i+1})^*$ $i\gets i+1$ $R {{\overset{\text{\tinydef}}{=}}}(x_1^i+1)(x_{i-1}^i)^*$ $S_1, S_i, R$

= \[ align=center\] = \[graphnode, red\] = \[graphnode, black\] = \[graphnode, black\] = \[graphnode, black\] = \[align=left,text width=3.5cm\] = \[-&gt;, lightgray\] = \[-, lightgray\] = \[-&gt;, red\] = \[draw,-&gt;, blue\]

(S0-0) \[snode\] [$x_0^{*}$]{}; (S0-1)\[snode, left=of S0-0\] [$x_1$]{}; (S0-label) \[label,right=of S0-0\] [start]{};

(S1-0) \[snode, below =of S0-0\] [$(x_0^1)^{*}$]{}; (S1-1) \[ snode, left =of S1-0\] [$x_1^1$]{};

(S1-label) \[below=of S0-label\] [$S_1 = {\mathit{SAT}(x_1x_0^*)} $]{} ;

(S1-rot-0) \[snode, below =of S1-0\] [$(x_0^1)^{*} $]{}; (S1-rot-1) \[snode, left =of S1-rot-0\] [$x_1^1$]{}; (S1-rot-2) \[newnode, left =of S1-rot-1\] [ $(x_0^1+1)$]{}; (S1-rot-label) \[label,below =of S1-label\] [$(x_0^1+1)S_1 $]{};

(S2-0) \[snode, below =of S1-rot-0\] [$(x_0^2)^{*}$]{}; (S2-1) \[snode, left =of S2-0 \] [$x_1^2$]{}; (S2-2) \[nnewnode, left = of S2-1\] [$x_2^2$]{}; (S2-label)\[label, below=of S1-rot-label\] [$S_2={\mathit{SAT}((x_0^1+1)S_1)}$]{};

(S2-rot-0) \[snode, below =of S2-0 \] [$(x_0^2)^{*} $]{}; (S2-rot-1) \[snode, left = of S2-rot-0\] [$x_1^2$]{}; (S2-rot-2) \[mnode, left = of S2-rot-1\] [ $x_2^2$]{}; (S2-rot-3)\[newnode, left =of S2-rot-2\][ $(x_0^2+1)$]{}; (S2-rot-label) \[label,below =of S2-label\] [$(x_0^2+1)S_2 $]{};

(S3-0) \[snode, below =of S2-rot-0\][$(x_0^3)^{*}$]{}; (S3-1) \[snode, left =of S3-0 \] [$x_1^3$]{}; (S3-2) \[mnode, left =of S3-1 \][$x_2^3$]{}; (S3-3) \[nnewnode, left =of S3-2 \][$x_3^3$]{}; (S3-label)\[label, below=of S2-rot-label\] [$S_3={\mathit{SAT}((x_0^2+1)S_2)}$]{};

(S3-rot-0) \[snode, below =of S3-0 \] [$(x_0^3)^{*} $]{}; (S3-rot-1) \[snode, left =of S3-rot-0\] [$x_1^3$]{}; (S3-rot-2) \[mnode, left =of S3-rot-1\] [ $x_2^3$]{}; (S3-rot-3) \[mnode,left =of S3-rot-2\] [$x_3^3$]{}; (S3-rot-4)\[newnode, left =of S3-rot-3\][ $(x_0^3+1)$]{}; (S3-rot-label) \[label,below =of S3-label\] [$(x_0^3+1)S_3 $]{};

(L4-0) \[snode,below =of S3-rot-0\][$(x_0^4)^{*}$]{}; (L4-1) \[snode, left =of L4-0\][$x_1^4$]{}; (L4-2) \[mnode,left =of L4-1\] [$x_2^4$]{}; (L4-3) \[mnode,left =of L4-2\] [$x_3^4$]{}; (L4-4) \[nnewnode,left =of L4-3\] [$x_4^4$]{}; (L4-label)\[label, below=of S3-rot-label\] [${\mathit{SAT}((x_0^3+1)S_3)}$]{};

(S4-0) \[snode, below=of L4-0\] [$(x_0^4)^{*}$]{}; (S4-1) \[snode, left =of S4-0\][$x_1^4$]{}; (S4-2) \[mnode, left=of S4-1\]; (S4-3) \[mnode, left=of S4-2\][$(x_3^4)^{*}$]{}; (S4-4) \[nnewnode, left =of S4-3\][$x_4^4$]{}; (S4-label)\[label, below=of L4-label\] [$S_4$]{};

(S4-rot-0) \[snode, below =of S4-0\][$(x_0^4)^{*}$]{}; (S4-rot-1) \[snode, left = of S4-rot-0\] [$x_1^4$ ]{}; (S4-rot-2) \[mnode, left=of S4-rot-1\]; (S4-rot-3) \[mnode, left=of S4-rot-2\][$(x_3^4)^{*}$ ]{}; (S4-rot-4)\[mnode, left =of S4-rot-3\][$x_4^4$]{}; (S4-rot-5) \[newnode, left =of S4-rot-4\][$(x_0^4+1)$ ]{}; (S4-rot-label) \[label,below =of S4-label\] [$(x_0^4+1)S_4 $]{};

(L5-0) \[snode, below=of S4-rot-0\] [$(x_0^5)^{*} $]{}; (L5-1) \[snode, left=of L5-0\] [$x_1^5$]{}; (L5-2) \[mnode, left=of L5-1\] ; (L5-3) \[mnode, left=of L5-2\] [$(x_3^5)^*$]{}; (L5-4) \[mnode, left=of L5-3\] [$x_4^5$]{}; (L5-5) \[nnewnode, left=of L5-4\] [$x_5^5$]{}; (L5-label)\[label, below=of S4-rot-label\] [${\mathit{SAT}((x_0^4+1)S_4)}$]{};

(S5-0) \[snode, below=of L5-0\] [$(x_0^5)^{*}$]{}; (S5-1) \[snode, left=of S5-0\] [$x_1^5$]{}; (S5-2) \[snode, left=of S5-1\] ; (S5-3) \[snode, left=of S5-2\] ; (S5-4) \[mnode, left=of S5-3\] [$(x_4^5)^{*}$]{}; (S5-5) \[nnewnode,left=of S5-4\] [$x_5^5$]{}; (S5-label)\[label, below=of L5-label\] [$S_5$]{};

(S5-rot-0) \[snode, below=1cm of S5-0\][$\vdots$]{}; (S5-rot-1) \[snode, left = of S5-rot-0\] [$\vdots$]{}; (S5-rot-2) \[mnode, left=of S5-rot-1\]; (S5-rot-3) \[mnode, left=of S5-rot-2\]; (S5-rot-4)\[mnode, left =of S5-rot-3\][$\vdots$]{}; (S5-rot-5)\[mnode, left =of S5-rot-4\][$\vdots$]{}; (S5-rot-6) \[newnode, left =of S5-rot-5\][$\vdots$]{}; (S5-rot-label) \[label,right=of S5-rot-0\] [$\vdots$]{};

(S0-0) -&gt; (S1-0); (S0-1) -&gt; (S1-1); \[evaluate=[=int(-1);=int(-2);]{}\] in [2,...,5]{}[ iin [0,...,]{}[ ]{} ]{} (S1-rot-2) -&gt; (S2-rot-3); (S2-rot-3) -&gt; (S3-rot-4); (S3-rot-4) -&gt; (S4-rot-5); (S4-rot-5) -&gt; (S5-rot-6);

(S2-2) -&gt; (S3-3); (S3-3) -&gt; (S4-4); (S4-4) -&gt; (S5-5);

(S3-2) -&gt; (S4-3); (S4-3) -&gt; (S5-4);

\[evaluate=[=int(-1);=int(-2);]{}\] in [1,...,5]{}[ iin [0,...,]{}[ ]{} ]{}

; ; ; ; ; ; ; ;

Given a length-2 simple expression $S_0$ where the rightmost symbol is starred, the algorithm will first saturate (\[def:discall\], in line 1), and then alternatingly rotate a copy of the rightmost symbol (\[oneclock:rota\]), 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 \[alg:inner\_loop\] is well defined because the ${\mathit{SAT}(S_i)}$ are computable by \[lem:discall\]. Termination is guaranteed by the following simple observation.

\[lem:termobs\] Let $x_j^i\in\Sigma$ be the symbols computed by \[alg:inner\_loop\]. Then

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

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

The first item is guaranteed by Point 2 of \[lem:discall\]. 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\ge 0$ (indicated as red arrows in \[fig:algorithm1\]). The second item now follows from this observation by \[lem:simulation\].

\[lem:termination\] \[alg:inner\_loop\] terminates with $i \le 4\cdot {{\lvertP\rvert}}\cdot({c_\mathit{max}}+1)$.

From \[lem:termobs\] we deduce that for all $i\ge2$, 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\ge 3}$ have length $4$ and that every symbol $x_i\in\Sigma$ can only increase at most ${{\lvertP\rvert}}\cdot ({c_\mathit{max}}+1)$ times.

\[lem:acc:correctness\] Suppose that $S_1,S_\ell, R$ be the expressions computed by \[alg:inner\_loop\] applied to the simple expression $x_1x_0^*$. Then ${\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![x_1x_0^*]\!]}{\aftergroup\egroup\originalright})}
    = {[\![S_1]\!]}
    \cup {[\![S_\ell]\!]}
    \cup {\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![R]\!]}{\aftergroup\egroup\originalright})}
    $.

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{\tinydef}}{=}}}S_1$ and if $E_i=e_i^ie_{i-1}^i\dots e_0^i$, we let $
E_{i+1} {{\overset{\text{\tinydef}}{=}}}e_{i+1}^{i+1}e_i^{i+1}e_{i-1}^{i+1}\dots e_0^{i+1}
{{\overset{\text{\tinydef}}{=}}}{\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 \[lem:accstep\], 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\bgroup\originalleft}({[\![x_1x_0^*]\!]}{\aftergroup\egroup\originalright})} = {\mathopen{}\mathclose\bgroup\originalleft}(\bigcup_{k-1\ge i\ge 1}{[\![E_i]\!]}{\aftergroup\egroup\originalright}) \cup {\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![E_k]\!]}{\aftergroup\egroup\originalright})}$ holds for all $k\in{\mathbb{N}}$. We will use that $$\label{eq:acc:EisS}
\bigcup_{i\ge 2}{[\![E_i]\!]}
= \bigcup_{i\ge 2}{[\![S_i]\!]}
={[\![S_\ell]\!]}.$$ We start by observing that for all $i,j\in{\mathbb{N}}$ it holds that $e_j^i = x_j^i$. For $i\le 3$ this holds trivially by definition of $E_i=S_i$. For larger $i$, this can be seen by induction using \[lem:discall\]. Towards the first equality in \[eq:acc:EisS\], 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{\tinydef}}{=}}}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\ge 0}{[\![S_i^j]\!]}$ and so the $\supseteq$-direction of the first equality in \[eq:acc:EisS\] follows by $$\begin{aligned}
{[\![S_i^j]\!]}= {[\![x_{i}^{i}({x_{i-1}^{i}})^{(j)}x_{1}^{i}(x_0^{i})^*]\!]}
&\subseteq
{[\![x_{i+j}^{i+j}
{\mathopen{}\mathclose\bgroup\originalleft}(
{x_{i+j-1}^{i+j}}
{x_{i+j-2}^{i+j}}
\ldots
{x_{i}^{i+j}}
{\aftergroup\egroup\originalright})
x_{1}^{i+1}(x_0^{i+1})^*]\!]}\\
&\subseteq
{[\![x_{i+j}^{i+j}
{\mathopen{}\mathclose\bgroup\originalleft}(
{x_{i+j-1}^{i+j}}
{x_{i+j-2}^{i+j}}
\ldots
{x_{i}^{i+j}}
{\aftergroup\egroup\originalright})
{\mathopen{}\mathclose\bgroup\originalleft}(
{x_{i-1}^{i+j}}
\ldots
{x_{2}^{i+j}}
{\aftergroup\egroup\originalright})
x_{1}^{i+1}(x_0^{i+j})^*]\!]}\\
&={[\![E_{i+j}]\!]},\end{aligned}$$ where the first inclusion is due to \[lem:termobs\]. The same helps for the other direction: $${[\![E_i]\!]} 
= {[\![x_{i}^{i}x_{i-1}^{i}x_{i-2}^{i}\dots x_2^ix_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]\!]},$$ which completes the proof of the first equality in \[eq:acc:EisS\]. The second equality holds because ${[\![S_i]\!]}\subseteq{[\![S_{i+1}]\!]}$ for all $i\ge 2$, by \[lem:termobs\], and by definition of $S_\ell=S_{\ell+1}$. As a next step we show that $$\label{eq:acc:Rconnection}
{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![S_\ell]\!]}{\aftergroup\egroup\originalright})}
= 
{[\![S_\ell]\!]}
\cup
{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![R]\!]}{\aftergroup\egroup\originalright})}$$ 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,

$$\begin{aligned}
{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![R]\!]}{\aftergroup\egroup\originalright})}
&=
{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![(x_1^\ell+1)x_\ell^\ell {(x_{\ell-1}^\ell)}^*]\!]}{\aftergroup\egroup\originalright})}
\\
&\subseteq
{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![x_\ell^\ell {(x_{\ell-1}^\ell)}^*x_1^\ell]\!]}{\aftergroup\egroup\originalright})}\\
&\subseteq
{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![x_\ell^\ell {(x_{\ell-1}^\ell)}^*x_1^\ell {(x_0^\ell)}^*]\!]}{\aftergroup\egroup\originalright})}
={\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![S_\ell]\!]}{\aftergroup\egroup\originalright})}\end{aligned}$$

where the first equation follows by \[cor:nonstarrotation\] and the second because ${{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}(x_\ell^\ell {(x_{\ell-1}^\ell)}^*x_1^\ell{\aftergroup\egroup\originalright})}\subseteq {{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}(x_\ell^\ell {(x_{\ell-1}^\ell)}^*x_1^\ell {(x_0^\ell)}^*{\aftergroup\egroup\originalright})}$. For the left to right inclusion in \[eq:acc:Rconnection\], consider a marking $M\in{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![S_\ell]\!]}{\aftergroup\egroup\originalright})}\setminus {[\![S_\ell]\!]}$. We show that $M\in{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![R]\!]}{\aftergroup\egroup\originalright})}$. Recall that ${\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![S_\ell]\!]}{\aftergroup\egroup\originalright})}$ consists of all those markings $M$ so that there exists a finite path $$M_0{\xrightarrow{*}_{\textit{Disc}}}M'_0{\xrightarrow{d_1}_{\textit{Time}}}M_1{\xrightarrow{*}_{\textit{Disc}}}M'_1{\xrightarrow{d_2}_{\textit{Time}}}M_2\dots M'_{k-1}{\xrightarrow{*}_{\textit{Disc}}}M_k$$ alternating between timed and (sequences of) discrete transition steps, with $M_0\in{[\![S_\ell]\!]}$, $M_k\ge M$ and all $d_i\le \max({{\it frac}(M'_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'_{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\ge 2}{[\![S_i]\!]}$, it must hold that $M'_{i-1} \in {[\![S_j]\!]} ={[\![x_j^j(x_{j-1}^j)^* x_1^j(x_0^j)^*]\!]}$ for some index $j\ge 2$. We claim that it already holds that $$\label{eq:acc:almostR}
    M'_{i-1} \in {[\![x_j^j{(x_{j-1}^j)}^*x_1^j]\!]}.$$ Suppose not. If $d_i<\max({{\it frac}(M'_{i-1})})$ then $M_i\in{[\![\emptyset S_j]\!]}\subseteq {[\![S_j]\!]}$ by \[lem:epsilonsteps\], contradiction. Otherwise, if $d_i=\max({{\it frac}(M'_{i-1})})$, notice that every abstraction ${\mathit{abs}_{S}(M'_{i-1})}\in{{\mathcal{L}}{\mathopen{}\mathclose\bgroup\originalleft}(S_j{\aftergroup\egroup\originalright})}$ must have ${{\lvertS\rvert}}=4$. So by \[lem:nonstarrotation\], $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}]\!]},$$ contradicting our assumption that $M_i\notin {[\![S_\ell]\!]}$. Therefore \[eq:acc:almostR\] holds. By \[lem:nonstarrotation\] 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 \[eq:acc:Rconnection\].

Notice that by \[lem:accstep\] we have that $$\label{eq:acc:EisSunr1}
{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![x_1 x_0^*]\!]}{\aftergroup\egroup\originalright})}
={[\![{\mathit{SAT}(x_1 x_0^*)}]\!]}
\cup{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![{\mathit{SAT}(x_1 x_0^*)}]\!]}{\aftergroup\egroup\originalright})}
={[\![S_1]\!]}
\cup{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![S_1]\!]}{\aftergroup\egroup\originalright})}.$$ Analogously, we get for every $i\ge 1$ that $$\begin{aligned}
    \label{eq:acc:2}
{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![E_i]\!]}{\aftergroup\egroup\originalright})}
= 
{[\![{\mathit{SAT}(E_i)}]\!]}
\cup {\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![{\mathit{SAT}((x^i_0+1)E_i)}]\!]}{\aftergroup\egroup\originalright})}
=
  {[\![E_i]\!]}
  \cup {\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![E_{i+1}]\!]}{\aftergroup\egroup\originalright})}\end{aligned}$$ This used \[lem:accstep\] and the fact that ${\mathit{SAT}(E_i)}=E_i$ by construction. Using \[eq:acc:2\] and that ${[\![E_i]\!]}\subseteq{[\![E_{i+1}]\!]}$ for $i\ge 2$, we deduce $$\label{eq:acc:3}
{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![S_1]\!]}{\aftergroup\egroup\originalright})}
={\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![E_1]\!]}{\aftergroup\egroup\originalright})}
=
{[\![E_1]\!]}
\cup
{\mathopen{}\mathclose\bgroup\originalleft}(
\bigcup_{i\ge 2}{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![E_i]\!]}{\aftergroup\egroup\originalright})}
{\aftergroup\egroup\originalright}).$$ Finally we can conclude the desired result as follows. $$\begin{aligned}
{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![x_1 x_0^*]\!]}{\aftergroup\egroup\originalright})}
&{\overset{\text{\tiny(\ref{eq:acc:EisSunr1})}}{=}}
{[\![S_1]\!]}
\cup
{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![S_1]\!]}{\aftergroup\egroup\originalright})}
{\overset{\text{\tiny(\ref{eq:acc:3})}}{=}}
{[\![S_1]\!]}
\cup
{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}(
\bigcup_{i\ge 2}{[\![E_i]\!]}
{\aftergroup\egroup\originalright})}\\
&{\overset{\text{\tiny(\ref{eq:acc:EisS})}}{=}}
{[\![S_1]\!]}
\cup
{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![S_\ell]\!]}{\aftergroup\egroup\originalright})}\\
&{\overset{\text{\tiny(\ref{eq:acc:Rconnection})}}{=}}
{[\![S_1]\!]}
\cup
{[\![S_\ell]\!]}
\cup
{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({[\![R]\!]}{\aftergroup\egroup\originalright})}
\qedhere\end{aligned}$$

Main Result {#sec:central}
-----------

The following theorem summarizes our main claims regarding the [$\exists$COVER ]{}problem.

\[thm:central\] 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.  \[thm:cent:1\] The number of different simple expressions of length $m$ is $B(m) {{\overset{\text{\tinydef}}{=}}}2^{({{\lvertP\rvert}} \cdot ({c_\mathit{max}}+2) \cdot m)+m}$.

2.  \[thm:cent: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\le i\le \ell}{[\![S_i]\!]} =  {\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({\mathbb{N}}\cdot \{(p,{0})\}{\aftergroup\egroup\originalright})}$ and where $\ell \le 3\cdot B(2)$. Each of the $S_i$ has length either $2$ or $4$.

3.  \[thm:cent:3\] Checking if there exists $M\in{\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({\mathbb{N}}\cdot \{(p,0)\}{\aftergroup\egroup\originalright})}$ with $M{\longrightarrow_{t}}$ can be done in ${\mathcal{O}}({{\lvertP\rvert}}\cdot{c_\mathit{max}})$ deterministic space.

For \[thm:cent: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{\tinydef}}{=}}}2^{P{\times}{[{{c_\mathit{max}}+1}]}}$ and ${{\lvert{[{{c_\mathit{max}}+1}]}\rvert}}={c_\mathit{max}}+2$, the result follows.

Towards \[thm:cent:2\], we can assume w.l.o.g. that our TPN is non-consuming by \[lem:mtpn:wlog\], and thus the region abstraction introduced in \[sec:regionabs\] applies. In particular, the initial set of markings ${\mathbb{N}}\cdot \{(p,{0})\}$ is represented exactly by the expression $S_0 {{\overset{\text{\tinydef}}{=}}}\{(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 \[alg:inner\_loop\] until a previously seen expression is revisited. Starting at $i=0$ and $S_0 {{\overset{\text{\tinydef}}{=}}}\{(p,0)\}\emptyset^*$, each round will set $S_{i+1},S_{i+2}$ and $S_{i+3}$ to the result of applying \[alg:inner\_loop\] 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\le 3B(2)$). Finally, an induction using \[lem:acc:correctness\] provides that $\bigcup_{1\le i\le \ell}{[\![S_i]\!]} =  {\mathit{Cover}_{}{\mathopen{}\mathclose\bgroup\originalleft}({\mathbb{N}}\cdot \{(p,{0})\}{\aftergroup\egroup\originalright})}$.

Towards \[thm:cent: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; uses space ${\mathcal{O}}(\log(B(5)))$ because it stores only simple expressions of length $\le 5$. The space required to store the three expressions resulting from each application of \[alg:inner\_loop\] 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 \[thm:cent:1\], this is ${\mathcal{O}}(|P|\cdot ({c_\mathit{max}}+2))={\mathcal{O}}({{\lvertP\rvert}}\cdot{c_\mathit{max}})$.

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

The [$\mathsf{PSPACE}$]{} lower bound was shown in \[thm:LB\]. The upper bound follows from \[lem:mtpn:wlog\] and \[thm:cent:3\] of \[thm:central\].

Conclusion and Future Work {#sec:conclusion}
==========================

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}}$ [@HSS2012].

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 [@ADM2004].

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 [@AMM07; @AA2001] and the read-arc timed Petri nets of [@BHR2006].

\[sec:appendix\]

Proof of \[lem:discall\]
========================

\[lem:discall-starfree\] 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.  \[lem:discall-starfree-ad1\] $f$ and $g$ are monotone (w.r.t. subset ordering) in each argument.

2.  \[lem:discall-starfree-ad2\] $f(\alpha, \beta, x) \supseteq x$ and $g(\alpha, \beta, x) \supseteq x$ for all $\alpha,\beta,x \in \Sigma$.

3.  \[lem:discall-starfree-ad3\] For every word $w=x_0x_1\dots x_k$ over $\Sigma$, $\alpha {{\overset{\text{\tinydef}}{=}}}x_0$ and $\beta {{\overset{\text{\tinydef}}{=}}}\bigcup_{i>0} x_i$, and\
    $w' {{\overset{\text{\tinydef}}{=}}}f(\alpha,\beta,x_0)g(\alpha,\beta,x_1)\dots g(\alpha,\beta,x_k)$ we have ${[\![w']\!]} = 
        \{M'' \mid \exists M \in {[\![w]\!]} \land M{{\xrightarrow{*}_{\textit{Disc}}}}M' \ge M''\}
        $.

(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 ${{\lvertP\rvert}} \cdot ({c_\mathit{max}}+1)$ times, the number of iterations is polynomial. Moreover, the properties of \[lem:discall-starfree-ad1\], \[lem:discall-starfree-ad2\] and \[lem:discall-starfree-ad3\] 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{\tinydef}}{=}}}\{(p,c) \,|\, (p,y) \in S\ \wedge\ \pi(y)=c \in {\mathbb{N}}\}$ and $\pi_{>0}(S) {{\overset{\text{\tinydef}}{=}}}\{(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_0x_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{\tinydef}}{=}}}x$ and $f_t(\alpha,\beta,x) {{\overset{\text{\tinydef}}{=}}}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{\tinydef}}{=}}}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{\tinydef}}{=}}}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. \[lem:discall-starfree-ad1\] and \[lem:discall-starfree-ad2\] follow directly from the definition.

Towards \[lem:discall-starfree-ad3\], we show ${[\![w']\!]} \supseteq \{M'' \mid \exists M \in {[\![w]\!]} \land M
{\longrightarrow_{t}} M' \ge M''\}$. (The proof of the reverse inclusion $\subseteq$ is similar.) Let $w=x_0x_1\dots x_k$, $\alpha {{\overset{\text{\tinydef}}{=}}}x_0$, $\beta {{\overset{\text{\tinydef}}{=}}}\bigcup_{i>0} x_i$ such that $(\alpha,\beta)$ enables $t$ and $w' {{\overset{\text{\tinydef}}{=}}}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'$ then $M' \ge M$ since ${\mathcal{N}}$ is non-consuming. We show that every additional token $(p,u) \in M' \ominus M$ is included in ${[\![w']\!]}$. (This implies the inclusion above, since $M' \ominus M \ge M'' \ominus M$.) For every additional token $(p,u) \in M' \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'$ is abstracted to $g_t(\alpha,\beta,x_i)$ in $w'$.

-   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'$ is abstracted to $f_t(\alpha,\beta,x_0)$ in $w'$. 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'$ was abstracted to $f_t(\alpha,\beta,x_0)$ in $w'$.

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

Let $f$ and $g$ be the functions from \[lem:discall-starfree\], which immediately yields \[lem:discall-ad1\] and \[lem:discall-ad2\]. Towards \[lem:discall-ad3\], 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 \[lem:discall-starfree\] are the same as the $\alpha, \beta$ derived from $E$ in \[lem:discall-ad3\]. If $x_i$ in $E$ carries a star then $w$ contains a corresponding nonempty subsequence $x_i\dots x_i$. We apply \[lem:discall-starfree\] to each such $w$ to obtain the corresponding $w'$. The word $w'$ then contains the corresponding subsequence $g(\alpha,\beta,x_i)\dots g(\alpha,\beta,x_i)$. Let $E'$ then be defined as in \[lem:discall-ad3\], i.e., by applying functions to the symbols and keeping the stars at the same symbols as in $E$. By \[lem:discall-starfree\], this is computable in polynomial time. We have ${\mathcal{L}}(E') = \bigcup_{w \in {\mathcal{L}}(E)} \{w'\}$. Thus ${[\![E']\!]} = \bigcup_{w \in {\mathcal{L}}(E)} {[\![w']\!]}
=
\bigcup_{w \in {\mathcal{L}}(E)} \{M'' \mid \exists M \in {[\![w]\!]} \land
M{{\xrightarrow{*}_{\textit{Disc}}}}M' \ge M''\}
=
\{M'' \mid \exists M \in {[\![E]\!]} \land M{{\xrightarrow{*}_{\textit{Disc}}}}M' \ge M''\}
$ for \[lem:discall-ad3\] as required.
