Decidability Border for Petri Nets with Data: WQO Dichotomy Conjecture

Abstract

In Petri nets with data, every token carries a data value, and executability of a transition is conditioned by a relation between data values involved. Decidability status of various decision problems for Petri nets with data may depend on the structure of data domain. For instance, if data values are only tested for equality, decidability status of the reachability problem is unknown (but decidability is conjectured). On the other hand, the reachability problem is undecidable if data values are additionally equipped with a total ordering.

We investigate the frontiers of decidability for Petri nets with various data, and formulate the WQO Dichotomy Conjecture: under a mild assumption, either a data domain exhibits a well quasi-order (in which case one can apply the general setting of well-structured transition systems to solve problems like coverability or boundedness), or essentially all the decision problems are undecidable for Petri nets over that data domain.

The work is partially supported by the Polish National Center of Science 2012/07/B/ST6/01497.

1 Introduction

We investigate the model of Petri nets with data, where tokens carry values from some data domain, and executability of transitions is conditioned by a relation between data values involved. One can consider unordered data, like in [26], i.e. an infinite data domain with the equality as the only relation; or ordered data, like in [24], i.e. an infinite densely totally ordered data domain. One can also consider a more general setting of Petri nets over an arbitrary fixed data domain ${\mathbb A}$. In Sect. 2 we provide such a general definition of Petri nets with atoms ${\mathbb A}$, parametric in a relational structure ${\mathbb A}$. For instance, unordered and ordered data are modeled by ${\mathbb A}= ({\mathbb N}, =)$ and ${\mathbb A}= ({\mathbb Q}, \le )$, respectively. We want to emphasize here that the idea seems not at all new, as similar net models have been proposed already in the early 80ies: high-level Petri nets [13] and colored Petri nets [19]. Since then, similar formalisms seem to have been rediscovered, for instance constraint multiset rewriting [5, 8, 9].

Equivalently, Petri nets with atoms are just reinterpretation of the classical definition of Petri nets with a relaxed notion of finiteness, namely orbit-finiteness, where one allows for orbit-finite sets of places and transitions instead of just finite ones; this is along the lines of [3, 4].

It is well known that the reachability problem is undecidable for Petri nets with ordered data, while the decidability status of this problem for unordered data is a intriguing open problem. In this note we do not embark on investigation of the reachability problem. Instead, we concentrate on the termination problem, the boundedness problem, the coverability problem, and alike, jointly called here standard problems. Again, it is well known that standard problems are decidable for Petri nets with ordered data [24] (and in consequence also for Petri nets with unordered data), as the model fits into the framework of well-structured transition systems of [11]. Most importantly, the structure of ordered data admits, in a certain technical sense explained in Sect. 5, a well quasi-order (wqo).

The decidability status of standard problems depends on the choice of atoms ${\mathbb A}$, and the purpose of this note is to investigate the decidability border. In order to make it possible to finitely present Petri nets and its configurations, and in particular to consider Petri nets as input to algorithms, we restrict to relational structures ${\mathbb A}$ that are homogeneous [25] and effective (the formal definitions are given in Sect. 4). On one side, in Sect. 5 we provide a simple but general decidability result that works under the sole additional assumption that ${\mathbb A}$ admits a wqo (which generalizes the decidability result for ordered data [24]). On the other side, in Sect. 3 we provide an example of an effective homogeneous structure ${\mathbb A}$ that makes all standard problems for Petri nets undecidable; further such examples are mentioned in Sect. 6. An observation that none of this examples admits a wqo naturally leads to the WQO Dichotomy Conjecture formulated in Sect. 6: for a homogeneous effective structure ${\mathbb A}$, either ${\mathbb A}$ admits a wqo (and then the standard problems are easily decidable), or all the standard problems are undecidable for Petri nets with atoms ${\mathbb A}$. It seems that either confirming or falsifying this conjecture would be very interesting: in the former case one can expect a deeper insight into the power of wqo-based methods, while in the latter case one would have to come up with a completely new approach to deciding properties of Petri nets with data.

In this note we do not use the recent approach to forward analysis of well-structured transition systems based on idea completion [10]. In [17] this approach have been recently applied to compute Karp-Miller trees for Petri nets with unordered data. The procedure does not generalize however to other structures ${\mathbb A}$ that admit a wqo, for instance to ordered data.

2 Petri Nets with Atoms

Atoms. A model of data Petri nets, to be defined below, is parametric in the underlying logical structure; the structure can be seen as data domain. Thus in the sequel we always assume a fixed a countable relational¹ structure ${\mathbb A}$, which we call atoms. Here are some example structures of atoms:

• Equality atoms: natural numbers with equality ${\mathbb A}= ({\mathbb N}, =)$; equally well any other countable infinite set could be used instead of natural numbers ${\mathbb N}$, as the only available relation is equality.

• Total order atoms: rational numbers with the natural order ${\mathbb A}= ({\mathbb Q}, \le )$; again, any other countable infinite dense total order without extremal elements could be used instead.

• Timed atoms: ${\mathbb A}= ({\mathbb Q}, \le , +1)$ extending total order atoms with the binary relation $x +1 = y$.

Note that every structure in the above list extends the preceding one by some additional relations. In the sequel we always assume that the vocabulary (signature) $\varSigma$ of ${\mathbb A}$ is finite and contains the equality $=$.

Petri Nets with Atoms. We define a model that extends classical place/transition Petri nets. A Petri net with atoms ${\mathbb A}$ consists of two disjoint finite sets of places P and of transitions T, the arcs $A \subseteq P{\times } T \cup T{\times } P$, and two labelings:

• arcs are labelled by pairwise disjoint finite nonempty sets of variables;

• transitions are labelled by first-order formulas over the vocabulary $\varSigma$ of ${\mathbb A}$, such that free variables of the formula labeling a transition t belong to the union of labels of the arcs incident to t.

