Coverability Trees for Petri Nets with Unordered Data
 8 Citations
 461 Downloads
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 wellstructured 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 HyperAckermann bounds on the size of coverability trees and on the running time of the induced decision procedures.
Keywords
Coverability Tree Data Vector Simple Ideal Configuration Ideal Limit Ordinal1 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 nonequality 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 wellstructured ones [1, 7]. As such, they still enjoy decision procedures for several verification problems, prominently safety (through the coverability problem) and termination.
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 downwardsclosed sets (see Sect. 4.1). We rely for all this on a general theory for representing downwardsclosed sets as finite unions of ideals developed by Finkel and GoubaultLarrecq [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 ‘hyperAckermannian’ 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 fastgrowing complexity classes \((\mathbf {F}_\alpha )_\alpha \) from [23]. These complexity results rely largely on the work of RosaVelardo [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/hal01252674.
Related Work. A coverability tree construction has already been undertaken by RosaVelardo, MartosSalgado, and de FrutosEscrig [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 RosaVelardo 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 RosaVelardo et al. [22] we rely on the work of Finkel and GoubaultLarrecq [9] on forward analysis of wellstructured systems. Finkel and GoubaultLarrecq 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 nonnegative 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 nonnegative 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 nonnegative 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 nonnegative. 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 {}\).
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 2dimensional 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\).
Embeddings. We say that a data vector fembeds 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 downwardclosure\({\downarrow }C\) is \(\{f\in Confs \mid \exists g\in C\mathbin .f\sqsubseteq _{}g\}\), and as usual a set C is downwardsclosed 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 wellquasiordered by the embedding ordering. Thus an UDPN defines a quasiordered 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 wellstructured 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
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?).
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; RosaVelardo and de FrutosEscrig [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; RosaVelardo and de FrutosEscrig [21] call this bounded depth.
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
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 downwardclosures \({\downarrow }g\) of nonnegative 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 nonnegative data vector with finite \(\varvec{I}\)support. In particular, a finitely supported nonnegative 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
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
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 Spermutations, by which we mean those data permutations \(\pi \) that satisfy \(\pi (d) = d\) for all \(d\in S\). Equality and finiteness up to Spermutation 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 Spermutation. 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 Spermutation. 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}\).
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 widthbounded iff \({ Clover (f)}{\upharpoonright _{K}}\) contains only finitely supported vectors. An UDPN is depthbounded 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 depthboundedness forces \( Clover (f){\upharpoonright _{K}}\) to contain only finite vectors. Indeed, a nonfinite simple ideal has necessarily \(\omega \) at some component, which implies depthunboundedness. \(\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
Definition 4.1
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 depthaccelerated path can not contain another accelerated path, while a widthaccelerated path can. However, as width accelerations strictly increase the \(\varvec{I}\) part, a widthaccelerated path is never contained in another accelerated path. Therefore the only allowed inclusion is when a depthaccelerated path is included in a widthaccelerated 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\).
 (a)
 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

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 wellquasiordering 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 fastgrowing complexity classes [23], which we present succinctly in Sect. 5.1 and in more details in the full paper, before showing hyperAckermannian upper and lower bounds in Sects. 5.2 and 5.3.
5.1 FastGrowing Complexity
In order to express the nonelementary 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 _{n1}}+1\), and if \(\alpha _n>0\) the ordinal \(\alpha \) is a limit ordinal. We usually write \(\lambda \) to denote limit ordinals.
5.2 Upper Bounds
We focus on the worstcase 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 kdimensional 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 socalled controlled bad sequences proven by RosaVelardo [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 RosaVelardo’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 kdimensional 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 multiplyrecursive, matching essentially the statement of Theorem 5.2:
Theorem 5.3
(HyperAckermannian 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)\).
Using a natural representation of ordinals \(\alpha <\omega ^{\omega ^k}\) as finite multisets of vectors also employed by RosaVelardo [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 ^{k1}\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 placeboundedness, depth and width placeboundedness. 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].

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 worstcase Ackermannian size [4, 6], but coverability, boundedness, and placeboundedness are all ExpSpacecomplete [2, 5, 17, 19].
References
 1.Abdulla, P.A., Čerāns, K., Jonsson, B., Tsay, Y.K.: Algorithmic analysis of programs with well quasiordered domains. Inform. and Comput. 160(1–2), 109–127 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
 2.Blockelet, M., Schmitz, S.: Model checking coverability graphs of vector addition systems. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol. 6907, pp. 108–119. Springer, Heidelberg (2011)CrossRefGoogle Scholar
 3.Bojańczyk, M., Klin, B., Lasota, S.: Automata theory in nominal sets. Logic. Meth. Comput. Sci. 10(3:4), 1–44 (2014)MathSciNetzbMATHGoogle Scholar
 4.Cardoza, E., Lipton, R.J., Meyer, A.R.: Exponential space complete problems for Petri nets and commutative semigroups: preliminary report. In: STOC 1976, pp. 50–54. ACM (1976)Google Scholar
 5.Demri, S.: On selective unboundedness of VASS. J. Comput. Syst. Sci. 79(5), 689–713 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
 6.Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and primitiverecursive bounds with Dickson’s Lemma. In: LICS 2011, pp. 269–278. IEEE Press (2011)Google Scholar
 7.Finkel, A., Schnoebelen, P.: Wellstructured transition systems everywhere!. Theor. Comput. Sci. 256(1–2), 63–92 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
 8.Finkel, A., GoubaultLarrecq, J.: Forward analysis for WSTS, part I: completions. In: STACS 2009. LIPIcs, vol. 3, pp. 433–444. LZI (2009)Google Scholar
 9.Finkel, A., GoubaultLarrecq, J.: Forward analysis for WSTS, part II: complete WSTS. Logic. Meth. Comput. Sci. 8(3:28), 1–35 (2012)MathSciNetzbMATHGoogle Scholar
 10.Finkel, A., McKenzie, P., Picaronny, C.: A wellstructured framework for analysing Petri net extensions. Inform. and Comput. 195(1–2), 1–29 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
 11.Haddad, S., Schmitz, S., Schnoebelen, P.: The ordinal recursive complexity of timedarc Petri nets, data nets, and other enriched nets. In: LICS 2012, pp. 355–364. IEEE Press (2012)Google Scholar
 12.Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969)MathSciNetCrossRefzbMATHGoogle Scholar
 13.Kosaraju, S.R.: Decidability of reachability in vector addition systems. In: Proceedings STOC 1982, pp. 267–281. ACM (1982)Google Scholar
 14.Lambert, J.L.: A structure to decide reachability in Petri nets. Theor. Comput. Sci. 99(1), 79–104 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
 15.Lazić, R., Newcomb, T., Ouaknine, J., Roscoe, A., Worrell, J.: Nets with tokens which carry data. Fund. Inform. 88(3), 251–274 (2008)MathSciNetzbMATHGoogle Scholar
 16.Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: LICS 2015, pp. 56–67. IEEE Press (2015)Google Scholar
 17.Lipton, R.: The reachability problem requires exponential space. Technical Report 62, Yale University (1976)Google Scholar
 18.Mayr, E.W.: An algorithm for the general Petri net reachability problem. In: Proceedings STOC 1981, pp. 238–246. ACM (1981)Google Scholar
 19.Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6(2), 223–231 (1978)MathSciNetCrossRefzbMATHGoogle Scholar
 20.RosaVelardo, F.: Ordinal recursive complexity of unordered data nets. Technical Report TR414, Departamento de Sistemas Informáticos y Computación, Universidad Complutense de Madrid (2014). http://antares.sip.ucm.es/frosa/docs/complexityUDN.pdf
 21.RosaVelardo, F., de FrutosEscrig, D.: Decidability and complexity of Petri nets with unordered data. Theor. Comput. Sci. 412(34), 4439–4451 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
 22.RosaVelardo, F., MartosSalgado, M., de FrutosEscrig, D.: Accelerations for the coverability set of Petri nets with names. Fund. Inform. 113(3–4), 313–341 (2011)MathSciNetzbMATHGoogle Scholar
 23.Schmitz, S.: Complexity hierarchies beyond elementary. ACM Trans. Comput. Theor. (2016) (to appear). http://arxiv.org/abs/1312.5686
 24.Schmitz, S., Schnoebelen, P.: Algorithmic aspects of WQO theory. Lecture notes (2012).http://cel.archivesouvertes.fr/cel00727025
 25.Schmitz, S., Schnoebelen, P.: The power of wellstructured systems. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 5–24. Springer, Heidelberg (2013)CrossRefGoogle Scholar
 26.Schnoebelen, P.: Revisiting Ackermannhardness for lossy counter machines and reset Petri nets. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 616–628. Springer, Heidelberg (2010)CrossRefGoogle Scholar