Coverability Trees for Petri Nets with Unordered Data

Abstract

We study an extension of classical Petri nets where tokens carry values from a countable data domain, that can be tested for equality upon firing transitions. These Unordered Data Petri Nets (UDPN) are well-structured and therefore allow generic decision procedures for several verification problems including coverability and boundedness.

We show how to construct a finite representation of the coverability set in terms of its ideal decomposition. This not only provides an alternative method to decide coverability and boundedness, but is also an important step towards deciding the reachability problem. This also allows to answer more precise questions about the reachability set, for instance whether there is a bound on the number of tokens on a given place (place boundedness), or if such a bound exists for the number of different data values carried by tokens (place width boundedness).

We provide matching Hyper-Ackermann bounds on the size of coverability trees and on the running time of the induced decision procedures.

P. Hofman—Partially funded by the Polish National Science Centre grant 2013/09/B/ST6/01575 and by Labex Digicosme, Université Paris-Saclay, project VERICONISS.

S. Lasota—Partially funded by the Polish National Science Centre grant 2012/07/B/ST6/01497.

R. Lazić and P. Totzke—Partially supported by the EPSRC grant EP/M011801/1.

S. Schmitz—Partially supported by the ANR grant ANR-14-CE28-0005 prodaq and by the Leverhulme Trust Visiting Professorship VP1-2014-041.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Unordered data Petri nets (UDPN [15]) extend Petri nets by decorating tokens with data values taken from some countable data domain $\mathbb {D}$. These values act as pure names: they can only be compared for equality or non-equality upon firing transitions. Such systems can model for instance distributed protocols where process identities need to be taken into account [21]. UDPNs also coincide with the natural generalisation of Petri nets in the framework of sets with atoms [3]. In spite of their high expressiveness, UDPNs fit in the large family of Petri net extensions among the well-structured ones [1, 7]. As such, they still enjoy decision procedures for several verification problems, prominently safety (through the coverability problem) and termination.

Unordered data Petri nets have an interesting position in the taxonomy of well-structured Petri net extensions (see Fig. 1). Indeed, all their extensions forgo the decidability of the reachability problem (whether a target configuration is reachable) and of the place boundedness problem (whether the number of tokens in a given place can be bounded along all runs): this is the case of $\nu$ -Petri nets [21] that allow to create fresh data values, of ordered data Petri nets [15] that posit a dense linear ordering on $\mathbb {D}$, and of unordered data nets [15] that allow to perform ‘whole-place’ operations, which move and/or duplicate all the tokens from a place to another. By contrast, it is currently open whether reachability is decidable in UDPNs, and a consequence of our results in this paper is that place boundedness is decidable—which is a significant first step if we wish to adapt to UDPNs some of the known algorithms for reachability in Petri nets [13, 18].

Fig. 1.

A short taxonomy of some well-structured extensions of Petri nets. Complexities in violet refer to the coverability and termination problems, and can be taken as proxies for expressiveness; the exact complexities of coverability and termination in $\nu$-Petri nets and UDPNs are unknown at the moment. Place boundedness is decidable below the yellow line and undecidable above. As indicated by the dashed arrows, freshness can be enforced using a dense linear order or whole-place operations (Colour figure online).

Contributions. In this paper, we show how to construct finite coverability trees for UDPNs, adapting the existing construction of Karp and Miller [12] for Petri nets. Such trees are constructed forward from an initial configuration like reachability trees, but approximate the latter by accelerating sequences of transitions and explicitly manipulating limits of reachable configurations as downwards-closed sets (see Sect. 4.1). We rely for all this on a general theory for representing downwards-closed sets as finite unions of ideals developed by Finkel and Goubault-Larrecq [9] for this exact purpose (see Sect. 3).

Coverability trees contain a wealth of information about the system at hand, and allow to answer various coverability and boundedness questions—allowing us to derive a new result: the place boundedness problem is decidable for UDPNs, and so are its variants, like place width- and place depth boundedness (see Sect. 2). We also establish in Sect. 5 matching ‘hyper-Ackermannian’ lower and upper bounds on the size of UDPNs coverability trees. This yields $\mathbf {F}_{\omega ^\omega }$ upper bounds for the already mentioned decidable problems in UDPNs, in terms of the fast-growing complexity classes $(\mathbf {F}_\alpha )_\alpha$ from [23]. These complexity results rely largely on the work of Rosa-Velardo [20] on the complexity of coverability in unordered data nets. Due to space constraints, most proof details are omitted but can be found online in the full version of the paper available from https://hal.inria.fr/hal-01252674.

Related Work. A coverability tree construction has already been undertaken by Rosa-Velardo, Martos-Salgado, and de Frutos-Escrig [22] in the case of $\nu$-Petri nets, and inescapably there are many similarities between their work and ours. Our construction does however not merely remove freshness constraints from theirs: (1) we start a new and rely on a strong invariant on the form of ideals in UDPN coverability trees, which leads to significant simplifications but would be markedly difficult to extract from Rosa-Velardo et al.’s [22] construction, and (2) coverability trees are not necessarily finite for $\nu$-Petri nets (place boundedness is indeed undecidable [21]), which means that our termination argument and complexity bounds are entirely new considerations.

Like Rosa-Velardo et al. [22] we rely on the work of Finkel and Goubault-Larrecq [9] on forward analysis of well-structured systems. Finkel and Goubault-Larrecq provide in particular an abstract generic procedure, but without guarantee of termination in general, and their framework needs to be instantiated for each specific class of systems.

2 Model

Our presentation of unordered data Petri nets differs from the original one [15] on two counts: we work with an equivalent formalism with more of a vector addition system [12] flavour, and because we need to work with ideals we define the syntax and the semantics on extended configurations, which allow for infinitely many different data values and infinite counts.

Let $\mathbb {Z}$ and $\mathbb {N}$ denote the sets of integers and non-negative integers respectively, and complete them as $\mathbb {Z}_\omega \mathop {=}\limits ^{{\tiny {\text {def}}}}\mathbb {Z}\uplus \{\omega \}$ and $\mathbb {N}_\omega \mathop {=}\limits ^{{\tiny {\text {def}}}}\mathbb {N}\uplus \{\omega \}$ with a new top element $\omega$ with $\omega > z$ and $z\,+\,\omega =\omega \,+\,z=\omega$ for all z in $\mathbb {Z}$. Given a dimension k in $\mathbb {N}$, we denote the projection into the ith component of a vector $\varvec{v}\in \mathbb {Z}_{\omega }^k$ by $\varvec{v}[i]$ and define the product ordering and sum over $\mathbb {Z}^k_\omega$ componentwise: $\varvec{u}\le \varvec{v}$ if $\varvec{u}[i]\le \varvec{v}[i]$ for all $1\le i\le k$, and $(\varvec{u}\,+\,\varvec{v})[i]\mathop {=}\limits ^{{\tiny {\text {def}}}}\varvec{u}[i]\,+\,\varvec{v}[i]$ for all $1\le i\le k$. We write $\varvec{0}$ for the vector with 0 on all components.