Fig. 1.

A Petri net with equality atoms with places $P = \{p_1, p_2\}$ and transitions $T = \{t_1, t_2\}$. Different atoms are depicted through differently colored tokens.

Example 1

As an illustrating example, consider a Petri net with equality atoms with two places $p_1, p_2$ and two transitions $t_1, t_2$ depicted on Fig. 1. Transition $t_1$ outputs two tokens with arbitrary but distinct data values onto place $p_1$. Transition $t_2$ inputs two tokens with the same data value, say a, one from $p_1$ and one from $p_2$, and outputs three tokens: two tokens with arbitrary but equal data values, say b, one onto $p_1$ and the other onto $p_2$; and one token with a data value $c \ne a$ onto $p_2$. Note that transition $t_2$ does not specify whether $b = a$, or $b = c$, or $b \ne a, c$, and therefore all three options are allowed. Variables $y_1, y_2$ can be considered as input variables of $t_2$, while variables $z_1, z_2, z_3$ can be considered as output ones; analogously, $t_1$ has no input variables, and two output ones $x_1, x_2$.

From syntactic point of view, the net in Fig. 1 can be considered to be over any atoms ${\mathbb A}$, as we always assume equality relation to be available in ${\mathbb A}$.

The formal semantics of Petri nets with atoms is given by translation to multiset rewriting. Given a set X, finite or infinite, a finite multiset over X is a finite (possible empty) partial function from X to positive integers. In the sequel let $\mathcal{M}(X)$ stand for the set of all finite multisets over X. A multiset rewriting system $(\mathcal{P}, \mathcal{T})$ consists of a set $\mathcal{P}$, and a set of rewriting rules:

$$ \mathcal{T}\quad \subseteq \quad \mathcal{M}(\mathcal{P}) \times \mathcal{M}(\mathcal{P}). $$

Configurations $C \in \mathcal{M}(\mathcal{P})$ are finite multisets over $\mathcal{P}$, and the step relation $\longrightarrow$ between configurations is defined as follows: for every $(I, O) \in \mathcal{T}$ and every $M \in \mathcal{M}(\mathcal{P})$, there is the step ($+$ stands for multiset union)

$$ M + I \ \longrightarrow \ M + O. $$

For instance, a classical Petri net induces a multiset rewriting system where $\mathcal{P}$ is the set of places, and $\mathcal{T}$ is essentially the set of transitions, both $\mathcal{P}$ and $\mathcal{T}$ being finite. Configurations correspond to markings.

A Petri net with atoms ${\mathbb A}$ induces a multiset rewriting system $(\mathcal{P}, \mathcal{T})$, where $\mathcal{P}= P \times {\mathbb A}$ and is thus infinite. Configurations are finite multisets over $P\times {\mathbb A}$ (cf. a configuration depicted in Fig. 1). The rewriting rules $\mathcal{T}$ are defined as

$$ \mathcal{T}\quad = \quad \bigcup _{t\in T} \mathcal{T}_t, $$

where the relation $\mathcal{T}_t \subseteq \mathcal{M}(\mathcal{P}) \times \mathcal{M}(\mathcal{P})$ is defined as follows. Let $\phi$ denote the formula labeling the transition t, and let $X_i$, $X_o$ be the sets of input and output variables of t. Every valuation $v_i : X_i \rightarrow {\mathbb A}$ gives naturally raise to a multiset $M_{v_i}$ over $\mathcal{P}$, where $M_{v_i}(p, a)$ is the (positive) number of variables x labeling the arc (p, t) with $v_i(x) = a$. Likewise for valuations $v_o : X_o \rightarrow {\mathbb A}$. Then let

$$ \mathcal{T}_t = \left\{ \, (M_{v_i}, M_{v_o}) \, | \, v_i : X_i \rightarrow {\mathbb A}, \ v_o : X_o \rightarrow {\mathbb A}, \ v_i, v_o \vDash \phi \,\right\} . $$

Like $\mathcal{P}$, the set of rewriting rules $\mathcal{T}$ is infinite in general.

As usual, for a net N and its configuration C, a run of (N, C) is a maximal finite, or infinite sequence of step starting in C. A configuration of N is reachable from C if it appears in some run of (N, C).

Remark 1

Petri nets with equality atoms are equivalent to (even if defined differently than) unordered data Petri nets of [24]. An even different but equivalent definition, in the style of vector addition systems, have been used in [17]. Another equivalent model is $\nu$-PNs of [26] but without name creation: indeed, name creation considered in [26] is generation of a globally fresh atom, while in Petri nets with equality atoms it is only possible to generate a locally fresh one. Petri nets with total ordered atoms are equivalent to ordered data Petri nets of [24]. Finally, Petri nets with timed atoms subsume many timed extensions of Petri nets, including timed Petri nets [1] and timed-arc Petri nets [18].

Orbit-Finiteness. An atom automorphism is an automorphism of ${\mathbb A}$ with itself, that is a bijection ${\mathbb A}\rightarrow {\mathbb A}$ such that for every n-tuple $(a_1, \ldots , a_n)$ and every n-ary relation r in ${\mathbb A}$, $r(a_1, \ldots , a_n)$ holds if, and only if $r(f(a_1), \ldots , f(a_n))$ holds. For instance, in the case of equality atoms these are all bijections of ${\mathbb N}$, in the case of total order atoms these are all monotonic bijections of ${\mathbb Q}$, and in the case of timed atoms these are monotonic bijections of ${\mathbb Q}$ that preserve integer differences.

Fig. 2.

A pair of configurations related by $\preceq$, in the case of equality atoms. One witnessing automorphism maps black to blue, blue to brown, and preserves red; the other one maps black to red, red to blue, and blue to brown. (Color figure online)

