Introduction

Language inclusion refers to the problem of deciding whether a first language is included in a second language, that is, whether every word of the first language is also a word in the second language. For this paper, we assume that a language is described by a sound unlabelled WF-net (a subclass of Petri nets), and that every word in the language corresponds to a successfully terminating trace in that WF-net. As a result, the problem can now be rephrased as deciding whether every successfully terminating trace of a first sound unlabelled WF-net is also a successfully terminating trace of a second sound unlabelled WF-net.

There already is a large body of work on equivalences and/or similarities between Petri nets, e.g., [1][2][3]. However, in some cases we do not need to decide on language equivalence as language inclusion is already sufficient to investigate relevant properties. For example, suppose we have a large repository of Petri nets that are all different. To reduce the number of Petri nets we need to maintain, we might want to remove any Petri net that has less behaviour than some other Petri net. This requires us to determine whether the language of a Petri net is included in the language of another Petri net.

Conformance checking is another interesting application area for language inclusion. In conformance checking, one seeks to validate an event log against a Petri net, i.e., does every trace in the event log correspond to a successfully terminating transition sequence of the Petri net [4]? If we can create a Petri net that precisely captures the traces from the event log, then this question corresponds to whether the language of this created Petri net is included in the language of the original, given, Petri net.

Another interesting application of language inclusion comes from the CoSeLoG project 1 . In this project, we are cooperating with municipalities of different sizes and with different characteristics. If, for instance, a first, small, municipality wants to cooperate with a second, large, municipality, then the second municipality might have more generic process models (that is, Petri nets) that also support the first municipality. Although, language equivalence is unlikely to hold, language inclusion might very well hold, which is already sufficient for a fruitful cooperation. Apart from comparing the Petri nets of these municipalities, we can also combine them into a more generic Petri net [5], and check whether a Petri net of a third municipality is already included in this generic Petri net. If so, then this third municipality can be supported by this generic Petri net as well, while it might not have been supported by the Petri net of the first or the second municipality only. In the context of [5], we already have standardised the Petri nets, i.e., same activities names, and same level of abstraction.

The main problem with Petri-net-based language inclusion is that it is defined on the state-space underlying the Petri net (encoded as a transition system) and is PSPACE-complete. Due to the state-space explosion problem, such a transition system may be extremely large. Therefore, in general, it is computationally expensive to decide on language inclusion using the underlying transition systems.

We present a framework for deciding whether and how Petri-net-based language inclusion can be decided in a more efficient way for sound unlabelled WF-nets. The framework is based on the general pattern: If a sound unlabelled WF-net adheres only to some characteristics (e.g., is acyclic), then we can map this net to an alternative representation using a mapping function λ. Using a comparator ≤ λ , we may then efficiently decide whether language inclusion holds or not. As an example, Fig. 1 depicts a mapping function that maps every net to its set of transitions. Using the subset operator as comparator, we can already conclude that language inclusion does not hold, i.e., that the transition set of the first net is not a subset of the transition set of the second net.

For the case, sound unlabelled WF-nets that are free-choice and contain no loops, we prove that our approach is complete. If the net is not free-choice or contains loops, we present mapping functions and corresponding comparators that can signal that language inclusion does not hold. (⊆)

Fig. 1: General pattern of the framework: First, we map every net to an alternative representation (like its set of transitions); second, by efficiently comparing these alternative representations (like the standard subset comparator on the sets of transitions), language inclusion may be decided.

The structure of the paper is as follows. In Sect. 2, we present the approaches from literature and present the mappings found in literature. Preliminaries are provided in Sect. 3. Section 4 presents the general framework for our approach, which includes different mapping functions and comparators to tackle the language inclusion problem at hand. Finally, the conclusions and directions for future work are elaborated on in Sect. 5.

Related Work

There are solutions for checking whether the language of a first Petri net is included in the language of a second Petri net, see [6][7][8]. However, these solutions use the transition systems underlying both Petri nets. Unfortunately, these transition systems may become very large in the presence of parallelism. Therefore, as mentioned, we are designing a framework for deciding whether and how Petri-net-based language inclusion can be decided in a more efficient way. An important element of this framework is mapping a net to an alternative representation. In the remainder of this section, we present different candidates for such mappings as found in the literature. Note that this list is not exhaustive, but that our framework can easily incorporate other, new, mappings.

The first mapping we consider is based on the α-relation [9]. The α-relation denotes direct succession between activities and was originally designed for process discovery. In [10], a characterisation is given for the nets discoverable by the α-relation. Extensions have been made to the α-relation in [11] to be able to discover a larger set of nets.