Data Vectors. Fix some countable domain $\mathbb {D}$ of data values and a dimension k in $\mathbb {N}$. A data vector is a function $f{:}\,\mathbb {D}\rightarrow \mathbb {Z}_\omega ^k$. Data vectors can be partially ordered and summed pointwise: $f\le g$ if $f(d)\le g(d)$ for all d in $\mathbb {D}$, and $(f\,+\,g)(d)\mathop {=}\limits ^{{\tiny {\text {def}}}}f(d)\,+\,g(d)$ for all d in $\mathbb {D}$. As usual we write $f<g$ if $f\le g$ and $f(d) < g(d)$ for some d in $\mathbb {D}$. For a subset $K\subseteq \{1,\dots ,k\}$ we write $f{\upharpoonright _{K}}$ for the projection of f into components in K: for all d in $\mathbb {D}$, $f{\upharpoonright _{K}}(d)\mathop {=}\limits ^{{\tiny {\text {def}}}}(f(d)){\upharpoonright _{K}}$. The support of a data vector f is $Supp _{\varvec{0}}(f)\mathop {=}\limits ^{{\tiny {\text {def}}}}\{d\in \mathbb {D}\mid f(d)\ne \varvec{0}\}$; f is finitely supported if $Supp _{\varvec{0}}(f)$ is finite. We say that a data vector f is non-negative if f(d) belongs to $\mathbb {N}_\omega ^k$ for all d in $\mathbb {D}$. It is finite if f(d) belongs to $\mathbb {Z}^k$ for all d and it is finitely supported.

We call bijections $\sigma :\mathbb {D}\rightarrow \mathbb {D}$ (data) permutations and write $f\sigma$ for the composition of a permutation $\sigma$ and a data vector f. If two data vectors f, g satisfy $f = g\sigma$ for some permutation $\sigma$, we say f and g are equal up to permutation and write $f \equiv _{}g$.

In the sequel we will consider sets of data vectors that are finite up to permutation: a set X of data vectors is finite up to permutation if there is a finite subset $X'$ of X such that every $f\in X$ is equal up to permutation to some $f' \in X'$. Note that if X is closed under permutations then $X'$ can be used as its finite presentation; any such finite set $X'$ we call representative of X.

Definition 2.1

(UDPN). An unordered data Petri net (UDPN) is a finite set $\mathcal {T}$ of finite data vectors. A transition is a data vector $t\mathop {=}\limits ^{{\tiny {\text {def}}}}f\sigma$, where $f \in \mathcal {T}$ and $\sigma$ is a data permutation. There is a step $f\xrightarrow {t}g$ between non-negative data vectors f, g if $g=f\,+\,t$ for some transition t. Note that this enforces that $f(d)\,+\,t(d)\ge 0$ for all d in $\mathbb {D}$ since g is non-negative. We simply write $f\xrightarrow {}g$ if $f\xrightarrow {t}g$ for some transition t and let $\xrightarrow {*}$ denote the transitive and reflexive closure of $\xrightarrow {}$.

A configuration is a finite non-negative data vector f, i.e. f(d) belongs to $\mathbb {N}^k$ for all d in $\mathbb {D}$, and $f(d) = \varvec{0}$ for almost all d in $\mathbb {D}$. We write $Confs$ for the set of configurations and note that $Confs$ is closed under UDPN steps. The reachability set from a given vector f is defined as

$$\begin{aligned} Reach (f)\mathop {=}\limits ^{{\tiny {\text {def}}}}\{g\in Confs \mid f\xrightarrow {*}g\}. \end{aligned}$$

(1)

Observe that UDPNs over any domain with cardinality $|\mathbb {D}|=1$ are classical vector addition systems [12]. Notice also that, the set of transitions in an UDPN is finite up to permutations of $\mathbb {D}$ and that the step relation is closed under permutations: For every non-negative data vector f, transition t and permutation $\sigma$ we have that

$$\begin{aligned} f\xrightarrow {t}g \text { implies } f\sigma \xrightarrow {t\sigma } g\sigma . \end{aligned}$$

(2)

Example 2.2

For the domain $\mathbb {D}\mathop {=}\limits ^{{\tiny {\text {def}}}}\mathbb {N}$ and $k\mathop {=}\limits ^{{\tiny {\text {def}}}}2$, consider a 2-dimensional UDPN $\mathcal {T} = \{t_1, t_2\}$, with vectors $t_1,t_2$ defined as $t_1: 0 \mapsto (1,0)$ and $t_1: n\mapsto (0,0)$ for all $n>0$, and $t_2: 0 \mapsto (-1,-1)$, $t_2: 1 \mapsto (1,1)$ and $t_2: n\mapsto (0,0)$ for all $n>1$.

The configuration $f_0$ with $f_0:0\mapsto (1,1)$ and $f_0:n\mapsto (0,0)$ for $n>0$, has infinitely many $t_1$-successors. Namely, $g_i \mathop {=}\limits ^{{\tiny {\text {def}}}}f_0\,+\,t_1\sigma _i$ for every permutation $\sigma _i$ that swaps 0 and $i\in \mathbb {D}$. However, there are only two such successors up to permutation because $g_i\equiv _{}g_j$ for all $i,j>0$. The reachability set of $f_0$ is

$$\begin{aligned} Reach (f_0) = \left\{ \begin{array}{l|l} g \ &{}\ \begin{array}{l} \exists d_1,d_2,\dots ,d_m \in \mathbb {D}\ \exists n_1,n_2,\dots ,n_m \in \mathbb {N}\ \\ g(d_1) = (n_1,1) \text { and } \forall 1<i\le m,\ g(d_i) = (n_i,0), \\ \forall d\in \mathbb {D}\setminus \{d_1, d_2, \ldots , d_m\} \ g(d) = (0, 0) \end{array} \end{array} \right\} . \end{aligned}$$

(3)