We define an action of atom automorphisms on configurations: for a configuration C and an atom automorphism $\pi$, let $C\cdot \pi$ denote a configuration obtained from C by applying $\pi$ to every atom carried by every token in C. Using the action, we define a quasi-order (i.e., a reflexive and transitive relation) on configurations: $C \preceq C'$ if $C\cdot \pi \sqsubseteq C'$ for some atom automorphism $\pi$, where $\sqsubseteq$ stands for multiset inclusion (cf. Fig. 2). If $C \preceq C' \preceq C$ then $C\cdot \pi = C'$ for some atom automorphism $\pi$, in which case we call C and $C'$ equivalent. Note that the step relation is invariant under the equivalence: for equivalent C, $C'$, if $C \longrightarrow D$ then $C' \longrightarrow D'$ for some $D'$ equivalent to D. This is due to the fact the transitions are specified in the first-order logic which is clearly invariant under atom automorphisms.

A set of configurations $\mathcal C$ is orbit-finite if it is finite up to the equivalence. In other words, $\mathcal C$ is contained in a finite union of orbits, where an orbit of a configuration C is defined as $\left\{ \, C\cdot \pi \, | \, \pi \,\, \text {an atom automorphism}\,\right\}$. Similarly one can define orbits, and orbit-finiteness, for any other set on which an action of atom automorphisms is defined.

Remark 2

Our presentation is in the style of [14, 26], in order to keep it simple. Interestingly, an equivalent but more abstract definition can be provided, by following the approach of [3]. In this approach, a model of computation is reinterpreted with finiteness relaxed to orbit-finiteness. In case of Petri nets this boils down to allowing orbit-finite sets of places and transitions instead of finite ones only. Following the approach, one would consider the set $\mathcal{P}$ directly as places, and the set $\mathcal{T}$ as transitions of a net. For $\omega$-categorical structures ${\mathbb A}$, including all homogeneous relational structures [25], both $\mathcal{P}$ and $\mathcal{T}$ are orbit-finite sets.

Standard Decision Problems. We focus on classical decision problems, like the termination problem: does a given (N, C) admit only finite runs? The structure of atoms is considered as a parameter, and hence itself does not constitute part of input. Concerning representation of input, the net N is represented by finite sets P, T, A and appropriate labelings with variables and formulas. Representation of a configuration C will be discussed in Sect. 4. Another classical problem is the place non-emptiness problem (markability): given (N, C) and a place p of N, does (N, C) admit a run that puts at least one token on place p?

In order to define some other standard problems we need to take the action of atom automorphisms on configurations into account. For instance, a Petri net with atoms has typically infinitely many reachable configurations, and hence the classical boundedness question is not interesting. Thus we say that (N, C) is bounded if the set of reachable configurations is orbit-finite. This defines the appropriate variant of the boundedness problem. The coverability problem we define as follows: given N, C and $C'$, is there a configuration $C''$ of N reachable from C with $C' \preceq C''$? In the same vein one translates other decision problems to nets with atoms, for instance the evitability problem: given (N, C) and a finite set $\mathcal C$ of configurations of N, is there a run of (N, C) whose all configurations are in ${\uparrow }\mathcal{C} = \left\{ \, C' \, | \, \exists C\in \mathcal{C}. \ C\preceq C'\,\right\}$?

All the decision problems mentioned above we jointly call standard problems. These should be considered as examples rather that an exhaustive list – the results reported in the sequel keep holding for many other problems not mentioned above (we refrain however from an attempt of characterization of all such problems). An example of the problem for which the results do not hold is the place-boundedness problem, which is decidable for equality atoms (as shown in [17], using the forward analysis via computation of a Karp-Miller tree), but undecidable for total order atoms [24]. Also, we do not consider here the ‘hard’ decision problems, like reachability or liveness.

3 Undecidability

As already mentioned, decidability status of standard problems depends on the choice of data domain ${\mathbb A}$. Before stating a general decidability result for a wide class of structures ${\mathbb A}$ (cf. Sect. 5), in this section we exhibit an undecidable case – we sketch a proof of undecidability of the standard problems when tokens are allowed, roughly speaking, to carry pairs of equality atoms. Formally speaking, we consider Petri nets with atoms

$$ {\mathbb A}_2 \ = \ ({\mathbb N}^2, =_1, =_2, =_{12}), $$

where $=_1$, $=_2$, and $=_{12}$ are binary relations describing, respectively, equality on the first coordinate, equality on the second coordinate, and equality of the first coordinate of the first argument with the second coordinate of the second argument. We show that Petri nets with atoms ${\mathbb A}_2$ can faithfully simulate computations of Minsky counter machines.

In the sequel consider a fixed deterministic Minsky machine $\mathcal{M}$ with two counters $c_1, c_2$, and states Q. We will sketch a construction of a Petri net N over ${\mathbb A}_2$ that simulates the computation of $\mathcal{M}$ from the initial state with the initial counter values $c_1 = c_2 = 0$. The net will have the following transitions:

$$ T \ = \ \{z_1, z_2, d_1, d_2, i_1, i_2, i'_1, i'_2, t_1, t_2\} $$

and its places will include, except for a number of auxiliary ones, the following places:

$$ \{p_1, p_2, q, r\} \cup Q \ \subseteq \ P. $$

In particular, every state of $\mathcal{M}$ will have a corresponding place in N. The idea is to represent a value $c_j = n$ by storing $n+1$ tokens on place $p_j$, carrying atoms

$$\begin{aligned} (a_1, a_2), (a_2, a_3), \ldots , (a_{n}, a_{n+1}), (a_{n+1}, a_1), \end{aligned}$$