The α-relation denotes direct succession, the relation used in behavioural profiles [3,12,13] denotes the eventual succession. Based on the behavioural profiles, work has been done for language equivalence, but language inclusion has not been addressed. A more generic approach based on behavioural profiles is presented in [1], where eventual succession is still considered, but the distance between occurrences of transition is bounded. Using behavioural profiles, [14] considers an abstraction, but this abstraction is not language-equivalence preserving, i.e., the language of the abstraction is different from the language of the original net.

An approach similar to behavioural profiles is the approach using causal footprints [15]. Causal footprints denote causality between activities. In [15], causal footprints are used to deduce structural properties of sound WF-nets. Using causal footprints, [16] denotes the similarity between nets. This similarity can be used to deduce language equivalence (similarity of 1), but this approach is not tailored towards language inclusion.

Causal nets [4] allow us to model processes in such a way that causality between activities is made explicit. Language inclusion of causal nets has been defined in [17]. Furthermore, [4] presents an operational algorithm to transform a net to a causal net by transforming place and transition into activities.

Process nets [18] allow us to encode causal runs. Such a causal run is expressed as a marked graph. The approach was originally designed for the validation of nets. Therefore, no language equivalence or language inclusion is defined on process nets.

The last mapping we mention is the mapping from a net to its basis of semipositive transition invariants [19]. The intuitive notion of such an invariant is that if we start at a given marking, and execute all the transitions from the invariant as many times as the invariant indicates, we return to the marking we started with. As such, every behavioural cycle in the Petri net is covered by such an invariant, but this not work the other way around: It may be possible that an invariant does not correspond to any behavioural cycle (due to the fact that we may not have sufficient tokens to execute exactly the transitions from the invariant).

In this paper, we consider the α-mapping, and the work that has been done on behavioural profiles, due to the fact they can be computed efficiently (in case of free-choice Petri nets [20]) on the structure of the net. The other abstractions can be used, but some do no always run in a time polynomial with respect to the size of the net. Causal footprints are closely related to behavioural profile. Therefore, using causal footprints yields similar results as using behavioural profiles. Hence, we do not use causal footprints. To use causal nets, we would need an approach to deal with the places introduced in the transformation as the same place might have different names in different process models. To use process nets, we would need an approach to deduce language inclusion between sets of sets of marked graphs. Furthermore, the number of process nets might be exponential in the number of choices, as there is no choice in a marked graph and every trace needs to be encoded in at least one marked graph. Finally, the main problem with semi-positive transition invariants is that the basis of invariant may be exponential in the size of the net.

Preliminaries

We use the following general notions: A denotes the set of actions, and N denotes the set of non-negative integers.

First, the notions of language, word of a language, and language inclusion are defined. A word is a sequence of actions from A, a language is a set of words, and a language is included in another language if and only if all the words of the first language are part of the second language.

Next, we introduce the notion of a transition system, and the language of a transition system. Definition 1 (Transition System). A Transition System T S = (S, →, α, ω) is a tuple where:

-S is the set of states, -→⊆ S × A × S is the set of transitions, α ∈ S is the initial state, ω ∈ S is the final state.

A word of a transition system is a sequence of transitions starting from the initial state and ending in the final state. The language of a transition system is the set of all words which can be produced by the transitions system. Now we introduce some general Petri net concepts.

Definition 2 ((Unlabelled) Petri net). A Petri net N = (P, T, F ) is a tuple where:

-P is a set of places, -T ⊆ A is a set of transitions, such that

P ∩ T = ∅, -F ⊆ (P × T ) ∪ (T × P ) is a flow relation.

The preset of a transition/place n, denoted by •n, is the set of places/transitions in i ∈ P ∪ T : (i, n) ∈ F . The postset of a transition/place n, denoted by n•, is the set of places/transitions in i ∈ P ∪ T : (n, i) ∈ F . A Petri net is free-choice if and only if for every two transitions, either the presets of every two transitions is disjoint, or they are the same. Definition 3 (Bag over Set). Let S be a set. A bag over S is a function from S to the natural numbers N such that only a finite number of elements from S is assigned a non-zero function value.

Note that a finite set is also a bag, namely the function assigning 1 to every element in the set and 0 otherwise.

The set of all bags over S is denoted B(S). For a bag b over S and s ∈ S, b(s) denotes the number of occurrences of s in b, often called the cardinality of s in b. We use brackets to explicitly enumerate a bag and superscripts to denote cardinalities. For example, [a 2 , b 3 , c] is the bag with two a's, three b's and one c; the bag [s 2 | P (s)], where P is a predicate on S, contains two elements s for every s such that P (s) holds. The sum of two bags b 1 and b