In the sequel, we present UDPNs only up to permutation in matrix form by juxtaposing the vectors from their finite supports: we write $t_1\mathop {=}\limits ^{{\tiny {\text {def}}}}{\big [{\begin{matrix}1\\ 0\end{matrix}}\big ]}$, $t_2\mathop {=}\limits ^{{\tiny {\text {def}}}}{\big [{\begin{matrix}-1&{}1\\ -1&{}1\end{matrix}}\big ]}$ and $f_0\mathop {=}\limits ^{{\tiny {\text {def}}}}{\big [{\begin{matrix}1\\ 1\end{matrix}}\big ]}$. The $t_1$-successors of $f_0$ are $g_0 = {\big [{\begin{matrix}2\\ 1\end{matrix}}\big ]}$ and $g_i = {\big [{\begin{matrix}1\\ 1\end{matrix}}\big ]}\,+\,{\big [{\begin{matrix}1\\ 0\end{matrix}}\big ]} = {\big [{\begin{matrix}1&{}1\\ 1&{}0\end{matrix}}\big ]}$ for $i\ne 0$. The latter is depicted in Fig. 2 in the style of coloured place/transition nets. The reachability set of $f_0$ can be written as $Reach (f_0)= \big \{ {\big [{\begin{matrix}n_0&{}n_1&{}\cdots &{}n_m\\ 1&{}0&{}\cdots &{}0\end{matrix}}\big ]} \mid m\ge 0,n_0,\dots ,n_m\ge 1 \big \}$.

Fig. 2.

A place/transition representation of the UDPN of Example 2.2 in the style of [11, 21]. Different data values are depicted though differently coloured tokens in places (the circles), and through differently named variables in transitions (the boxes and arrows).

Embeddings. We say that a data vector f embeds into a data vector g and write $f\sqsubseteq _{}g$ (resp. $f\sqsubset g$) if there exists an injection $\pi {:}\,\mathbb {D}\rightarrow \mathbb {D}$ such that $f\le g \pi$ (resp. $f<g \pi$). The injection $\pi$ itself is called an embedding (of f into g) and a permutation embedding in case it is bijective. Given a set of configurations C, its downward-closure ${\downarrow }C$ is $\{f\in Confs \mid \exists g\in C\mathbin .f\sqsubseteq _{}g\}$, and as usual a set C is downwards-closed if ${\downarrow }C=C$.

Finitely supported data vectors are isomorphic to finite multisets of vectors in $\mathbb {Z}_\omega ^k$ when working up to data permutation. Moreover, on permutation classes of finitely supported data vectors, the embedding ordering coincides with the usual embedding ordering over finite multisets of vectors; in consequence, UDPN configurations are well-quasi-ordered by the embedding ordering. Thus an UDPN defines a quasi-ordered transition system $( Confs ,\xrightarrow {},{\sqsubseteq _{}})$, which satisfies a (strong) compatibility condition as shown in the following lemma. Together with the fact that $( Confs ,{\sqsubseteq _{}})$ is a wqo, this entails that it is a well-structured transition system in the sense of [1, 7].

Lemma 2.3

(Strong Strict Compatibility). Let $f,f',g$ be configurations. If $f\sqsubseteq _{}f'$ (resp. $f\sqsubset f'$) and $f\xrightarrow {} g$, then there exists a configuration $g'$ with $f'\xrightarrow {}g'$ and $g\sqsubseteq _{}g'$ (resp. $g\sqsubset g'$).

Proof

Consider a finite data vector t such that $f\xrightarrow {t} g$, and a permutation $\pi$ of $\mathbb {D}$ such that $f\le f'\pi$ (recall that, when working with finitely supported data vectors, embeddings can be assumed to be permutations). We claim that $g'\mathop {=}\limits ^{{\tiny {\text {def}}}}f'\,+\,t\pi ^{-1}$ satisfies $f'\xrightarrow {t\pi ^{-1}}g'$ and $g\le g'\pi$. Indeed, for all d in $\mathbb {D}$, noting $e\mathop {=}\limits ^{{\tiny {\text {def}}}}\pi (d)$,

$$\begin{aligned} g(d)&=f(d)\,+\,t(d)\le f'(\pi (d))\,+\,t(d) =f'(e)\,+\,t(\pi ^{-1}(e))=g'(e)=g'(\pi (d))\;. \end{aligned}$$

Furthermore, assuming $f< f'\pi$, for at least one d in $\mathbb {D}$ the above inequality is strict.   $\square$

Decision Problems. For the purpose of verification, we are interested in standard decision problems for UDPN, including reachability (does $f\xrightarrow {*}g$ hold for given configurations f and g?), coverability (given configurations f, g, does there exists $g'\sqsupseteq _{}g$ s.t. $f\xrightarrow {*}g'$?), and boundedness (is $Reach (f)$ finite up to permutation?).

While the decidability of reachability remains open, well-structuredness of UDPN (and some basic effectiveness assumptions) implies that the coverability and boundedness problems are decidable using the generic algorithms from [1, 7]. In fact, decidability holds more generally for ordered data Petri nets [15, Theorm 4.1]. For the coverability problem, Rosa-Velardo [20, Theorem 1] proved an HyperAckermann upper bound ($\mathbf {F}_{\omega ^\omega }$ in the hierarchy from [23]; see Sect. 5), while Lazić et al. [15, Theorem 5.2] proved a Tower lower bound ($\mathbf {F}_3$ in the same hierarchy). The complexity of the boundedness problem has not been studied before. Furthermore, the following, more precise variant of boundedness called place boundedness was not known to be decidable:

In the presence of an infinite data domain $\mathbb {D}$, place boundedness can be further refined: even if infinitely many configurations are reachable, the system can still be bounded in the sense that there exists a bound on the number of different data values in reachable configurations; Rosa-Velardo and de Frutos-Escrig [21] call this bounded width. Similarly, there may exist some bound on the multiplicities with which any data value occurs, while the number of different data values is unbounded; Rosa-Velardo and de Frutos-Escrig [21] call this bounded depth.

We formalise the resulting decision problems in our notation as follows. The place width boundedness problem is given as:

The place depth boundedness problem is the following:

If the answer to the depth (width) boundedness problem is positive we call those components $i\in K$ depth (width) bounded.

Example 2.4

From the initial configuration $f_0= {\big [{\begin{matrix}1\\ 1\end{matrix}}\big ]}$, the UDPN from Example 2.2 can reach any configuration of the form ${\big [{\begin{matrix}n\\ 1\end{matrix}}\big ]}$ in n many $t_1$-steps, all exercised on the same data value. Similarly, any configuration of the form ${\big [{\begin{matrix}1&{}1&{}\cdots &{}1\\ 1&{}0&{}\cdots &{}0\end{matrix}}\big ]}$ with a support of size $n\,+\,1$ can be reached after a sequence of n transitions $t_1$, each exercised on a different data value. Consequently, the first component is neither depth nor width bounded.