for some arbitrary but distinct $a_1, \ldots , a_{n+1} \in {\mathbb N}$. Intuitively, if atoms were considered as directed edges, a value n of a counter is represented by a directed cycle of length $n+1$. The initial configuration C of N encodes counter values $c_1 = c_2 = 0$, by placing on $p_1$ and $p_2$ an atom (a, a), for some arbitrary $a\in {\mathbb N}$, corresponding to a self-loop. In addition, C contains a token on the place corresponding to the initial state of $\mathcal{M}$.

Zero Test: A zero test on a counter $c_j$ is performed by a transition $z_j$ that inputs one token from $p_j$ (cf. Fig. 3). The transition detects a self-loop using the constraint $x =_{12} x$, where x is the input variable. The input token is output back onto place $p_j$ in order to preserve the representation of the counter value.

Fig. 3.

Transition $z_j$ simulating zero test of counter $c_j$. The equality $x = x'$ is a shorthand for $x =_1 x' \ \wedge \ x =_2 x'$. For simplicity, the places corresponding to control states of $\mathcal{M}$ are omitted.

Fig. 4.

Transition $z_j$ simulating decrement operation on counter $c_j$.

Decrement: The decrement operation on a counter $c_j$ is simulated, roughly speaking, by replacing two consecutive edges on a cycle by one edge; using the condition $y =_{12} x$ we can enforce that the edge y follows the edge x on the cycle. This is achieved by a transition $d_j$ (cf. Fig. 4) that inputs from $p_j$ two tokens carrying atoms $(a, a')$ and $(a', a'')$, for arbitrarily chosen pairwise different $a, a', a'' \in {\mathbb N}$, and outputs to $p_j$ one token carrying $(a, a'')$.

Increment: Slightly more complicated is the simulation of the increment operation on a counter, as it involves creating a fresh natural number that must be different from all currently used ones. In the first step of the simulation, the net executes a transition $i_j$ that inputs a token $(a, a')$ from $p_j$ and outputs, for an arbitrarily chosen $a'' \in {\mathbb N}$ different than a and $a'$, two tokens carrying $(a, a'')$ and $(a'', a')$ onto an auxiliary place q. In addition, let the transition output a token carrying $(a'', a')$ onto place r. In the very last step of the simulation, two tokens will be moved from place q to $p_j$ by a transition $i'_j$, and a single token will be removed from r. The aim of the remaining steps is to check that $a''$ does not currently appear on place $p_j$. To this aim the net traverses the cycle stored on $p_j$, starting from the edge $(a'', a')$. The traversal is done by iterative execution of the transition $t_j$, depicted on Fig. 5, that uses the place r to store the current edge in the course of traversal. The condition $x =_{12} z$ ensures that the edge x, picked up from place $p_j$, follows the edge z on the cycle. The equalities $x = x' = z'$ enforce that the edge x is put both back to $q_j$, and also copied to r. Finally, the condition $x \ne _2 y_1$ checks that the edges x and $y_1$ have different endpoints.

Fig. 5.

Transition $t_j$ constituting the crucial part of simulation of increment operation on counter $c_j$.

Note that replacing $x \ne _2 y_1$ by $x =_2 y_1$ would allow to detect that $a''$ does appear on the cycle, which means that $a''$ has been chosen incorrectly in the first step of the simulation. Note also that replacing $x \ne _2 y_1$ by $y_1 =_{12} x$ allows to detect that the endpoint of x equals a, and thus the traversal can be finished. Finally, observe that the case when the incremented counter has value $c_j = 0$ needs a separate treatment.

We have thus sketched a construction of a net N and configuration C such that the place corresponding to the halting state of $\mathcal{M}$ is nonempty in some reachable configuration of (N, C) if, and only if the machine $\mathcal{M}$ halts. This entails undecidability of the place non-emptiness, coverability and evitability problems. Furthermore, (N, C) terminates if and only if the machine $\mathcal{M}$ halts. This entails undecidability of the termination and boundedness problems.

Proposition 1

The standard problems are undecidable for Petri nets with atoms ${\mathbb A}_2$.

A similar undecidability argument can be given for Petri nets with slightly simpler atoms ${\mathbb A}'_2 = ({\mathbb N}^2, =_1, =_2)$. In contrast to this, all the standard problems are decidable for Petri nets with atoms ${\mathbb A}_1 = ({\mathbb N}^2, =_1, =)$, which will become apparent shortly. Below we investigate in more detail the decidability border between those atoms that admit decidability of classical decision problems and those atoms that do not.

4 Effective Homogeneous Atoms

In this section and in the next one we are going to stay on the decidable side. In this section we prepare the ground: we define the class of structures ${\mathbb A}$ we are going to restrict to, namely effective homogeneous ones [25]. This restriction will guarantee, in particular, that configurations of a Petri net can be finitely presented and thus input by an algorithm. We will also provide an operation of wreath product that preserves effective homogeneity. In the next section we will state a general decidability result for Petri nets over effective homogeneous atoms ${\mathbb A}$, using the setting of well-structured transition systems [11].

For two relational $\varSigma$-structures $\mathcal{A}$ and $\mathcal{B}$ we say that $\mathcal{A}$ embeds in $\mathcal{B}$, written $\mathcal{A} \unlhd \mathcal{B}$, if $\mathcal{A}$ is isomorphic to an induced substructure of $\mathcal{B}$, i.e. to a structure obtained by restricting $\mathcal{B}$ to a subset of its domain. This is witnessed by an injective function² $h : \mathcal{A} \rightarrow \mathcal{B}$, which we call embedding. The class of finite structures that embed into ${\mathbb A}$ we denote by $\textsc {Age}({\mathbb A})$.