2 , denoted b 1 + b 2 , is defined as [s n | s ∈ S ∧ n = b 1 (s) + b 2 (s)]. The difference of two bags b 1 and b 2 , denoted b 1 − b 2 , is defined as [s n | s ∈ S ∧ n = (b 1 (s) − b 2 (s)) max 0]. Bag b 1 is a subbag of b 2 , denoted b 1 ≤ b 2 , if and only if ∀s ∈ S : b 1 (s) ≤ b 2 (s).

A marking of a Petri net is a bag over the set of places. A transition t is enabled in a marking M , denoted by M [t , if and only if the preset of t is a subbag of M . Firing an enabled transition t from a marking M resulting in another marking M is denoted by M [t M . Marking M is obtained by taking the difference between M and the preset of t and summing it with the postset of t, i.e. M = M − •t + t•.

Definition 4 (Transition System of a Petri net). Let N = (P, T, F ) be a Petri net, let M i be a marking of N , and let M o be a marking of N , then the transition system T S = T S(N, M i , M o ), belonging to N , is constructed as follows:

-α = M i , -ω = M o , -S is the smallest set X, such that: • α ∈ X, ω ∈ X, and • if s ∈ X ∧ s[t s for some t ∈ T and s ∈ B(P ), then s ∈ X. -→= {(s 1 , t, s 2 ) | s 1 , s 2 ∈ S ∧ t ∈ T ∧ s 1 [t s 2 }.

The language of a Petri net is the language of the transition system as constructed in Def. 4.

As mentioned, we limit ourselves to WF-nets [21]. A WF-net has a unique input and output place, i.e., the preset of the input place is empty and the postset of the output place is empty. Furthermore, every transition is on a path between the input place and the output place. With T S(N ), we denote the transition system belonging to the WF-net N with unique input place i and output place o (i.e., T S(N

) = T S(N, [i], [o])).

We require a WF-net to be sound [21].

Definition 5 (Soundness [21]). Let N = (P, T, F ) be a WF-net, let T S = (S, →, α, ω) be a transition system belonging to N , i.e., T S = T S(N ), then N is sound if and only if (note that α is [i] and ω is [o]):

-∀m ∈ S : (m, ω) ∈→ * , where → * is the transitive closure of →, -∀t ∈ T : ∃s, s ∈ S : (s, t, s ) ∈→.

In the remainder of this paper, N denotes the set of all sound unlabelled WF-nets. Note that whenever we say WF-net the unlabelled variant is intended unless stated differently.

As mentioned in the related work section, there exist approaches to compute language inclusion on the transition system. However, this computation does not need to be polynomial in the size of the Petri net. Therefore, we provide in Sect. 4 an approach to deduce language inclusion based on the structure of the Petri net.

Approach

In this section, we determine in which situations language inclusion can be efficiently computed on the transition system, and what can be done to avoid using the transition system in other situations. For the latter, we use our framework, i.e., when the net has certain characteristics, this net is mapped onto an alternative representation. Using a comparator, language inclusion can be decided, similar to the example given in the introduction.

Whether it is computationally efficient to use the transition system and, if not, which mapping can be used, depends heavily on the constructs used in the Petri nets, i.e., on the characteristics of both nets. For example, if both nets are sequential and acyclic, then language inclusion can be efficiently computed on the transition systems. If both nets are acyclic, then the eventually-follows relation between transitions may provide valuable information on language inclusion, where the eventually-follows relation between two transitions denote that the first can be followed by the second.

The remainder of this section is organised as follows: We first define an abstract mapping, then introduce characteristics, and finally define a comparator. Afterwards, we revisit the used (concrete) mappings from literature. Having the concrete mappings in place, the characteristics are defined, and a polynomialtime algorithm is provided to compute these characteristics on the free-choice WF-nets. Using the mappings and characteristics, we provide comparators and accompanying abstractions together, as they are tightly linked.

Abstract framework

In our abstract framework, an abstraction consists of three elements: (1) a mapping function, mapping a Petri net into an abstract representation, (2) a set of characteristics denoting when this abstraction can be applied, and (3) a comparator to compare the abstract representations (mapping to the booleans). The first and the last follow straightforward from the previous explanations, but the second requires some extra explanation and mainly on the can be applied part.

We say a Petri net adheres to certain characteristics if and only if these characteristics are valid for this Petri net. This allows abstractions to be used when characteristics are added, i.e., the addition of an characteristic does not invalidate the results presented in this paper.

Two different kinds of abstractions are considered: (1) a positive abstraction between N and N denoting that: If the comparator yields true, N is guaranteed to be language included in N , and (2) a negative abstraction between N and N denoting that: If the comparator yields false, N is guaranteed to be not language included in N . This allows our framework to be more flexible.

Mappings

Having the abstract framework with abstractions in place, we now present the specific mappings used (based on the reasoning in Sect. 2) in the remainder of A B Fig. 2: Two WF-nets with different languages but with the same mapping. this paper. Please note that we do not claim that these mappings are exhaustive: Other mappings may exist that allow for efficient positive and/or negative abstractions that are not covered by this paper. However, these mappings (and corresponding comparator) can be easily added to our framework.

The T -mapping provides us with the set of transitions from a WF-net, as explained in the introduction (we denote this set as λ T (N )).

The α-mapping denotes that two transitions can follow each other directly in a Petri net N , i.e., if (t 1 , t 2 ) is part of the mapping (denoted by λ α (N )), then there is a trace in which t 1 is directly followed by t 2 .

The ∞-mapping denotes that two transitions can follow each other eventually in a Petri net N , i.e., if (t 1 , t 2 ) is part of the mapping (denoted by λ ∞ (N )), then there is a trace in which t 1 is eventually followed by t 2 .

The presence of loops may be problematic for the ∞-mapping. For this reason, we also include the k-mapping (generalisation of the α-mapping), which denotes that there are at most k other activities between two transitions in a Petri net N . As such, this mapping (denoted by λ k (N )) corresponds to the eventually-follows-within-k-steps-relation between transitions. As a result, transitions that occur in a loop of length of at least k are not automatically related in both ways by this mapping, e.g., assume a and b are in a loop, then (a, b) in λ k (N ) but (b, a) does not need to be in λ k (N ) while (b, a) would have been included in λ ∞ (N ).

These latter three specific mappings are all based on relations between two transitions, which poses a possible problem if a net only contains traces that contain only a single transition. Clearly, for such a net these follows relations are all empty, which yields equivalent mappings for the nets in Fig. 2. For this reason, we add artificial start and end activities ( , ⊥) to any net. Note that this does not limit the expressivity of the process models.

Characteristics

Since our framework depends on the exact definition of the characteristics, this section defines the characteristics of sound WF-nets, and shows that we can compute these characteristics efficiently in case of free-choice nets.

The sequential characteristic denotes that from a state firing one transition, means the other transitions enabled in the state are no longer enabled. Definition 6 (Sequential Characteristic). Let N = (P, T, F ) ∈ N be a sound WF-net, let T S = (S, →, α, ω) be the transition system belonging to N , i.e., T S = T S(N ), then N is sequential if and only if:

∀t 1 , t 2 ∈ T, s ∈ S : ¬(•t 1 + •t 2 ≤ s)

The acyclic characteristic denotes that it is not possible to reach a previously visited state.

Definition 7 (Acyclic Characteristic). Let N = (P, T, F ) ∈ N be a sound WF-net, let T S = (S, →, α, ω) be the transition system belonging to N , i.e., T S = T S(N ), then N is acyclic if and only if: ∀n ∈ N, s 0 , . . . , s n ∈ S, t 1 , . . . , t n ∈ T :

n < 1 ∨ s 0 = s n ∨ ∃1 ≤ k ≤ n : (s k−1 , t k , s k ) ∈→.

In general, these characteristics are defined on the transition system, and may be inefficient to compute. However, for free-choice nets we can compute them in an efficient way, as the following theorems show.

A B C

Fig. 3: With the dashed place and arrows, we have a sequential construct, else not.

In [1](Def. 26), a polynomial time algorithm is presented to compute the minimal structural successor between places and transitions (MSS) for a free-choice net, i.e., the minimal set of transitions and places between the execution of two transitions. For some characteristics, we require that the considered transitions can follow each other directly, thus a MSS has a size of 1, i.e., only a single place is between the transitions. Consider Fig. 3, without the dashed parts, B and C are non-sequential. However, with the dashed parts, B and C are sequential. In the first case, the size of the MSS between A and C is 1, in the latter case the size of the MSS between A and C is 3.

Theorem 1. Let N = (P, T, F ) be a sound, free-choice WF-net, then N is sequential if and only if:

∀u 1 , u 2 , u 3 ∈ T : u 1 • ∩ • u 2 = ∅ ∨ u 1 • ∩ • u 3 = ∅ ∨ •u 2 ∩ •u 3 = ∅ ∨ |MSS(u 1 , u 2 )| = 1 ∨ |MSS(u 1 , u 3 )| = 1.

Proof. We need to prove:

(∀t 1 , t 2 ∈ T, s ∈ S : ¬(•t 1 + •t 2 ≤ s)) ⇔ (∀u 1 , u 2 , u 3 ∈ T : u 1 • ∩ • u 2 = ∅ ∨ u 1 • ∩ • u 3 = ∅ ∨ •u 2 ∩ •u 3 = ∅ ∨ |MSS(u 1 , u 2 )| = 1 ∨ |MSS(u 1 , u 3 )| = 1).

⇒ We prove this by contradiction, assume the left-hand side is true, but the right-hand side is false, thus ∃u 1 , u 2 , u 3 ∈ T :

u 1 • ∩ • u 2 = ∅ ∧ u 1 • ∩ • u 3 = ∅ ∧ •u 2 ∩ •u 3 = ∅ ∧ |MSS(u 1 , u 2 )| = 1 ∧ |MSS(u 1 , u 3 )| = 1.

From the righthand side it follows that u 2 and u 3 are both enabled after executing u 1 (by soundness, we know u 1 can fire). Furthermore, u 2 and u 3 can fire directly after u 1 by the M SS, and because their presets are disjoint there is no ordering between u 2 and u 3 . Hence, there is a state s such that •u 2 +•u 3 ≤ s. ⇐ Again we prove this by contradiction, assume the right-hand side is true, but the left-hand side is false, thus ∃t 1 , t

u 1 • ∩ • u 2 = ∅ and u 1 • ∩ • u 3 = ∅ and •u 2 ∩ •u 3 = ∅. • Assume t • ∩ • t 1 = ∅,: •t 1 ∩ t n • = ∅ ∨ (∃1 ≤ k < n : t k • ∩ • t k+1 = ∅).

Proof. We need to prove: (∀n ∈ N, s 0 , . . . , s n ∈ S, t 1 , . . . , t n ∈ T :

n < 1 ∨ s 0 = s n ∨ ∃1 ≤ k ≤ n : (s k−1 , t k , s k ) ∈→) ⇔ (∀t 1 , . . . t n ∈ T : •t 1 ∩ t n • = ∅ ∨ (∃1 ≤ k < n : t k • ∩ • t k+1 = ∅)).

⇒ This follows from the free-choice property, i.e., as soon as we can mark a place in the preset of a transition, then this token can only be removed after this transition has been enabled. As a result, if we mark a place in the preset of a previously enabled transition, then we can do this an infinite amount of times as this transition has to be able to fire. Since the state-space is finite (bounded net due to soundness) this means we have a path to a previously visited state.

⇐ When we do not have a sequence of transition to mark a place again, this means as soon as this place has been marked it will never be marked again. Hence, we cannot revisit a state.

From Thm. 1 and Thm. 2, we can conclude that, for free-choice WF-nets the characteristics can be efficiently computed, i.e., in polynomial time. As a result, we can use these characteristics in our framework.

Abstractions

This section builds on the previous sections by presenting concrete instantiations of the framework, consisting of selected abstractions, that can be used to efficiently decide language inclusion for nets with certain characteristics. Therefore, in the remainder, we display different approaches, each tailored towards nets with certain characteristics. We start with the approach which does not require an abstraction of the Petri net.

No abstraction needed In case the Petri net is sequential and free-choice, the transition systems will not suffer from the state-space-explosion problem. For this reason, we do not need an abstraction, as we can efficiently decide the language inclusion problem on the transition systems.

Negative abstraction using T -mapping

The following negative abstraction is valid for all sound WF-nets.

Definition 8 (T -Comparator).

Let N = (P, T, F ) and N = (P , T , F ) be sound WF-nets, let λ T be the T -mapping, then λ T (N )

≤ T λ T (N ) if and only if: λ T (N ) ⊆ λ T (N ) Theorem 3. (λ T , ≤ T , ∅) is a negative abstraction.

Proof. As both nets are sound WF-nets, all transitions of N are included in L(N ). That is, for every t ∈ T there exists a trace σ ∈ L(N ) such that t ∈ σ. Clearly, if there exists a transition t ∈ T such that t ∈ T , then the traces in N that contain t are not traces of N . Hence, language inclusion cannot hold.

Negative abstraction using α-mapping

The following negative abstraction is also valid for all sound WF-nets. However, to our knowledge, only for freechoice WF-nets there is a polynomial-time algorithm to compute the α-mapping. Hence we can use the negative abstraction to efficiently decide language inclusion either if we have a free-choice net or if the required α-mappings are given. Definition 9 (α-Comparator). Let N = (P, T, F ), N = (P , T , F ), be sound WF-nets, let λ α be the α-mapping, then λ α (N ) ≤ α λ α (N ) if and only if:

λ α (N ) ⊆ λ α (N ) Theorem 4. (λ α , ≤ α , ∅) is a negative abstraction. Proof. We need to prove that ¬(λ α (N ) ≤ α λ α (N )) ⇒ ¬(L(N ) ⊆ L(N )) which can be rewritten to L(N ) ⊆ L(N ) ⇒ λ α (N ) ≤ α λ α (N ) which follows straight- forward from the definition of λ α .

Theorem 4 yields the following result: Given two sound WF-nets and their corresponding α-mappings, Def. 9 can be computed in polynomial time. Hence, Thm. 4 yields in polynomial time whether the language is not included, i.e., if

A B A B C D D

Fig. 4: Two process models where we have a false positive w.r.t. language inclusion if we simply use inclusion of the α-relation.

λ α (N ) ⊆ λ α (N ) yields false then the inclusion does not hold. In case no αmapping is provided, we can, for free-choice WF-nets, compute the α-mapping efficiently and determine if language inclusion does not hold.

Using the α-mapping, we did not obtain a positive abstraction, as we cannot do an inclusion of the relations between the different process models. Consider the models in Fig. 4. Here, it is easy to see that the relations of the righthand model are a subset of left-hand model. That is, in the left model we have the relations λ α (N ) = {(A, B), (A, C), (B, C), (C, B), (B, D), (C, D)}, and in the right model we have the relations: λ α (N ) = {(A, B), (B, D)}. However, the word ABD is included in the right model, but not in the left model.

The problem is that we are omitting related activities, e.g., the A is followed, in Fig. 4, by a C, while with omitting relations, we also omit these dependencies.

Consider Fig. 5, at the bottom, for both models, we have transformed the parallel execution into a sequential execution such that λ α (right model) ⊆ λ α (left model). In the top two models, we have done the same, but this yields a model allowing words not possible in the other model. So, we need to find an inclusion operator, which can either differentiate between both models or considers both models not to be included in the other. In the first case, we have false negatives (see bottom model), in the second case, we have false positive (see top model). The problem is: The α-mapping considers two activities exclusive if they cannot follow each other directly. Hence, we have to look at the transitivity of these relations.

Positive abstraction using ∞-mapping In case the WF-net is acyclic, we can use the ∞-mapping instead of the α-mapping. Using this mapping, we can compute the transitive closure of the α-relations to deduce the relations between all activities. However, similar to the α-mapping, a simple inclusion of the sets is not strong enough to deduce language inclusion. Therefore, we need an approach which takes into account the alternatives between different activities. Alternative activities are activities which do not occur together in a trace. So, if an activity does not occur in a word, then an alternative activity occurs in that word.

Theorem 5. Let N = (P, T, F ) be a sound acyclic free-choice net, then:

∀a ∈ T, σ ∈ L(N ) : a ∈ σ ⇒ ∃b ∈ T : b ∈ σ ∧ (a, b) ∈ λ ∞ (N ) ∧ (b, a) ∈ λ ∞ (N ).

Proof. Assume there is an a ∈ T and a ∈ σ (by soundness we know a can be executed). This means there is a choice to not execute a. Since we have freechoice nets, this means somewhere there are two transitions such that after t 1 a can still follow, but after executing t 2 a cannot follow. Due to the fact that the net is acyclic and free-choice, a cannot precede t 2 , i.e., if a can, via firing some transitions, mark the preset of t 2 then also the preset of t 1 is marked and hence a can execute again. Since a is not in σ, we have chosen t 2 , and thus t 2 ∈ σ. Also because a cannot follow t 2 , and t 2 cannot follow a, (a,

t 1 , t 2 (•t 1 = •t 2 ),t 2 ) ∈ λ ∞ (N ) ∧ (t 2 , a) ∈ λ ∞ (N ).

Now the comparator denotes that the activities have to be the same, the relations have to be a subset (similar to Def. 9), and there is always at least one alternative activity remaining. We have to require clause 3, as this allows us to only remove alternative activities. Consider Fig. 6, the lower model is language included in the right model, and this is valid since an alternative activity for B (namely C) follows A. However, the left model is not language included in the lower model, as there is no alternative activity for C following A. Without clause 3, the comparator would have denoted that the left model is included in the lower model.

(b) Thm. 5 yields that somewhere we have made a choice in σ prefix to not execute b in N , we call the activity after making this choice a. Since σ prefix can be followed by b in N , we obtain that (a, b) ∈ λ ∞ (N ), but also (a, b) ∈ λ ∞ (N ) (note that (b, a) λ ∞ (N ), since this violates the acyclic property). From clause 3, we obtain there has to be an activity c such that (a, c)

∈ λ ∞ (N ) ∨ (c, a) ∈ λ ∞ (N ) and (b, c) ∈ λ ∞ (N ) ∧ (c, b) ∈ λ ∞ (N ).

Finally, from Thm. 5, we obtain that there has to be an alternative activity for b in σ, which c also is. Now it remains to show that c is in σ prefix . By free-choiceness, we obtain that c has to be executed before t k . If c can be executed after t k , then dependent on the activities chosen before t k , c can either be executed or not, which violates the free-choice property. Since (c, t k ) ∈ λ ∞ (N ), it follows that c has to be in σ prefix , and thus no b can be between σ prefix and t k in N .

From this it follows that both models can execute t k directly after prefix σ prefix , and hence both models are able to perform σ (note that termination is taken care of by including ⊥ as unique end activity) and thus it follows that σ is also in L(N ). Thus by contradiction, we have shown that λ

∞ (N ) ≤ ∞ λ ∞ (N ) ⇒ L(N ) ⊆ L(N ).

In case T = T , we can decide language inclusion based on the ∞-mapping. However, in general it is the case that T = T . Therefore, we extend our approach to the case in which T ⊂ T . Note that we do not need to consider the case that T ⊂ T as language inclusion cannot hold.

In order to achieve T = T , we have the following reduction on N :

-Remove all transitions t ∈ (T \ T ) from N -Remove all places not connected to any transition If the reduced net is sound then we can use Def. 10 on the transformed net with T = T . It is easy to see that language inclusion is preserved as we only remove transitions not present in T , i.e., we do not reduce the language w.r.t. the overlap with T . If the resulting model is not sound, then a part of the language of N cannot be part of N .

Apart from showing the soundness of the abstraction using the ∞-mapping, we also want to show the completeness. This means that if the language of N is included in N , then our comparator always yields true. Theorem 7. (λ ∞ , ≤ ∞ , {Acyclic}) is complete, i.e., for two acyclic free-choice WF-nets N and N , we have λ

∞ (N ) ≤ ∞ λ ∞ (N ) ⇐ L(N ) ⊆ L(N ).

Proof. We prove this by contradiction. Assume L(N

) ⊆ L(N ), but λ ∞ (N ) ≤ ∞ λ ∞ (N ) does not yield true.

Then, at least one of the clauses has to be false. Clause 1 and 2 follow in a straightforward way. Assume clause 1 is false, then there is an activity x ∈ T which is not in T . Since T is sound, this means x occurs in at least one trace and this trace cannot occur in L(N ). Assume clause 2 is false, this means there is a relation between 2 activities x, y ∈ T such that (x, y) ∈ λ ∞ (N ), which is not in λ ∞ (N ). By definition, this means there is a word such that Assume clause 3 is not valid, this means that:

∃(a, b) ∈ λ ∞ (N ) : (∀c ∈ T : ¬((a, c) ∈ λ ∞ (N ) ∨ (c, a) ∈ λ ∞ (N )) ∨ (c, b) ∈ λ ∞ (N ) ∨ (b, c) ∈ λ ∞ (N )

) has to hold (negation of the clause 3). Recall that due to and ⊥, λ ∞ (N ) cannot be empty.

We choose an a and b, the universal quantifier denotes that either the activity c is exclusive to a, or can occur together with b in a trace. Thus, there is no alternative for b to occur together with a in the trace. If we chose b = c then we have that either b does not occur with a in a trace in N , or (b, b) ∈ λ ∞ (N ) which is not possible due to the acyclicness. Thus, in N a always occurs with b, while in N they are alternatives. Hence, language inclusion cannot hold.

We can conclude that Thm. 7 holds, and Def. 10 is complete.

No abstraction using the k-mapping In the most general case, when the characterisation does not pose any constraints, we have the same problems as mentioned earlier, e.g., that a simple inclusion does not work. Furthermore, we now have difficulties introduced by the combination of cycles and non-sequential activities, e.g., short loops in the α-mapping. Furthermore, the ∞-mapping has problems with cycles. For instance, see Fig. 7 where both models have the same ∞-mapping. However, the trace ACBDE is included in the right model, but not in the left model. Obviously, with equivalent ∞-mapping, we should have language equivalence, i.e., any comparator denotes that the sets are included in each other. Therefore, we consider the k-mapping. Again, using a naive approach, using the inclusion of relations does not work. Consider, for instance, the models in Fig. 8, where the relations in the right model are a subset of the relations in the left model. The problem with looking at k elements in advance is that this k is bounded by the shortest cycle. In other words, if k is larger than the shortest cycle then activities are considered in parallel when they are in sequence. Consider Fig. 9, from which it is clear that the right model is language-included in the left model. However, if we compute the relation between the activities, we need to have a relation between C and E (because present in right model, thus k ≥ 2), but also k < 2 because ...EGC... is a proper part of a trace due to the cycle, while this would yield that C and E are in parallel in the right model, and thus that the left model is language included in the right model.

The complete framework

In Table 1, the total framework is listed. Trans. Syst. denotes that language inclusion can be efficiently computed on the transitions system. T is the negative abstraction only considering transitions. The negative abstraction using the αmapping is listed under α. Finally, ∞ denotes the sound and complete positive abstraction using the ∞-mapping. Under characteristics: A denotes acyclic, and S denotes sequentiality. Pos/Neg denotes if it is a positive or negative approach, and complete denotes if the approach is complete.

Conclusion

We have presented a framework that supports the decision of language inclusion for sound unlabelled WF-nets in an efficient way. Apart from the framework, we have provided a number of mappings, characterisations, and comparators to be used in the framework. If there is sequentiality present in both WF-nets, the language inclusion problem can be computed in polynomial time in terms of the underlying transition systems. If one of the WF-nets is non-sequential, then our framework may still efficiently decide language inclusion using a number of abstractions. The first abstraction uses the sets of transitions: If the set of transitions of the first net is not a subset of the set of transitions of the second, then the language of the first net cannot be included in the language of the second net. The second abstraction uses the directly-follows relation (also called the α-relation) between transitions: If the α-relation of the first net is not a subset of the α-relation of the second net, then the language of the first net cannot be included in the language of the second net. The third abstraction uses the eventually follows relation (also called the ∞-relation) between transitions: If the ∞-relation of the first free-choice net is a subset of the ∞-relation of the second free-choice net, and if some additional structural requirements hold, then the language of the first net is included in the language of the second net. For free-choice acyclic nets this third abstraction is complete. In other words, language inclusion can only hold if the ∞-relation of the first net is a subset of the ∞-relation of the second net, and if the additional structural requirements hold.

In case of free-choice unlabelled WF-nets, all relations can be computed polynomial in the size of the WF-net. On these relations, we mainly perform containment between sets. In the third abstraction, we search for an alternative activity which, naively, entails trying every activity and adds a polynomial factor. Since each of the steps is polynomial in the size of the WF-net, we can conclude that our computations can be done polynomial in the size of the WF-net.

The framework cannot efficiently decide on language inclusion in all cases. Especially for nets that are (1) non-sequential, (2) are cyclic or are not freechoice, and (3) for which language inclusion is known to hold, our current set of abstractions will not be able to provide an answer in polynomial time. Due to the fact that the comparators of the first two abstraction will yield true and the preconditions of the third abstraction are not met. However, we do not claim that our framework is complete. Yet, our framework can be easily extended based on the general pattern provided with new abstractions that may provide efficient answers for cases uncovered by the current abstractions: Given an abstraction, a characterisation, and a comparator, a positive (like the third abstraction) or negative (like the first two abstractions) abstraction can be formulated.

In some cases, our abstractions can easily be applied to general Petri nets. However, there does not exist, to our knowledge, a polynomial time algorithm to compute the abstractions on general nets. One can argue that computing the abstractions means analysing the behaviour in part or in full.

In the future, we plan to extend our framework with abstractions that also can deal with labelled WF-nets and with nets that are cyclic, for example by considering abstractions based on block-structured nets. For block-structured nets (with a single entry and a single exit), the relations (like α and ∞) between transitions can often be derived efficiently from the block-structure.

Furthermore, we want to quantify the difference between two languages based on our framework, i.e., if language inclusion does not hold, what portion of the language in not included, and which part of the net is the main reason the language is not included. This can then be used as a quantification measure of inclusion between nets, and as a diagnostic result that can be used to align nets in such a way that language inclusion will hold.