However, any reachable configuration g will satisfy $\sum _{d\in \mathbb {D}}g(d)[2]=1$. In Petri net parlance, there is always exactly one token in the second place. The system is thus place bounded for $K\mathop {=}\limits ^{{\tiny {\text {def}}}}\{2\}$.

The main contribution of this paper is the effective computability of a suitable abstraction of the classical coverability tree construction [12] for UDPNs. This provides a way to decide all variants of the boundedness problem mentioned above. We summarise the consequences of our construction below.

Theorem 2.5

In UDPNs, place depth boundedness implies place width boundedness. In consequence, place depth boundedness coincides with place boundedness.

Theorem 2.6

The boundedness, place boundedness, and place width boundedness problems for UDPNs are in $\mathbf {F}_{\omega ^\omega }$, i.e. in HyperAckermann.

Let us emphasise the importance of decidability of place boundedness: first, the problem is undecidable in all the extensions of UDPNs in Fig. 1. Moreover, in the case of Petri nets, the decidability of place boundedness plays a crucial role in the decidability proofs for reachability [13, 14, 16, 18], hence Theorem 2.6 provides one of the basic building blocks for future attempts at proving the decidability of reachability for UDPNs.

3 Simple Ideals

A key observation about all decision problems mentioned in the previous section is that they do not require computing the reachability set: they can all be solved given some suitable representation of the cover [9], defined as

$$\begin{aligned} Cover (f)\mathop {=}\limits ^{{\tiny {\text {def}}}}{\downarrow } Reach (f), \end{aligned}$$

(4)

for f the initial configuration. Indeed, coverability reduces to checking whether $g\in Cover (f)$, boundedness to checking whether $Cover (f)$ is finite up to permutation of $\mathbb {D}$, and place boundedness to checking whether $\{g{\upharpoonright _{K}}\mid g\in Cover (f)\}$ is finite up to permutation of $\mathbb {D}$. The main property of the coverability tree we construct in Sect. 4 is that we can extract a suitable representation of $Cover (f)$.

Ideals and Clovers. We refer the reader to the work of Finkel and Goubault-Larrecq [8, 9] for details; it suffices to say that downwards-closed sets of configurations can be represented as finite unions of so-called configuration ideals. Formally, a configuration ideal J is a non-empty, downwards-closed, and directed set of configurations; this last condition means that, if f and $f'$ are configurations in J, then there exists h in J with $f\sqsubseteq h$ and $f'\sqsubseteq h$. Crucially for algorithmic considerations, a configuration ideal J can in turn be represented as the downward-closure

$$\begin{aligned} J={\downarrow }g\mathop {=}\limits ^{{\tiny {\text {def}}}}\{h\in Confs \mid h\sqsubseteq _{}g\} \end{aligned}$$

(5)

of a non-negative data vector g having a finite range: $g(\mathbb {D})$ is a finite subset of $\mathbb {N}^k_\omega$. We can check that every such ${\downarrow }g$ is a configuration ideal (see [8, 9] for the converse): it is non-empty and downwards-closed by definition, and we can check it is also directed. Indeed, if f, $f'$ are configurations and $\pi$, $\pi '$ are injections with $f\le g\pi$ and $f'\le g\pi '$, then since f and $f'$ are finitely supported we can assume $\pi$ and $\pi '$ to be permutations, and we can define a configuration $h\le g$ such that $f\le h\pi$ and $f'\le h\pi '$: set h as the pointwise least upper bound $h(d)[i]\mathop {=}\limits ^{{\tiny {\text {def}}}}\max (f(\pi ^{-1}(d))[i], f'({\pi '}^{-1}(d))[i])\le g(d)[i]$ for all d and $1\le i\le k$.

$Cover (f)$, being downwards-closed, is represented by a finite set of representations of configuration ideals, called $Clover (f)$ by Finkel and Goubault-Larrecq:

$$\begin{aligned} Cover (f) = \bigcup \{ {\downarrow }g \mid g \in Clover (f)\}\;. \end{aligned}$$

$Clover (f)$ is determined uniquely up to permutation, and contains $\sqsubseteq _{}$-maximal data vectors g satisfying ${\downarrow }g \subseteq Cover (f)$; for further details see [8, 9]. In the following we identify a configuration ideal $J={\downarrow }g$ with its representation g.

Remark 3.1

(Ideals for Petri nets). For readers familiar with Karp and Miller’s coverability trees for Petri nets, observe that configuration ideal representations generalise the notion of ‘extended markings’, which are vectors in $\mathbb {N}^k_\omega$. Also, $Clover (f)$ for a Petri net can be computed as the set of vertex labels in its coverability tree—this will also be our case.

Simple Ideals. Crucially, it turns out that we do not need general configuration ideals for our coverability trees for UDPNs. We only need to consider the downward-closures ${\downarrow }g$ of non-negative vectors g (cf. (5)), where the set of vectors appearing infinitely often as g(d), when d ranges over $\mathbb {D}$, is a singleton $\{\varvec{I}\}$ for some vector $\varvec{I}$ in $\{0,\omega \}^k$ (instead of a finite subset of $\mathbb {N}_{\omega }^k$ for general configuration ideals). Put differently, given such a vector $\varvec{I}$, we define the $\varvec{I}$ -support of a data vector f as $Supp _{\varvec{I}}(f)\mathop {=}\limits ^{{\tiny {\text {def}}}}\{d\in \mathbb {D}\mid f(d)\ne \varvec{I}\}$, and define an $\varvec{I}$ -simple ideal (representation) as a non-negative data vector with finite $\varvec{I}$-support. In particular, a finitely supported non-negative data vector is a $\varvec{0}$-simple ideal. We write M, N, ... to denote simple ideals. A simple ideal M can be represented concretely as a pair $M=\langle m,\varvec{I}\rangle$ where m is the finite multiset of vectors in $\mathbb {N}_{\omega }^k$ obtained from M by restriction to its $\varvec{I}$-support.

Example 3.2

We represent simple ideals similarly as configurations, using the additional last column for the $\varvec{I}$ part. Continuing with the UDPN of Example 2.2, its cover is the downward-closure of a single $\varvec{I}$-simple ideal:

$$\begin{aligned} Clover (f_0)&={\big [{\begin{matrix}\omega \\ 1\end{matrix}}\big |{\begin{matrix}\omega \\ 0\end{matrix}}\big ]}\;,&Cover (f_0)&={\downarrow }{\big [{\begin{matrix}\omega \\ 1\end{matrix}}\big |{\begin{matrix}\omega \\ 0\end{matrix}}\big ]}\;, \end{aligned}$$