Homogeneous Structures. A $\varSigma$-structure ${\mathbb A}$ is homogeneous if every isomorphism between two finite induced substructures of ${\mathbb A}$ extends to an automorphism of ${\mathbb A}$. (Intuitively, the ‘position’ of a finite induced substructure inside ${\mathbb A}$ depends only on its isomorphism type.) For instance, equality atoms and total order atoms are homogeneous structures. In the latter case finite induced substructures are just finite total orders, and every isomorphism between any two such total orders does extend to a monotonic bijection from ${\mathbb Q}$ to ${\mathbb Q}$. Timed atoms are not homogeneous: no isomorphism between two induced 2-element substructures $\{-1, 3\}$ and $\{0.5, 2.5\}$ extends to an automorphism of timed atoms, as the distances between $-1$ and 3, and between 0.5 and 2.5, are different integers.

There is a one-to-one correspondence between infinite countable homogeneous structures, and classes of finite structures over the same vocabulary that are closed under isomorphisms and induced substructures, and satisfy the amalgamation property³ (such classes of structures are called Fraïssé classes). In one direction, the class $\textsc {Age}({\mathbb A})$, for a homogeneous $\varSigma$-structure ${\mathbb A}$, is a Fraïssé class. In the other direction, a Fraïssé class of finite $\varSigma$-structures induces a unique up to isomorphism homogeneous $\varSigma$-structure via the construction of Fraïssé limit [12]. In particular, $({\mathbb N}, =)$ is the Fraïssé limit of finite pure sets (structures with $=$ as the only relation) and $({\mathbb Q}, \le )$ is the Fraïssé limit of finite total orders.

Many other natural classes of structures have the amalgamation property: finite graphs, finite directed graphs, finite partial orders, finite equivalence relations, finite tournaments, etc. Each of these classes induces, as the Fraïssé limit, a homogeneous relational structure. For instance finite graphs induce the universal graph (called also random graph) [12], which is the infinite countable graph that results with probability 1, if every pair of vertices is related by an edge with probability p, irrespectively of the choice of the probability as long as $0< p < 1$. Therefore, every finite graph G embeds into the universal graph, and if G embeds into another finite graph H then every embedding of G into the universal graph extends to an embedding of H. Along the same lines, finite partial orders induce the universal partial order, finite tournaments induce the universal tournament, etc. The Fraïssé limit of the finite equivalence relations is $({\mathbb D}, R, =)$, where ${\mathbb D}$ is a countably-infinite set and R is an infinite-index equivalence relation over ${\mathbb D}$ s.t. each one of the infinitely-many equivalence classes is itself an infinite subset of ${\mathbb D}$. This structure is isomorphic to $({\mathbb N}^2, =_1, =)$ and can be used to model data with nested equality, where one can check whether two elements belong to the same equivalence class and, if so, whether they are actually equal. Examples of homogeneous structures abound, see for instance [25].

From this point on we assume atoms to be a $\varSigma$-structure ${\mathbb A}$ satisfying the following two conditions:

• (A1) ${\mathbb A}$ is a homogeneous countable infinite relational structure.

• (A2) the following age problem for ${\mathbb A}$ is decidable: given a finite $\varSigma$-structure $\mathcal{A}$, decide whether $\mathcal{A} \unlhd {\mathbb A}$.

Such structures ${\mathbb A}$ we call effective homogeneous. All the structures ${\mathbb A}$ mentioned so far, except for timed atoms, are effective homogeneous.

Among various good properties, homogeneous structures admit quantifier elimination: every first-order formula is equivalent to (i.e., defines the same set as) a quantifier-free one. Therefore, from now on we may assume wlog. that formulas labeling transitions are quantifier-free.

Wreath Product. Given two relational structures ${\mathbb A}= (A, R_1, \dots , R_m)$ and ${\mathbb B}= (B, S_1, \dots , S_n)$, their wreath product is the relational structure ${\mathbb A} \otimes {\mathbb B}= (A \times B, R'_1, \dots , R'_m,$ $S'_1, \dots , S'_n)$, where

• $((a_1, b_1), \dots , (a_k, b_k)) \in R'_i$ if $(a_1, \dots , a_k) \in R_i$, and

• $((a_1, b_1), \dots , (a_k, b_k)) \in S'_j$ if $a_1 = \cdots = a_k$ and $(b_1, \dots , b_k) \in S_j$.

Intuitively, ${\mathbb A} \otimes {\mathbb B}$ is obtained by replacing each element in ${\mathbb A}$ with a disjoint copy of ${\mathbb B}$. For instance, $({\mathbb N}, =) \otimes ({\mathbb N}, =)$ is exactly ${\mathbb A}_1 = ({\mathbb N}^2, =_1, =)$. More generally, one can model data with k-nested equality: take ${\mathbb B}_1 = ({\mathbb N}, =)$ and, for each $k \ge 1$, let ${\mathbb B}_{k+1} = {\mathbb B}_1 \otimes {\mathbb B}_k$. Up to isomorphism, ${\mathbb B}_k$ is the structure $({\mathbb D}, R_1, \dots , R_k)$ with k nested equivalence relations $R_1, \ldots , R_k$ over an infinite set ${\mathbb D}$, where $R_1$ has infinitely many infinite equivalence classes, $R_{i+1}$ refines every equivalence class of $R_i$ into infinitely many classes, for $i = 1, \ldots , k-1$; and the finest relation $R_k$ is the equality.

The wreath product preserves effective homogeneity: first, if ${\mathbb A}$ and ${\mathbb B}$ are homogeneous then the same holds for ${\mathbb A} \otimes {\mathbb B}$, and second, the age problem for ${\mathbb A} \otimes {\mathbb B}$ reduces to the same problem for ${\mathbb A}$ and ${\mathbb B}$ [7]. As an example, the wreath product $({\mathbb Q}, \le ) \otimes ({\mathbb N}, =)$ is, up to isomorphism, the universal total quasi-order, i.e. the Fraïssé limit of all finite total quasi-orders.

5 Well-Structured Petri Nets

