We present a framework to efficiently check language inclusion between two sound unlabelled WF-nets. That is, to efficiently check whether every successfully terminating transition sequence of one sound unlabelled WF-net also is a successfully terminating transition sequence of a second sound unlabelled WF-net. Existing approaches for checking language inclusion are typically based on the underlying transition systems of both nets, and hence are subject to the well-known stateexplosion problem. As a result, these approaches cannot check language inclusion on sound unlabelled WF-nets in polynomial time. Our framework allows for efficient language inclusion checks even if parallelism is present, by comparing specific net abstractions that can be computed and compared in polynomial time. For sound unlabelled WF-nets that are free-choice and do not contain loops, we prove that our approach is complete.
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., [
Governments (CoSeLoG) project (http://www.win.tue.nl/coselog/). 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 [
Another interesting application of language inclusion comes from the CoSeLoG
project1. 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 [
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. 1 http://www.win.tue.nl/coselog/ {A, B, D, E, F, H, I}
{A, B, C, D, E, F, G, H, I } ≤λ (⊆)
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. 2
There are solutions for checking whether the language of a first Petri net is
included in the language of a second Petri net, see [
The first mapping we consider is based on the α-relation [
The α-relation denotes direct succession, the relation used in behavioural
profiles [
An approach similar to behavioural profiles is the approach using causal
footprints [
Causal nets [
Process nets [
The last mapping we mention is the mapping from a net to its basis of
semipositive transition invariants [
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 [
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.
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 Transition System T S = (S, →, α, ω)
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 S i ∈ P ∪ T : (i, n) ∈ F . The postset of a transition/place n, denoted by n•, is the set of places/transitions in S 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.
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, [a2, b3, c] is the bag with two a’s, three b’s and one c; the bag [s2 | 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 b1 and b2, denoted b1 + b2, is defined as [sn | s ∈ S ∧ n = b1(s) + b2(s)]. The difference of two bags b1 and b2, denoted b1 − b2, is defined as [sn | s ∈ S ∧ n = (b1(s) − b2(s)) max 0]. Bag b1 is a subbag of b2, denoted b1 ≤ b2, if and only if ∀s ∈ S : b1(s) ≤ b2(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 [ti, 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 0 is denoted by M [tiM 0. Marking M 0 is obtained by taking the difference between M and the preset of t and summing it with the postset of t, i.e. M 0 = M − •t + t•.
Definition 4 (Transition System of a Petri net). Let N = (P, T, F ) be a Petri net, let Mi be a marking of N , and let Mo be a marking of N , then the transition system T S = T S(N, Mi, Mo), belonging to N , is constructed as follows: – α = Mi, – ω = Mo, – S is the smallest set X, such that: • α ∈ X, ω ∈ X, and • if s ∈ X ∧ s[tis0 for some t ∈ T and s0 ∈ B(P ), then s0 ∈ X. – →= {(s1, t, s2) | s1, s2 ∈ S ∧ t ∈ T ∧ s1[tis2}.
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 [
We require a WF-net to be sound [
Definition 5 (Soundness [
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.
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. 4.1 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 0 denoting that: If the comparator yields true, N is guaranteed to be language included in N 0, and (2) a negative abstraction between N and N 0 denoting that: If the comparator yields false, N is guaranteed to be not language included in N 0. This allows our framework to be more flexible. 4.2
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 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 (t1, t2) is part of the mapping (denoted by λα(N )), then there is a trace in which t1 is directly followed by t2.
The ∞-mapping denotes that two transitions can follow each other eventually in a Petri net N , i.e., if (t1, t2) is part of the mapping (denoted by λ∞(N )), then there is a trace in which t1 is eventually followed by t2.
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. 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: ∀t1, t2 ∈ T, s ∈ S : ¬(•t1 + •t2 ≤ 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, s0, . . . , sn ∈ S, t1, . . . , tn ∈ T : n < 1 ∨ s0 6= sn ∨ ∃1 ≤ k ≤ n : (sk−1, tk, sk) 6∈→.
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
In [
Theorem 1. Let N = (P, T, F ) be a sound, free-choice WF-net, then N is sequential if and only if: ∀u1, u2, u3 ∈ T : u1 • ∩ • u2 = ∅ ∨ u1 • ∩ • u3 = ∅ ∨ •u2 ∩ •u3 6= ∅ ∨ |MSS(u1, u2)| 6= 1 ∨ |MSS(u1, u3)| 6= 1.
Proof. We need to prove: (∀t1, t2 ∈ T, s ∈ S : ¬(•t1 + •t2 ≤ s)) ⇔ (∀u1, u2, u3 ∈ T : u1 • ∩ • u2 = ∅ ∨ u1 • ∩ • u3 = ∅ ∨ •u2 ∩ •u3 6= ∅ ∨ |MSS(u1, u2)| 6= 1 ∨ |MSS(u1, u3)| 6= 1). ⇒ We prove this by contradiction, assume the left-hand side is true, but the right-hand side is false, thus ∃u1, u2, u3 ∈ T : u1 • ∩ • u2 6= ∅ ∧ u1 • ∩ • u3 6= ∅ ∧ •u2 ∩ •u3 = ∅ ∧ |MSS(u1, u2)| = 1 ∧ |MSS(u1, u3)| = 1. From the righthand side it follows that u2 and u3 are both enabled after executing u1 (by soundness, we know u1 can fire). Furthermore, u2 and u3 can fire directly after u1 by the M SS, and because their presets are disjoint there is no ordering between u2 and u3. Hence, there is a state s such that •u2 +•u3 ≤ s. ⇐ Again we prove this by contradiction, assume the right-hand side is true, but the left-hand side is false, thus ∃t1, t2 ∈ T, s ∈ S : •t1 + •t2 ≤ s. Since we have a sound WF-net, we start with a single token in the input place. This means there is a sequence of transitions to reach a state s where two transitions are enabled say t1 and t2, let s be the first state. Then there is a transition t to reach state s, let t fire from state s0, i.e., s0[tis. By the fact that t1 and t2 can fire directly from s, we know that |MSS(t, t1)| = 1 and |MSS(t, t2)| = 1. Now it remains to prove that the first 3 clauses are false, that is: u1 • ∩ • u2 6= ∅ and u1 • ∩ • u3 6= ∅ and •u2 ∩ •u3 = ∅.
• Assume t • ∩ • t1 = ∅, this means that s0[ti and s0[t1i. Then there are two options: •t + •t1 ≤ s0, this means s0 is an earlier state in which two ( t + •t1 ≤ transitions are enabled (not possible by assumption), and ¬ • s0). We now obtain by free-choiceness that •t = •t1. From the fact that t1 is still enabled after firing t, and the fact that t • ∩ • t1 = ∅, we obtain that •t + •t1 ≤ s0, this is not possible due to the free-choiceness and soundness as this allows t1 to fire twice, and hence (by free-choiceness) it is possible to mark the output place with two tokens. • The proof for t • ∩ • t2 goes analogous. • We only have the case where •t1 ∩ •t2 6= ∅, thus •t1 = •t2. Again by soundness and free-choiceness it follows that t1 can fire twice from state s, hence it is not sound. tu tu Theorem 2. Let N = (P, T, F ) be a sound, free-choice WF-net, then N is acyclic if and only if: ∀t1, . . . tn ∈ T : •t1 ∩ tn• = ∅ ∨ (∃1 ≤ k < n : tk • ∩ • tk+1 = ∅).
Proof. We need to prove: (∀n ∈ N, s0, . . . , sn ∈ S, t1, . . . , tn ∈ T : n < 1 ∨ s0 6= sn ∨ ∃1 ≤ k ≤ n : (sk−1, tk, sk) 6∈→) ⇔ (∀t1, . . . tn ∈ T : •t1 ∩ tn• = ∅ ∨ (∃1 ≤ k < n : tk • ∩ • tk+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. 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 0 = (P 0, T 0, F 0) be sound WF-nets, let λT be the T -mapping, then λT (N ) ≤T λT (N 0) if and only if: λT (N ) ⊆ λT (N 0) 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 6∈ T 0, then the traces in N that contain t are not traces of N 0. Hence, language inclusion cannot hold. tu 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 0 = (P 0, T 0, F 0), be sound WF-nets, let λα be the α-mapping, then λα(N ) ≤α λα(N 0) if and only if: λα(N ) ⊆ λα(N 0) Theorem 4. (λα, ≤α, ∅) is a negative abstraction.
Proof. We need to prove that ¬(λα(N ) ≤α λα(N 0)) ⇒ ¬(L(N ) ⊆ L(N 0)) which can be rewritten to L(N ) ⊆ L(N 0) ⇒ λα(N ) ≤α λα(N 0) which follows straightforward from the definition of λα. tu
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
B
C A
D
A
B
D λα(N ) ⊆ λα(N 0) 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 0) = {(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 6∈ σ ⇒ ∃b ∈ T : b ∈ σ ∧ (a, b) 6∈ λ∞(N ) ∧ (b, a) 6∈ λ∞(N ). Proof. Assume there is an a ∈ T and a 6∈ σ (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 t1, t2 (•t1 = •t2), A A > C D ⊥ >
F G E
A A D > ⊥
B B E A
D A D
C
B such that after t1 a can still follow, but after executing t2 a cannot follow. Due to the fact that the net is acyclic and free-choice, a cannot precede t2, i.e., if a can, via firing some transitions, mark the preset of t2 then also the preset of t1 is marked and hence a can execute again. Since a is not in σ, we have chosen t2, and thus t2 ∈ σ. Also because a cannot follow t2, and t2 cannot follow a, (a, t2) 6∈ λ∞(N ) ∧ (t2, a) 6∈ λ∞(N ). tu
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. Definition 10 ( ∞-Comparator). Let N = (P, T, F ), N 0 = (P 0, T 0, F 0) be sound FC-nets adhering to the {Acyclic} characterisation, let λ∞ be the ∞mapping, then λ∞(N ) ≤∞ λ∞(N 0) if and only if: 1. T = T 0 2. λ∞(N ) ⊆ λ∞(N 0) 3. (∀(a, b) ∈ λ∞(N 0) : (a, b) ∈ λ∞(N ) ∨ (b, a) ∈ λ∞(N ) ∨ (∃c ∈ T : ((a, c) ∈ λ∞(N ) ∨ (c, a) ∈ λ∞(N )) ∧ (b, c) 6∈ λ∞(N 0) ∧ (c, b) 6∈ λ∞(N 0))) Theorem 6. (λ∞, ≤∞, {Acyclic}) is a positive abstraction.
Proof. We need to prove: λ∞(N ) ≤∞ λ∞(N 0) ⇒ L(N ) ⊆ L(N 0).
We prove this by contradiction, thus L(N ) 6⊆ L(N 0) but λ∞(N ) ≤∞ λ∞(N 0). By definition, this means there is a trace σ ∈ L(N ) such that σ 6∈ L(N 0).
Now it remains to prove that this σ does not exist. We prove this by induction on the prefix of the trace. Let σ = ht1, . . . , tk−1, tk, . . . , tmi be a trace, the prefix of σ (denoted by σprefix ) are transitions before position k (i.e., σprefix = ht1, . . . , tk−1i). It remains to show that if the prefix of σ corresponds to a prefix of a trace σN0 ∈ L(N 0) then tk has to be directly executable in N 0 after having executed this prefix.
Base case k = 1. In this case, the prefix is empty and by definition we always start with an unique start activity, hence both models can execute >.
Inductions hypothesis: assume σprefix = ht1, . . . tk−1i corresponds to a prefix of a trace in N 0, then there are two options: (1) tk cannot follow σprefix in N 0, or (2) tk cannot follow σprefix directly in N 0, i.e., there is at least on transition in between σprefix and tk.
(1) If tk cannot follow σprefix in N 0, then either tk 6∈ T 0 (not possible due to clause 1) or there is an alternative activity ti ∈ σ (Thm. 5). Note that this alternative activity has to be in σprefix , because else from σprefix it cannot follow that tk cannot follow σprefix in N 0. This latter option cannot happen due to clause 2 (else (ti, tk) ∈ λ∞(N ) but (ti, tk) 6∈ λ∞(N 0)). Hence tk must be able to follow σprefix in N 0.
(2) When tk cannot directly follow σprefix this means there is an activity between σprefix and tk in N 0. We denote this activity with b ∈ T 0. We know that (b, tk) ∈ λ∞(N 0) but also that (tk, b) 6∈ λ∞(N 0) (else b does not need to be between σprefix and tk, by free-choiceness and soundness). Furthermore, by the absence of loops and soundness, we know that b 6∈ σprefix (else b can be followed by b in N 0). Then there are two options; (a) either b can follow σprefix in N , or (b) b cannot follow σprefix in N .
(a) Since (tk, b) 6∈ λ∞(N 0) it follows from clause 2, that (tk, b) 6∈ λ∞(N ). This means that if b can follow σprefix in N , it has to be executed before tk is executed. In σ this is not the case, i.e., there is no activity executed between σprefix and tk, and Thm. 5 yields that there has to be an alternative activity for b in σ (note that it does not need to be an alternative activity for b in N 0) and by free-choiceness it has to be before tk, thus in σprefix . From this it follows that b cannot follow σprefix in N . We only need to prove that part (b) yields a contradiction. (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 0, we obtain that (a, b) ∈ λ∞(N 0), but also (a, b) 6∈ λ∞(N ) (note that (b, a) 6∈ λ∞(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) 6∈ λ∞(N 0) ∧ (c, b) 6∈ λ∞(N 0). 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 tk. If c can be executed after tk, then dependent on the activities chosen before tk, c can either be executed or not, which violates the free-choice property. Since (c, tk) ∈ λ∞(N ), it follows that c has to be in σprefix , and thus no b can be between σprefix and tk in N 0.
From this it follows that both models can execute tk 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 0). Thus by contradiction, we have shown that λ∞(N ) ≤∞ λ∞(N 0) ⇒ L(N ) ⊆ L(N 0). tu
In case T = T 0, we can decide language inclusion based on the ∞-mapping. However, in general it is the case that T 6= T 0. Therefore, we extend our approach to the case in which T ⊂ T 0. Note that we do not need to consider the case that T 0 ⊂ T as language inclusion cannot hold.
In order to achieve T = T 0, we have the following reduction on N 0: – Remove all transitions t ∈ (T 0 \ T ) from N 0 – 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 0. 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 0.
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 0, then our comparator always yields true.
Theorem 7. (λ∞, ≤∞, {Acyclic}) is complete, i.e., for two acyclic free-choice WF-nets N and N 0, we have λ∞(N ) ≤∞ λ∞(N 0) ⇐ L(N ) ⊆ L(N 0). Proof. We prove this by contradiction. Assume L(N ) ⊆ L(N 0), but λ∞(N ) ≤∞ λ∞(N 0) 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 0. Since T is sound, this means x occurs in at least one trace and this trace cannot occur in L(N 0). 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 0). By definition, this means there is a word such that A
A
E B C
B
E
D
C
D
B A
C E Fig. 7: Two process models where using the ∞-mapping gives a false positive.
D
A
B
D σ = h. . . , x, . . . , y, . . .i, but this trace cannot be in L(N 0), else this relation was also included in λ∞(N 0).
Assume clause 3 is not valid, this means that: ∃(a, b) ∈ λ∞(N 0) : (∀c ∈ T : ¬((a, c) ∈ λ∞(N ) ∨ (c, a) ∈ λ∞(N )) ∨ (c, b) ∈ λ∞(N 0) ∨ (b, c) ∈ λ∞(N 0)) has to hold (negation of the clause 3). Recall that due to > and ⊥, λ∞(N 0) 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 0) which is not possible due to the acyclicness. Thus, in N 0 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.
A
C
G B D
E
F Fig. 9: For the k-mapping, we cannot find a value for k such that it yields that the right model is language included in the left model, but does not yield that the left model is language included in the right 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 h...EGC...i 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. 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. 5
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.