where $\varvec{I}\mathop {=}\limits ^{{\tiny {\text {def}}}}(\omega ,0)$. The $\varvec{I}$-support of the ideal has one element, mapped to $(\omega ,1)$.

Note that UDPN steps map $\varvec{I}$-simple ideals to $\varvec{I}$-simple ideals. Lemma 3.3 formally states the relation between steps of ideals and steps of configurations in the downward closures. The next lemma shows that $\varvec{I}$-simple ideals can only have finitely many successors up to permutation. This property will later be used to define coverability trees of finite branching degree.

Lemma 3.3

Let $M,M'$ be $\varvec{I}$-simple ideals such that $M\xrightarrow {}M'$. Then for every configuration $c'\in {\downarrow }M'$ there exist configurations $c\in {\downarrow }M$ and $c''\in {\downarrow }M'$ with $c\xrightarrow {}c''$ and $c'\sqsubseteq _{}c''$.

Proof

Suppose $M \xrightarrow {t}M'$ for a finite data vector t. The data vector $f \mathop {=}\limits ^{{\tiny {\text {def}}}}c' - t$ satisfies $f\le M$ but f(d) can possibly be negative for some data value d; therefore we can not simply put $c \mathop {=}\limits ^{{\tiny {\text {def}}}}f$. A way to fix this is to define c by

$$ c(d)[i] \mathop {=}\limits ^{{\tiny {\text {def}}}}\max (0,x(d)[i]), \quad \text { for all } d\in \mathbb {D}\text { and all coordinates } i. $$

Thus defined, c satisfies $c\le M$, and setting $c''\mathop {=}\limits ^{{\tiny {\text {def}}}}c\,+\,t$ satisfies $c'\le c''$ as required.   $\square$

Lemma 3.4

Let M be a simple ideal. The set $\{ N \mid M \xrightarrow {} N \}$ of successors of M is finite up to permutation and has a representative with cardinality bounded by $(| Supp _{\varvec{I}}(M)|+\max _{t\in \mathcal {T}}| Supp _{\varvec{0}}(t)|)!\cdot |\mathcal {T}|^2$.

Proof

Consider an UDPN defined by the finite set $\mathcal {T}$ of data vectors. Fix an $\varvec{I}$-simple ideal M, and denote by S the $\varvec{I}$-support of M. We will be now considering S-permutations, by which we mean those data permutations $\pi$ that satisfy $\pi (d) = d$ for all $d\in S$. Equality and finiteness up to S-permutation can be defined exactly as for plain permutations.

A crucial but simple observation is that the set of transitions of the UDPN is finite up to S-permutation. Indeed, assume wlog. that S is disjoint from the supports of all vectors in $\mathcal {T}$. Consider the finite set $\mathcal {T}'$ that contains all data vectors $t\sigma$, where $t \in \mathcal {T}$ and permutation $\sigma$ swaps some subset of S with some subset of the support of t. Then every transition of the UDPN is of the form $t'\pi$, where $t'\in \mathcal {T}'$ and $\pi$ is an S-permutation. Regarding the size of this new UDPN, there are at most $\sum _{t\in \mathcal {T}}(|S|+| Supp _{\varvec{0}}(t)|)!$ such permutations $\sigma$, hence $|\mathcal {T}'|\le \sum _{t\in \mathcal {T}}(|S|+| Supp _{\varvec{0}}(t)|)!\cdot |\mathcal {T}|$.