Fix an effective homogeneous $\varSigma$-structure ${\mathbb A}$. For a set X, let $\textsc {Age}({\mathbb A}, X)$ denote the set of all functions $\mathcal{A} \rightarrow X$, where $\mathcal{A} \in \textsc {Age}({\mathbb A})$. In other words, $\textsc {Age}({\mathbb A}, X)$ contains finite induced substructures of ${\mathbb A}$ labeled by elements of X.

Finite Representations. Recall that a configuration is a finite partial function from ${\mathbb A}\times P$ to positive integers, which can be reformatted into a total function $\mathcal{A} \rightarrow \mathcal{M}(P)$ from a finite (possibly empty) induced substructure $\mathcal{A}$ of ${\mathbb A}$ to finite multisets⁴ over P. Thus from now on we consider configurations as elements of

$$ \text {conf}({\mathbb A}, P) \quad = \quad \textsc {Age}({\mathbb A}, \mathcal{M}(P)). $$

By homogeneity of atoms, two configurations $C : \mathcal{A} \rightarrow \mathcal{M}(P)$ and $D : \mathcal{B} \rightarrow \mathcal{M}(P)$ are equivalent if, and only if the two domain structures $\mathcal{A}$, $\mathcal{B}$ are related by an isomorphism $h : \mathcal{A} \rightarrow \mathcal{B}$ that preserves labels: $C(a) = D(h(a))$ for every $a\in \mathcal{A}$. Similarly, $C\preceq C'$ if, and only if there is an embedding $h : \mathcal{A} \rightarrow \mathcal{B}$ that increases labels: $C(a) \sqsubseteq D(h(a))$ for every $a\in \mathcal{A}$ (recall that $\sqsubseteq$ stands for multiset inclusion).

Recall that the step relation is invariant under equivalence: equivalent configurations have equivalent successor configurations. Thus to represent a configuration it is enough to know the equivalence class of a configuration; furthermore, by homogeneity it is enough to know the isomorphism type of the domain structure $\mathcal{A}$. Therefore configurations of a Petri net with homogeneous atoms can be finitely represented (up to isomorphism of the domain structure), which makes the model amenable to algorithmic analysis.

Well Quasi-orders. By skeleton of a quasi-order $(X, \le )$ we mean the partial order obtained as the quotient of X by the equivalence relation that relates every two elements $x, y\in X$ satisfying $x \le y \le x$. We call two quasi-orders $(X, \le )$ and $(X', \le ')$ skeleton-isomorphic, and write $(X, \le ) \cong (X', \le ')$, if their skeletons are isomorphic.

A quasi-order $(X, \le )$ lifts naturally to $\textsc {Age}({\mathbb A}, X)$: for $f: \mathcal{A}\rightarrow X$ and $g:\mathcal{B}\rightarrow X$, let $f\unlhd _{(X, \le )} g$ if there is an embedding $h: \mathcal{A}\rightarrow \mathcal{B}$ such that $f(a) \le g(h(a))$ for every $a\in \mathcal{A}$. For instance, for equality atoms we obtain the natural lifting of $(X, \le )$ to finite multisets over X, and for total order atoms we obtain Higman ordering of finite sequences $X^*$ over X with respect to the base order $(X, \le )$ (see e.g. [10] for formal definitions). When $(X, \le ) = (\mathcal{M}(P), \sqsubseteq )$, one obtains the quasi-order of configurations:

$$ (\textsc {Age}({\mathbb A}, \mathcal{M}(P)), \unlhd _{(\mathcal{M}(P), \sqsubseteq )}) \quad \cong \quad (\text {conf}({\mathbb A}, P), \preceq ). $$

A well quasi-order (WQO) is a quasi-order $(X, \le )$ such that for every infinite sequence $x_1, x_2, \ldots$ of elements of X, there are positions $i<j$ with $x_i \le x_j$. Equivalently, a wqo is a well founded quasi-order without infinite antichains. For two skeleton-isomorphic quasi-orders, if one is a wqo than the other is a wqo too. For the rest of this section assume that

• (A3) for every wqo $(X, \le )$, the lifted quasi-order $(\textsc {Age}({\mathbb A}, X), \unlhd _{(X, \le )})$ is a wqo (we say in this case that ${\mathbb A}$ preserves WQO).

For example, both equality atoms and total order atoms preserve wqo. Indeed, if $(X, \le )$ is a wqo then $(\textsc {Age}(({\mathbb N}, =), X), \unlhd _{(X, \le )})$ is a wqo, which is a generalization of Dickson’s Lemma; and $(\textsc {Age}(({\mathbb Q}, \le ), X), \unlhd _{(X, \le )})$ is a wqo as well, which is exactly Higman’s Lemma [16]. Interestingly, for a suitably defined structure of atoms (a forest order, see [2] for details) one can also provide a similar model-theoretic reformulation of Kruskal’s lemma [22].

When ${\mathbb A}$ preserves wqo then $(\textsc {Age}({\mathbb A}), \unlhd )$ is necessarily a wqo. We do not know whether the converse holds, and thus the following question is open:

Question 1

For every homogeneous ${\mathbb A}$ such that $(\textsc {Age}({\mathbb A}), \unlhd )$ is a wqo, and for every wqo $(X, \le )$, is the lifted quasi-order $(\textsc {Age}({\mathbb A}, X), \unlhd _{(X, \le )})$ a wqo?

Let’s concentrate on an important special case, when $(X, \le ) = (\textsc {Age}({\mathbb B}), \unlhd )$ for some homogeneous structure ${\mathbb B}$. We observe that $\textsc {Age}({\mathbb A}, \textsc {Age}({\mathbb B}))$, containing induced substructures of ${\mathbb A}$ labeled by induced substructures of ${\mathbb B}$, is essentially the same set as $\textsc {Age}({\mathbb A} \otimes {\mathbb B})$, containing induced substructures of the wreath product. Furthermore, the lifted quasi-order coincides with the embedding quasi-order on $\textsc {Age}({\mathbb A} \otimes {\mathbb B})$. Formally, the following two quasi-orders are isomorphic:

$$\begin{aligned} (\textsc {Age}({\mathbb A}, \textsc {Age}(B)), \unlhd _{\unlhd }) \quad \cong \quad (\textsc {Age}({\mathbb A} \otimes {\mathbb B}), \unlhd ). \end{aligned}$$

(1)

This leads to a ‘weaker’ version of Question 1 (in the sense that the positive answer to Question 1 implies the same answer to the following one):

Question 2

For every homogeneous structures ${\mathbb A}$, ${\mathbb B}$ such that both $(\textsc {Age}({\mathbb A}), \unlhd )$ and $(\textsc {Age}({\mathbb B}), \unlhd )$ are wqos, is $({\mathbb A} \otimes {\mathbb B}, \unlhd )$ a wqo?

Note that the answer to Question 2 is positive in the special case when ${\mathbb A}$ preserves wqo.

We stress upon importance of the homogeneity assumption, as one can easily come up with a non-homogeneous counterexample to both questions, for instance taking ${\mathbb A}= ({\mathbb N}, +1)$.

Well-Structured Petri Nets with Atoms. We are now going to use the setting of well-structured transition systems of [11] to derive a general decidability result. Consider in the sequel a fixed effective homogeneous $\varSigma$-structure ${\mathbb A}$ that preserves wqo, and a fixed Petri net with atoms ${\mathbb A}$. We need to check a number of assumptions required for the decidability results of [11].

By decidability of the embedding problem one easily deduces that the step relation is computable. Indeed, a satisfying valuation of variables of a formula corresponds to an embedding of finite structure $\mathcal{A}$ in ${\mathbb A}$, and thus one can compute all (up to isomorphism) valuations satisfying a quantifier-free formula that labels a transition, by enumerating all finite $\varSigma$-structures $\mathcal{A}$ of bounded size. In particular one can compute successors $\left\{ \, C' \, | \, C\longrightarrow C'\,\right\}$ of a given configuration C (note that the successor set is finite, up to isomorphism of the domain structure). The ordering $\preceq$ is also easily decidable.

Like for classical Petri nets, step relation of a Petri net with atoms ${\mathbb A}$ satisfies a compatibility condition with respect to $\preceq$: if $C \prec D$ and $C \longrightarrow C'$ then there exists a configuration $D'$ with $C' \prec D'$ and $D \longrightarrow D'$. This property, combined with the invariance of step relation under equivalence, implies strong strict compatibility of [11].

Let ${\uparrow }C = \left\{ \, C' \, | \, C\preceq C'\,\right\}$ denote the upward closure of C. By compatibility, the predecessor set $\text {pred}({\uparrow }C) = \left\{ \, C' \, | \, C'\longrightarrow C'' \in {\uparrow }C\,\right\}$ is upward closed. As ${\mathbb A}$ preserves wqo, $(\text {conf}({\mathbb A}, P), \preceq )$ is a wqo and hence the set $\text {pred}({\uparrow }C)$ has only finitely many minimal elements. Using decidability of the embedding problem one shows the property called effective pred bases in [11]: given a configuration C, the finite set $\min (\text {pred}({\uparrow }C))$ is computable.

We have thus completed the check-list: $(\text {conf}({\mathbb A}, P), \longrightarrow , \preceq )$ is a well-structured transition system that satisfies all assumptions of Theorems 3.6, 4.6, 4.8 and (if skeleton of $(\text {conf}({\mathbb A}, P), \preceq )$ is considered) Theorem 4.11 in [11]. Therefore we may state the following general decidability result:

Theorem 1

If ${\mathbb A}$ is an effective homogeneous structure that preserves wqo then the standard problems are decidable for Petri nets with atoms ${\mathbb A}$.

This generalizes the decidability result of [24], and applies to a range of different structures of atoms including, among the others, equality atoms, total order atoms, and all structures obtained from them by the wreath product. Indeed, using the following generalization of the isomorphism (1):

$$\begin{aligned} (\textsc {Age}({\mathbb A}, \textsc {Age}({\mathbb B}, X)), \unlhd _{\unlhd _{(X, \le )}}) \quad \cong \quad (\textsc {Age}({\mathbb A} \otimes {\mathbb B}, X), \unlhd _{(X, \le )}), \end{aligned}$$

one easily shows that wreath product, in addition to preservation of effective homogeneity, also preserves wqo-preservation: if homogeneous structures ${\mathbb A}$ and ${\mathbb B}$ preserve wqo then ${\mathbb A} \otimes {\mathbb B}$ also does. For instance, in the case of nested equality atoms ${\mathbb A}_1 = ({\mathbb N}, =) \otimes ({\mathbb N}, =)$, the lifted quasi-order is skeleton isomorphic to the natural ordering of $\mathcal{M}(\mathcal{M}(X))$ finite multisets over finite multisets over X; and when atoms is the wreath product $({\mathbb Q}, \le ) \otimes ({\mathbb N}, =)$ of total order atoms and equality atoms, the lifted quasi-order is skeleton-isomorphic to the Higman ordering of ${\mathcal{M}(X)}^*$ finite sequences of finite multisets over X.

The decision procedures solving the standard problems, as derived from [11], can be actually directly encoded in the one of recently developed programming languages designed for manipulating infinite definable structures: LOIS [21] or N$\lambda$ [20].

6 The WQO Dichotomy Conjecture