Now we use the extension, to simple ideals, of the closure of the step relation under permutations, cf. Eq. (2), to derive a strengthening of our claim, namely finiteness of the successors of M up to S-permutations. Consider an arbitrary step $M\xrightarrow {t'\pi }N$ of M; by  Eq. (2) we get

$$\begin{aligned} M = M\pi ^{-1} \xrightarrow {t'} N\pi ^{-1} \end{aligned}$$

(the equality holds as $\pi$ is an S-permutation). Therefore N is equal up to S-permutation to some $\mathcal {T}'$-successor of M. As $\mathcal {T}'$ is finite, the set of $\mathcal {T}'$-successors of M is finite and bounded by $|\mathcal {T}'|$, which implies our claim.   $\square$

A consequence of our construction of coverability trees in Sect. 4, and of the complexity analysis conducted in Sect. 5, is the following core result:

Theorem 3.5

Given an UDPN and an initial configuration f, an ideal representation $Clover (f)$ of $Cover (f)$ is computable in $\mathbf {F}_{\omega ^\omega }$. Furthermore, $Clover (f)$ contains only simple ideals.

Theorem 3.5, together with the following proposition, easily imply Theorems 2.5 and 2.6 (below ${ Clover (f)}{\upharpoonright _{K}} \mathop {=}\limits ^{{\tiny {\text {def}}}}\{ g{\upharpoonright _{K}} \mid g\in Clover (f)\}$):

Proposition 3.6

Fix $K \subseteq \{1, \ldots , k\}$. An UDPN is width-bounded iff ${ Clover (f)}{\upharpoonright _{K}}$ contains only finitely supported vectors. An UDPN is depth-bounded iff $Clover (f){\upharpoonright _{K}}$ contains only finite vectors.

Proof

The former equivalence, as well as the if direction of the latter one, follow by finiteness of $Clover (f){\upharpoonright _{K}}$. It remains to argue that place depth-boundedness forces $Clover (f){\upharpoonright _{K}}$ to contain only finite vectors. Indeed, a non-finite simple ideal has necessarily $\omega$ at some component, which implies depth-unboundedness.   $\square$

The remaining part of the paper is devoted to the proof of Theorem 3.5. In Sect. 4, we present an algorithmic construction of the coverability tree, and show its termination and correctness. Then in Sect. 5 we provide upper and lower bounds on the size of the coverability tree.

4 Representing a Cover

We will show that, analogously to the classical construction of Karp and Miller [12] for vector addition systems, the cover set of any UDPN configuration can be effectively represented in the form of a finite coverability tree, where nodes are labelled by simple ideals.

For a given initial ideal the construction of a coverability tree amounts to iteratively computing successors (up to permutation), applying symbolic acceleration steps when a strictly dominating pair $M \sqsubset M'$ appears on a branch, and terminating a branch if a label embeds into one of its ancestors.

4.1 Accelerations

The idea behind acceleration steps is that due to monotonicity (Lemma 2.3), any finite sequence of steps

$$\begin{aligned} M_0\xrightarrow {t_1}M_1\xrightarrow {t_2}\dots \xrightarrow {t_k}M_k \end{aligned}$$

(6)

such that $M_0\sqsubset M_k$ can be extended indefinitely. Such an unfolding may have two distinct kinds of effect: Firstly, it may unboundedly increase components in data values already contained in the initial $\varvec{I}$-support (we call this effect depth acceleration). Secondly, it may increase an unbounded number of ‘fresh’ data values, outside of the initial $\varvec{I}$-support (we call this effect width acceleration). Our construction only accelerates increasing sequences as above when there is a permutation (i.e. bijective) embedding of $M_0$ into $M_k$.

As a building block we shall use the usual vector acceleration: for two non-negative vectors $\varvec{v}, \varvec{v}' \in \mathbb {N}_\omega ^k$ with $\varvec{v}' \le \varvec{v}$, define a new vector $\text {acc}(\varvec{v}', \varvec{v})$, for $1 \le i \le k$ by:

$$\begin{aligned} \text {acc}(\varvec{v}', \varvec{v})[i] \mathop {=}\limits ^{{\tiny {\text {def}}}}{\left\{ \begin{array}{ll} \varvec{v}[i], &{}\text {if } \varvec{v}'[i]=\varvec{v}[i],\\ \omega , &{}\text {if } \varvec{v}'[i]<\varvec{v}[i]. \end{array}\right. } \end{aligned}$$

Definition 4.1

(Depth and Width Acceleration). For $\varvec{I}$-simple ideals $M'$, M and a permutation $\pi$ with $M' < M\pi$, or equivalently $M'\pi ^{-1} < M$, the depth acceleration of $M',M,\pi$ is the $\varvec{I}$-simple ideal defined by

$$\begin{aligned} M_\text {depth}(d)\mathop {=}\limits ^{{\tiny {\text {def}}}}\text {acc}(M'(\pi ^{-1}(d)), M(d)), \qquad \text { for all data values } d\in \mathbb {D}. \end{aligned}$$

For $d\in \mathbb {D}$ such that $M'(\pi ^{-1}(d)) = \varvec{I} < M(d)$, put $\varvec{I}_d \mathop {=}\limits ^{{\tiny {\text {def}}}}\text {acc}(M'(\pi ^{-1}(d)), M(d))$; the width acceleration of $M',M,\pi , d$ is the $\varvec{I}_d$-simple ideal defined by

$$\begin{aligned} M_\text {width}(d)\mathop {=}\limits ^{{\tiny {\text {def}}}}{\left\{ \begin{array}{ll} \varvec{I}_d, &{}\text { if } M(d) = \varvec{I} \\ M(d), &{}\text { otherwise,} \end{array}\right. } \end{aligned}$$

By definition, $M < M_\text {depth}, M_\text {width}$.

4.2 Coverability Trees

By Lemma 3.4 we can compute for any $\varvec{I}$-simple ideal M a successor representative, namely a finite set such that every successor of M is equal up to permutation to some element of this set.

For the sake of simplicity, we choose a conservative policy of application of accelerations: first, a proper nesting is imposed, in the sense that two different accelerated paths are either disjoint, or contained one in the other; second, a depth-accelerated path can not contain another accelerated path, while a width-accelerated path can. However, as width accelerations strictly increase the $\varvec{I}$ part, a width-accelerated path is never contained in another accelerated path. Therefore the only allowed inclusion is when a depth-accelerated path is included in a width-accelerated one.

Definition 4.2

(Coverability Tree). A coverability tree is a tree with nodes labelled by simple ideals such that the following criteria are satisfied.

• 1. A node with label N is a leaf iff it has an ancestor with label $N'\sqsupseteq _{}N$.

• 2. Otherwise, suppose an interior node N has an ancestor $N'$ such that both $N'$, N are $\varvec{I}$-simple and $N' \sqsubset N$. Let $\mathcal P$ denote the path from $N'$ to N in the tree, including $N'$ and N.

  • (a) Suppose $N'(\pi ^{-1}(d)) = \varvec{I} < N(d)$ for some permutation $\pi$ with $N'\pi < N$ and $d\in \mathbb {D}$; and for every node in $\mathcal P$ that is a depth acceleration of some nodes $M', M$, both $M'$ and M belong to $\mathcal P$. Then N has exactly one child labelled by the width acceleration of $N',N,\pi ,d$.

  • (b) Otherwise, if $\mathcal P$ contains no acceleration then N has exactly one child labelled by the depth acceleration of $N',N,\pi$, for some permutation $\pi$ with $N'\pi < N$.

• 3. Otherwise, if a node N satisfies none of the above criteria then its set of children is the successor representative of N.

Remark 4.3

Note that Definition 4.2 does not determine the coverability tree unambiguously: the choice of a permutation $\pi$ in points 2(a) and 2(b) is not unique.

Remark 4.4

The condition in point 1 in Definition 4.2 implies that no branch of a coverability tree contains two different nodes with the same label. We identify a node with its label in the sequel.

Example 4.5

We pick some coverability tree for the UDPN from Example 2.2 rooted in the configuration $f_0$. There is a branch with labels (up to permutation)

$$\begin{aligned} f_0\!=\!{\big [{\begin{matrix}1\\ 1\end{matrix}}\big |{\begin{matrix}0\\ 0\end{matrix}}\big ]}, \, f_1\!=\!{\big [{\begin{matrix}2\\ 1\end{matrix}}\big |{\begin{matrix}0\\ 0\end{matrix}}\big ]}, \, f_2\!=\!{\big [{\begin{matrix}\omega \\ 1\end{matrix}}\big |{\begin{matrix}0\\ 0\end{matrix}}\big ]}, \, f_3\!=\!{\big [{\begin{matrix}\omega &{}1\\ 0&{}1\end{matrix}}\big |{\begin{matrix}0\\ 0\end{matrix}}\big ]}, \, f_4\!=\!{\big [{\begin{matrix}\omega &{}1\\ 0&{}1\end{matrix}}\big |{\begin{matrix}\omega \\ 0\end{matrix}}\big ]}, \, f_5\!=\!{\big [{\begin{matrix}\omega &{}1&{}1\\ 0&{}1&{}0\end{matrix}}\big |{\begin{matrix}\omega \\ 0\end{matrix}}\big ]}, \end{aligned}$$

where $f_2$ is a depth acceleration (of $f_0,f_1$), $f_4$ is a width acceleration (of $f_0,f_3$), and all other nodes are the result of successor steps from their parent. The node $f_5$ is a leaf because $f_5\sqsubseteq _{}f_4$.

Correctness. A coverability tree is finite (termination), and represents the cover of its root node (completeness and soundness). These required properties are proven in detail in the full paper:

• Finiteness is proven by first exhibiting a wqo for the specific type of $\varvec{I}$-simple ideals that appears on coverability trees. This wqo depends on the existence of permutation embeddings, a property that on its own does not induce a well-quasi-ordering over the set of all $\varvec{I}$-simple ideals. Our termination argument is further refined to derive complexity bounds; see Sect. 5.2.

• The completeness proof relies on the monotonicity of steps over simple ideals, and shows that all the elements in $Cover (f)$ are covered by some simple ideal in any coverability tree.

• Soundness is the most delicate property to establish. Its crux is that neither width nor depth accelerations may take us outside the cover of the initial configuration.

5 Complexity Bounds

In the section, we prove lower and upper bounds on the resources needed by the construction of the coverability tree. We refer the reader to [24, 25] for gentle introductions to the techniques employed to prove these results. The enormous complexities involved in our construction require to use fast-growing complexity classes [23], which we present succinctly in Sect. 5.1 and in more details in the full paper, before showing hyper-Ackermannian upper and lower bounds in Sects. 5.2 and 5.3.

5.1 Fast-Growing Complexity

In order to express the non-elementary functions required for our complexity statements, we shall employ a family of subrecursive functions $(h^\alpha )_\alpha$ indexed by ordinals $\alpha$ known as the Hardy hierarchy.

Ordinal Terms. We use ordinal terms $\alpha$ in Cantor Normal Form (CNF), which can be written as terms $\alpha = \omega ^{\alpha _1}+\cdots +\omega ^{\alpha _n}$ where $\alpha _1\ge \cdots \ge \alpha _n$ are themselves written in CNF. Using such notations, we can express any ordinal below $\varepsilon _0$, the minimal fixpoint of $x=\omega ^x$. The ordinal 0 is obtained when $n=0$; otherwise if $\alpha _n=0$ the ordinal $\alpha$ is a successor ordinal $\omega ^{\alpha _1}+\cdots +\omega ^{\alpha _{n-1}}+1$, and if $\alpha _n>0$ the ordinal $\alpha$ is a limit ordinal. We usually write $\lambda$ to denote limit ordinals.

Fundamental Sequences. For all x in $\mathbb {N}$ and limit ordinals $\lambda$, we use a standard assignment of fundamental sequences $\lambda (0)<\lambda (1)<\cdots <\lambda (x)<\cdots <\lambda$ with supremum $\lambda$. Fundamental sequences are defined by transfinite induction by:

$$\begin{aligned} (\gamma +\omega ^{\beta +1})(x)&\mathop {=}\limits ^{{\tiny {\text {def}}}}\gamma +\omega ^\beta \cdot (x+1)\;,&(\gamma +\omega ^{\lambda '})(x)&\mathop {=}\limits ^{{\tiny {\text {def}}}}\gamma +\omega ^{\lambda '(x)}\;. \end{aligned}$$

(7)

For instance, $\omega (x)=x+1$, $\omega ^{2}(x)=\omega \cdot (x+1)$, $\omega ^{\omega }(x)=\omega ^{x+1}$, etc.

The Hardy Hierarchy. Let $h{:}\,\mathbb {N}\rightarrow \mathbb {N}$ be a strictly increasing function. The Hardy functions $(h^\alpha {:}\,\mathbb {N}\rightarrow \mathbb {N})_\alpha$ are defined by transfinite induction on their ordinal indices by

$$\begin{aligned} h^0(x)&\mathop {=}\limits ^{{\tiny {\text {def}}}}x\;,&h^{\alpha +1}(x)&\mathop {=}\limits ^{{\tiny {\text {def}}}}h^\alpha (h(x))\;,&h^{\lambda }(x)&\mathop {=}\limits ^{{\tiny {\text {def}}}}h^{\lambda (x)}(x)\;. \end{aligned}$$

(8)

Observe that $h^k(x)$ for a finite k is simply the kth iterate of h. For limit ordinals $\lambda$, $h^\lambda (x)$ performs a form of diagonalisation: for instance, setting $H(x)\mathop {=}\limits ^{{\tiny {\text {def}}}}x\,+\,1$ the successor function, $H^\omega (x)=H^{x\,+\,1}(x)=2x\,+\,1$, $H^{\omega ^2}(x)=2^{x\,+\,1}(x\,+\,1)-1$ is a function of exponential growth, while $H^{\omega ^3}$ is a non elementary function akin to a tower of exponentials of height x, $H^{\omega ^\omega }$ is a non primitive-recursive function with growth similar to the Ackermann function, and $H^{\omega ^{\omega ^\omega }}$ is a non multiply-recursive function characteristic of hyper-Ackermannian complexity.

Complexity Classes. Following [23], we can define complexity classes for computations with time or space resources bounded by Hardy functions of the size of the input. We concentrate in this paper on the HyperAckermann complexity class. Let FMR denote the set of multiply-recursive functions and let h be any multiply-recursive strictly increasing function, then [23, Theorem 4.2]:

$$\begin{aligned} \textsc {HyperAckermann}\mathop {=}\limits ^{{\tiny {\text {def}}}}\mathbf {F}_{\omega ^\omega }=\bigcup _{m\in \textsc {FMR}}\textsc {DTime}(h^{\omega ^{\omega ^\omega }}(m(n))) \end{aligned}$$

(9)

is the set of decision problems solvable with resources bounded by an hyper-Ackermannian function applied to a multiply-recursive function m of the size of the input. This class is closed under multiply-recursive reductions, and several problems are known to be complete for it (see Sect. 6.2 of [23] for a survey), including coverability in unordered data nets [20].

5.2 Upper Bounds

We focus on the worst-case norm of the constructed simple ideals, from which bounds on the total size of the coverability tree and the complexity upper bound in Theorem 3.5 can both be derived.

Norms of Simple Ideals. For a vector $\varvec{u}$ in $\mathbb {Z}_\omega ^k$, its norm is its maximal finite absolute value: $||\varvec{v}||_{}\mathop {=}\limits ^{{\tiny {\text {def}}}}\max \{|\varvec{v}[i]|\,\mid 1\le i\le k\wedge \varvec{v}[i]\ne \omega \}$. Observe that, if $\varvec{I}$ is in $\{0,\omega \}^k$, then $||\varvec{I}||_{}=0$. For an $\varvec{I}$-simple ideal M, and thus for finitely supported ones in particular, we define its norm as the maximum between the cardinality of its support and the maximal norm of its vectors: $||M||_{}\mathop {=}\limits ^{{\tiny {\text {def}}}}\max \{| Supp _{\varvec{I}}(M)|, ||M(d)||_{}\,\mid d\in \mathbb {D}\}$. Note that the vectors for data d outside the support have all norm 0. In the full paper, we exhibit a bound $B\mathop {=}\limits ^{{\tiny {\text {def}}}}h^{\omega ^{\omega ^{k+3}}}(||f_0||_{})$ on the norms of all the simple ideals constructed in a coverability tree rooted by $f_0$ as defined in Definition 4.2, where h also depends on the UDPN:

Theorem 5.1

The norms of the simple ideals in a coverability tree rooted in a configuration $f_0$ for a k-dimensional UDPN $\mathcal T$ are bounded by $h^{\omega ^{\omega ^{k+3}}}\!(||f_0||_{})$, where h(x) is an elementary function of x, k, and $||\mathcal {T}||_{}$.

The main technical ingredients for Theorem 5.1 are combinatorial statements on the lengths of so-called controlled bad sequences proven by Rosa-Velardo [20, Appendix A] for finite multisets of vectors of natural numbers. Our proofs require however a substantial amount of work on top of that of Rosa-Velardo’s for two reasons: we work with extended vectors in $\mathbb {N}_\omega ^k$, and use permutation embeddings rather than just plain embeddings.

Relating Norms with Sizes and Complexity. The norm $||M||_{}\le B$ of a simple ideal M is directly related to the size of its concrete binary representation: the latter needs at most $||M||_{}\cdot k\cdot (\lceil \log ||M||_{}\rceil \,+\,1)$ bits for the $\varvec{I}$ supported part of the ideal and k bits for the $\varvec{I}$ vector itself. We can also bound the length of the branches in our coverability trees: there are indeed at most $(B+2)^{kB}\cdot 2^k$ different simple ideals with norm $\le B$, and no two interior nodes on a branch are labelled by the same ideal due to condition 1 in Definition 4.2 (see  Remark 4.4). Finally, by Lemma 3.4, the branching degree of the coverability tree is bounded by an exponential function $(B\,+\,||\mathcal {T}||_{})!\cdot |\mathcal {T}|^2$ in B and the size of $\mathcal {T}$. These three observations combined allow to bound the size of the coverability tree:

Theorem 5.2

(Size of Coverability Trees). The size of a coverability tree built from an initial configuration $f_0$ for a k-dimensional UDPN $\mathcal T$ is bounded by an elementary function of B, k, and the size of $\mathcal {T}$.

Theorem 5.2 along with Eq. (9) and the completeness and soundness of coverability trees yields the proof of Theorem 3.5, using the fact that $\mathbf {F}_{\omega ^\omega }$ is closed under elementary reductions [23, Theorem 4.7].

5.3 Lower Bounds

The sheer complexity bounds we just obtained on the size of coverability trees beg the question whether they are the best possible. We show in Theorem 5.3 that, indeed, the size of coverability trees for a family of UDPNs is provably non multiply-recursive, matching essentially the statement of Theorem 5.2:

Theorem 5.3

(Hyper-Ackermannian Coverability Trees). There exists families of O(k)-sized UDPNs $(\mathcal {T}_k)_k$ and $O(k\,+\,\log n)$-sized initial configurations $(f_{k,n})_{k,n}$, whose coverability trees are of size at least $H^{\omega ^{\omega ^k}}(n)$.

Hardy Computations. As detailed in the full paper, we prove Theorem 5.3 by ‘implementing’ the computation of Hardy functions $H^{\omega ^{\omega ^k}}$ in nets $\mathcal {T}_k$. The main idea, first developed in [11, 24], is to see the equations in (8) for $0<\alpha$ as rewriting rules operating on pairs $(\alpha ,n)$:

$$\begin{aligned} (\alpha \,+\,1,n)&\rightarrow (\alpha ,n\,+\,1)\;,&(\lambda ,n)&\rightarrow (\lambda (n),n)\;. \end{aligned}$$

(10)

Note that a sequence $(\alpha _0,n_0)\rightarrow (\alpha _1,n_1)\rightarrow \cdots \rightarrow (\alpha _i,n_i)\rightarrow \cdots$ of rewriting steps maintains $H^{\alpha _i}(n_i)=H^{\alpha _0}(n_0)$ for all i, and must eventually terminate at some rank $\ell$ with $\alpha _\ell =0$ since $\alpha _i>\alpha _{i+1}$ for all i, and then $n_\ell =H^{\alpha _0}(n_0)$.

Using a natural representation of ordinals $\alpha <\omega ^{\omega ^k}$ as finite multisets of vectors also employed by Rosa-Velardo [20], a pair $(\alpha ,n)$ can be encoded as a configuration of $\mathcal {T}_k$, and the rewriting rules of (10) can be implemented on such codes by steps of $\mathcal {T}_k$. This is however not a perfect implementation: many incorrect computations yielding results different from $H^{\omega ^{\omega ^k}}(n)=H^{\omega ^{\omega ^{k-1}\cdot (n+1)}}(n)$ are possible. The crucial point is that there exists a perfect computation in $\mathcal {T}_k$, of length at least $H^{\omega ^{\omega ^k}}(n)$. Furthermore, this computation does not allow any acceleration step, and has therefore to occur as such in any coverability tree.

6 Concluding Remarks

In this paper, we have presented a procedure to construct coverability trees for UDPNs in the style of Karp and Miller [12]. This yields decision procedures for coverability and several variants of the boundedness problem including place-boundedness, depth- and width place-boundedness. Besides its interest for the formal verification of UDPNs, this paves the way towards future attempts at proving the decidability of reachability along the lines developed for Petri nets in [13, 14, 16, 18].

We have derived hyper-Ackermannian upper bounds on the complexity of our construction, and shown that such enormous complexities are actually attained on some UDPNs. Note that this however does not provide a lower bound

• on the size of $Clover (f)$, for which the best known bound is an Ackermannian lower bound adapted from the case of Petri nets [4], nor

• on the complexity of the various boundedness problems on UDPNs, for which the best lower bound is hardness for $\textsc {Tower}=\mathbf {F}_3$, adapted from the coverability problem [15].

We actually suspect that much lower complexities that HyperAckermann could be obtained for the coverability and boundedness problems. For instance, in the case of Petri nets, coverability trees have a worst-case Ackermannian size [4, 6], but coverability, boundedness, and place-boundedness are all ExpSpace-complete [2, 5, 17, 19].