What is the crucial difference between atoms ${\mathbb A}_1 = ({\mathbb N}^{(2)}, =_1, =)$ and ${\mathbb A}'_2 = ({\mathbb N}^{(2)}, =_1, =_2)$ that makes Petri nets with the former atoms decidable, while Petri nets with the latter atoms undecidable? We claim that the crucial difference is that the quasi-order $(\text {conf}({\mathbb A}_1, P), \preceq )$ is a wqo, while the quasi-oder $(\text {conf}({\mathbb A}'_2, P), \preceq )$ is not. All quasi-orders considered by us are well founded (as P is finite), hence the difference lies in existence of an infinite antichain in $(\text {conf}({\mathbb A}'_2, P), \preceq )$.

The induced substructure of ${\mathbb A}$ with domain $A\subseteq {\mathbb A}$ we call below the substructure induced by A. For the encoding of counter values in the undecidability proof in Sect. 3 we have actually used an infinite antichain $\{\mathcal{A}_1, \mathcal{A}_2, \ldots \}$ in $(\textsc {Age}({\mathbb A}_2), \unlhd )$, namely one that contains, for every $n\ge 1$, the substructure $\mathcal{A}_n$ of ${\mathbb A}_2$ induced by:

$$\begin{aligned} A_n = \{(a_1, a_2), (a_2, a_3), \ldots , (a_{n-1}, a_{n}), (a_{n}, a_1)\}, \end{aligned}$$

for some arbitrary but pairwise different $a_1, \ldots , a_n \in {\mathbb N}$. Note that when one moves to ${\mathbb A}'_2$, the substructures $\mathcal{A}'_n$ induced by the same subsets $A_n$ do not form an antichain any more; indeed, for $n< m$, an arbitrary injection $A_n \rightarrow A_m$ is an embedding of $\mathcal{A}'_n$ into $\mathcal{A}'_m$. In order to adapt the undecidability proof to Petri nets with atoms ${\mathbb A}'_2$, we can use another infinite antichain, namely one that contains, for every $n\ge 1$, the substructure of ${\mathbb A}'_2$ induced by:

$$ A'_n = \{(a_1, b_1), (a_2, b_1), (a_2, b_2), (a_3, b_2), \ldots , (a_n, b_{n-1}), (a_n, b_n), (a_1, b_n)\}, $$

for some arbitrary but pairwise different $a_1, \ldots , a_n\in {\mathbb N}$, and arbitrary but pairwise different $b_1, \ldots , b_n \in {\mathbb N}$. We leave it as an exercise to check that this is an antichain in $(\textsc {Age}({\mathbb A}'_2), \unlhd )$, and to adapt the undecidability proof.

Interestingly, for all structures ${\mathbb A}$ not preserving wqo that have been mentioned so far, one easily comes up with an infinite antichain $\{\mathcal{A}_1, \mathcal{A}_2, \ldots \}$ admitting an undecidability argument similar to the one in Sect. 3. For instance, in the case of the random graph atoms, take as $\mathcal{A}_n$ a cycle of length n, and in the case of the directed random graph, take as $\mathcal{A}_n$ a directed cycle of length n.

Fig. 6.

A crone partial order $\mathcal{A}_5$.

For the universal partial order $({\mathbb D}, \le )$, take as $\mathcal{A}_n$, for $n\ge 1$, a crone partial order (cf. Fig. 6) consisting of 2n elements $a_1, \ldots , a_n, b_1, \ldots , b_n\in {\mathbb D}$ such that $a_i \le b_j$ if and only if $i = j$, or $i = j+1$, or $i = 1$ and $j = n$, and moreover $\{a_1, \ldots , a_n\}$ and $\{b_1, \ldots , b_n\}$ are pairwise incomparable w.r.t. $\le$. One readily verifies that this is an antichain. Essentially, the antichain provides an encoding of finite cycles into partial orders.

Fig. 7.

A tournament $\mathcal{A}_8$ [15, 23]. All missing edges are oriented from left to right.

For the universal tournament, take as $\mathcal{A}_n$, for $n \ge 7$, an n-element tournament obtained from an n-element total order $a_1< a_2< \ldots < a_n$ by reversing edges $(a_1, a_3)$, $(a_{n-2}, a_n)$, and all edges $(a_i, a_{i+1})$ (cf. Fig. 7). Again, this is essentially an encoding of finite cycles into tournaments. A formal proof that $\left\{ \, \mathcal{A}_n \, | \, n\ge 7\,\right\}$ is an antichain can be found in [15, 23]. We encourage the reader to try reusing some of the antichains listed above in the undecidability proof.

We do not know whether every homogeneous structure not preserving wqo admits a similar encoding of finite cycles. Formally, we do not know the answer to the following question:

Question 3

When ${\mathbb A}$ is an effective homogeneous structure not preserving wqo, are all the standard problems undecidable for Petri nets with atoms ${\mathbb A}$?

We conjecture positive answers to Questions 1–3. Put explicitly, we formulate the following:

Conjecture 1

(WQO Dichotomy). For every effective homogeneous infinite countable relational structure ${\mathbb A}$ over a finite vocabulary, exactly one of the two conditions hold:

• $(\textsc {Age}({\mathbb A}),\unlhd )$ is a wqo;

• the standard problems are undecidable for Petri nets with atoms ${\mathbb A}$.

Any answers to Questions 1–3 will be interesting. If the conjecture is proved, this would shed a new light on the decidability border, and on the power of wqo-based methods. On the other hand, in order to falsify the conjecture one has to come up with a completely new method for solving (some of) the standard problems for Petri nets with data.

The conjecture is easily confirmed for atoms ${\mathbb A}$ ranging over a restricted subclass of homogeneous graph, or homogeneous directed graphs, using the classification result by Cherlin [6].

Remark 3

An analogous conjecture can be stated for other models of computation. For instance, instead of the standard problems for Petri nets with atoms, one can consider the universality problem for nondeterministic finite automata with one register, or the emptiness problems for alternating automata with one register (cf. [2]).