We consider the problem of synthesizing a bounded place / transition Petri net from a labelled prime event structure with cutting context, which actually is the most expressive notion for the specification of the nonsequential behaviour of concurrent systems allowing for a solution of the Petri net synthesis problem. The existing solution method is mainly of theoretical value and not applicable in practise in general. As a step towards practical application we develop an algorithm solving the synthesis problem using the technique of wrong continuations. We give a characterization of exact solutions, present an implementation of the algorithm and show first experimental results.
In [
As usual in region based theory, the places of the synthesized net are computed as
non-negative integral solutions of a linear inequation sys tem. As mentioned in [
In [
As a step towards practical application we adapt the technique of wrong
continuations from [
We use N to denote the set of non-negative integers . A multiset over a set A is a function m : A → N. For an element a ∈ A the number m(a) determines the number of occurrences of a in m. Addition + on multisets is defined by (m + m′)(a) = m(a) + m′(a). The relation ≤ between multiset is defined through m ≤ m′ ⇐⇒ ∃m′′(m + m′′ = m′). In case m(a) > 0 we also write a ∈ m. The multiset m satisfying ∀a ∈ A : m(a) = 0 we call empty multiset.
Given a binary relation R ⊆ A × A over A, the symbol R+ denotes the transitive closure of R. A directed graph is a tuple G = (V, →), where V is its set of nodes and →⊆ V × V is its set of arcs. As usual, given a binary relation →, we write v → w to denote (v, w) ∈→. In this case, v is called pre-node of w and w is called post-node of v. For v ∈ V we denote by • v = { w ∈ V | w → v} the preset of v, and by v• = { w ∈ V | v → w} the postset of v.
A partial order is a directed graph (V, <), where <⊆ V × V is an irreflexive and transitive binary relation. In the context of this paper, a partial order is interpreted as an ”earlier than”-relation between events. A node v is called maximal if v• = ∅, and minimal if • v = ∅. A subset W ⊆ V is called left-closed if ∀v, w ∈ V : (v ∈ W ∧ w < v) =⇒ w ∈ W. For a left-closed subset W ⊆ V , the partial order (W, <| W × W ) is called prefix of (V, <), defined by W . The set S(W ) = { v ∈ V \ W | w < v =⇒ w ∈ W } is the set of the direct successors of the prefix defined by W . The left-closure of a subset W is given by the set W ∪ { v ∈ V | ∃ w ∈ W : v < w} . Given two partial orders po1 = (V, <1) and po2 = (V, <2), we say that po2 is a sequentialization of po1 if <1⊆ <2 (note that a sequentialization in general does not refer to a total order or a sequence; a sequentialization being a total order is called a linearization). By <s⊆ < we denote the smallest subset <s of < which fulfils (<s)+ = <, called the skeleton of <. The distance d(u, w) between two nodes u, w of partial order (V, <) with u < w is defined by d(u, w) := min{ n | u = v0 <s v1 . . . <s vn = w} .
A labelled partial order (LPO) over T is a triple (V, <, l), where (V, <) is a partial
order, and l : V → T is a labelling function on V . We use all notations defined for
partial orders also for LPOs. For a finite subset W ⊆ V , we define the multiset l(W )
by l(W )(x) = |{ v ∈ W | l(v) = x}| . LPOs are used to represent partially ordered runs
of Petri nets. Such runs are distinguished only up to isomorphism [
A net is a triple N = (P, T , F ), where P is a set of places, T is a set of transitions, satisfying P ∩ T = ∅, and F ⊆ (P ∪ T ) × (T ∪ P ) is a flow relation. Places and transitions are called the nodes of N .
(P, T , F, W ), where (P, T , F ) is a net with finite sets of places and transitions, and W : F → N \ { 0} is a weight function. A marking of a p/t-net N = (P, T , F, W ) is a function m : P → N. A marked p/t-net is a pair (N, m0), where N is a p/t-net, and m0 is a marking of N , called initial marking.
We extend the weight function W to pairs of net elements (x, y) ∈ (P × T )∪(T × P ) satisfying (x, y) 6∈ F by W (x, y) = 0. A multiset of transitions is called a transition step. A transition step τ is enabled to occur in a marking m of N if ∀p ∈ P : m(p) ≥ Pt∈T τ (t)· W ((p, t)). If τ is enabled to occur in a marking m, then its occurrence leads to the new marking m′ defined by m′(p) := m(p)+Pt∈T τ (t)· (W ((t, p))−W ((p, t))) for all p ∈ P .
An LPO lpo = (V, <, l) over T is enabled to occur in a marking m of N if m(p) + Pv′∈V ′ (W (l(v′), p) − W (p, l(v′))) ≥ Pv∈S(V ′) W (p, l(v)) for each prefix lpo′ = (V ′, <, l) of lpo and each place p. If lpo is enabled to occur in a marking m, then its occurrence leads to the new marking m′ defined by m′(p) := m(p) + Pv∈V (W (l(v), p) − W (p, l(v))) for all p ∈ P .
We use labelled prime event structures (LPES) to represent the non-sequential
behaviour of p/t-nets. An LPES consists of a set of events label led with action names,
a partial order representing an “earlier than”-relation be tween events and a set of
socalled consistency sets, where left-closed consistency se ts represent single runs of a
net. Events which are never in the same consistency set are assumed to be in conflict
and to belong to alternative runs. Labels of events represent transition names.
Definition 2 (Labelled prime event structure [
The elements of Con are called consistency sets. An inifinite set X is a consistent subset of E if ∀Y ⊆ X, Y finite : Y ∈ Con. The conflict relation # between events of pes is defined by e#e′ ⇔ { e, e′} 6∈ Con.
A tuple (E, Con, ≺, l), where (E, Con, ≺) is a PES and l : E → T is a labelling function on E, is called labelled prime event structure (LPES) over T .
As LPOs, LPES are distinguished only up to isomorphism [
For a set of events E′ and C ∈ Conpre we denote by C ⊕ E′ the set C ∪ E′, if C ∪ E′ ∈ Conpre and C ∩ E′ = ∅. If E′ = { e} , we also write C ⊕ e to denote C ⊕ { e} . Such an E′ is a suffix of C, and C ⊕ E′ is an extension of C. Let C, D ∈ Conpre with C ⊆ D. The set SD(C) = { v ∈ D \ C | w ≺ v =⇒ w ∈ C} is the set of the direct successors of C in D. For a left-closed subset F ⊆ E and a subset of consistency sets Con′F ⊆ ConF := { C ∈ Con | C ⊆ F } satisfying the properties of the definition of LPES, the LPES (F, Con′F , ≺| F× F , l| F ) is called prefix of the LPES (E, Con, ≺, l), defined by F and Con′F .
In [
A prime token flow event structure is an LPES together with a token flow function. Since equally labelled events represent different occurrences of the same transition, they are required to have equal intoken flow. Since not all tokens which are produced by an event are consumed by further events, there is no such requirement for the outtoken flow. It is assumed that there is a unique initial event producing the initial marking.
ture over T is a pair (lpes, x), where lpes = (E, Con, ≺, l) has a unique minimal event einit with ∀e 6= einit : l(einit) 6= l(e) and l(E \ { einit} ) ⊆ T and x :≺→ NP is a token flow function with ∀e, e′ ∈ E : l(e) = l(e′) ⇒ IN x(e) = IN x(e′).
Two events are called strongly identical (w.r.t. a token flow function), if they are
labelled with the same action name and depend on the same events with identical token
flow. In [
Definition 4 (Strongly identical events [
A token flow unfolding of a marked p/t-net is a prime token flow e vent structure, in which intoken and outtoken flows are consistent with the arc weights resp. the initial marking of the net within each left-closed consistency set. It is also required that the token flow on a skeleton arc may not be zero, that means only real causal dependencies are represented in an unfolding.
Definition 5 (Token flow unfolding [
Token flow unfoldings are distinguished only up to isomorphism [
Mark(C)(p) := m0(p) +
X(W (l(e), p) − W (p, l(e)) (p ∈ P ) e∈C is a reachable marking of (N, m0), called the final marking of C. Every final marking in Unf max is reachable in (N, m0), and every reachable marking is a final marking in Unf max.
Since the maximal unfolding is infinite whenever the original net has infinite
behaviour, there are approaches for constructing finite and complete prefixes. The
essential feature of the existing unfolding algorithms computing finite, complete prefixes is
the use of cutoff events, beyond which the unfolding can be truncated without loss of
information. In [
Let Unf max be the maximal token flow unfolding of a marked p/t-net (N, m0). We denote by Con and Conpre the sets of consistency sets and left-closed consistency se ts of Unf max. A cutting context is a triple Θ = (≈, ⊳, { Ce} e∈E ), where: 1. ≈ is an equivalence relation on Conpre, capturing the information which is intended to be retained in a complete prefix. In the standard case ≈=≈mar, this is the set of reachable markings, i.e. C ≈mar C′ if Mark(C) = Mark(C′). 2. ⊳ is a so-called adequate order on Conpre which refines ⊂. All ⊳-minimal leftclosed consistency sets in each equivalence class of ≈ will be preserved in a complete prefix (in algorithms, ⊂ is often used directly). 3. ≈ and ⊳ are preserved by finite extensions of left-closed consisten cy sets. 4. { Ce} e∈E is a family of subsets of Conpre specifying the set of left-closed consistency sets used to decide whether an event can be designated as a cutoff event. In the standard case, Ce contains the local consistency sets of Unf max.
Roughly spoken, a prefix of Unf max is complete, if each equivalence class w.r.t. ≈ is represented once in it. Hence, for the relation ≈mar, each reachable marking is represented by a left-closed consistency set of a complete p refix.
With these notions, cutoff events can be defined in a ”static way” without referring
to a specific algorithm building the unfolding. The set CutOff of static cutoff events is
defined together with the set Feas of feasible events. Feasible events are precisely those
events whose causal predecessors are not cutoff events, and as such must be included
in the prefix determined by the static cutoff events. An event e is a static cutoff event,
if it is feasible, and there is C ∈ Ce such that C ⊆ Feas \ CutOff, C ≈ [e], and
C ⊳ [e]. The token flow unfolding Unf Θ defined by the set of events Feas is called the
canonical prefix of Unf max. In [
In this section we briefly recall the synthesis approach from [
In this paper we use the finite representation of the non-sequ ential behaviour of a
concurrent system from [
lpes = (E, Con, ≺, l) together with a finite cutoff-list Cut = (Di, ei)i∈I consisting of maximal events ei ∈ E and left-closed consistency sets Di with Di ⊂ [ei] (with some finite index set I). We assume that lpes has a unique minimal event e0 with empty label.
An example of an LPES with cutoff-list is shown in Figure 1. In general, each LPES underlying the complete finite prefix of the maximal unfolding of a bounded p/tnet together with its list of cutoff events (ei)i∈I and the set of consistency sets (Di)i∈I with [ei] ≈ Di forms an LPES with cutoff list. We will use an LPES with cutoff-list to synthesize a p/t-net having the runs specified by lpes and satisfying Mark(Di) = Mark([ei]) for each i. An LPES with cutoff-list serves as a finite specification of a n infinite LPES, a so-called completion.
Definition 7 (Completion). Let lpes = (E, Con, ≺, l) be an LPES with cutoff-list Cut = (Di, ei)i∈I . A completion of (lpes, Cut) is an LPES lpes′ = (E′, Con′, ≺′, l′) with the following properties: 1. lpes is a prefix of lpes′. 2. If C ∈ Conpre such that ∀i : ei 6∈ C, and C ⊕ e ∈ Con′pre for some event e, then
C ⊕ e ∈ Conpre. 3. Let ≈ be the smallest equivalence relation on Con′pre satisfying: (a) [ei] ≈ Di for each i. (b) ≈ is preserved by finite extensions.
Then ≈ satisfies: (c) If C′ ∈ Con′pre, then there is C ∈ Conpre such that ∀i : ei 6∈ C and C′ ≈ C. (d) For C′ ≈ C′′ and each extension E′ = { e′} of C′ there is an extension E′′ = { e′′} of C′′ with l′(e′) = l′(e′′) (note that this property is symmetric).
This definition is stronger than the one given in [
As an example, the maximal unfolding of a bounded p/t-net is a completion of its complete finite prefix using ≈=≈mar. The equivalence relation ≈ represents the reachable states and it is required that all reachable states are represented in lpes. The cutoff-list Cut = (Di, ei)i∈I specifies that exactly the extensions of Di should also be possible extensions of [ei] in a completion. Note that not all maximal events of lpes need to be cutoff events. If a maximal event e is not a cutoff event, then the final marking of [e] is intended not to enable any further transition occurrence. In the rest of the paper we consider the following formal problem statement: – Given: A finite LPES lpes = (E, Con, ≺, l) over a finite alphabet of transition names T together with a cutoff-list Cut = (Di, ei)i∈I . – Searched: A marked p/t-net (N, m0) with set of transitions T such that the partial language corresponding to its unfolding is minimal with the property, that it includes the partial language corresponding to a completion of (lpes, Cut).
In [
In order to present the constraints of the equation system defining a feasible place
p (resp. a region), we denote by E = { e0, . . . , en} the list of events, by { C0, . . . , Cm}
the list of left-closed consistency sets which are maximal w .r.t. the subset-relation and
by { t0, . . . , tl} the list of transitions. The table 1 shows the variables together with their
constraints and their interpretation as used in the approach of [
In this section we adapt the notions of wrong continuations and separation
representation w.r.t. partial language based specifications [
In the following we denote by x a region as defined in the previous section (that
means an integral non-negative solution of the equation sys tem presented in the
previous section) and by px the place defined by x. An idea to get a finite representation is to
separate behavior specified by (lpes, Cut) from behavior not specified by (lpes, Cut)
by a finite set of regions (see [
Definition 8 (Exact solution). A solution (N, m0) of the considered synthesis problem is called exact solution, if the partial language corresponding to its maximal unfolding equals the partial language corresponding to a completion of (lpes, Cut).
For example, a bounded p/t-net is an exact solution w.r.t. th e specification given by the complete finite prefix of its maximal unfolding. Formally we split a wrong continuation into a prefix belonging to the partial language of lpes, a subsequently enabled step of transitions and an additional transition which should be prohibited. Definition 9 (Wrong continuation). Let lpes = (E, Con, ≺, l) be a finite LPES over a finite alphabet of transition names T together with a cutoff-list Cut = (Di, ei)i∈I .
A wrong continuation of (lpes, Cut) is a triple (C, τ, t), where – C is a left-closed consistency set C of lpes such that lpoC does not contain a cutoff event (∀i : ei 6∈ C). – There is a maximal consistency set D of lpes with C ⊆ D, τ ≤ l(SD(C)) and τ (t) = l(SD(C))(t) (τ may be the empty multiset). – There is no maximal consistency set D′ of lpes with C ⊆ D′, τ ≤ l(SD′ (C)) and τ (t) < l(SD′ (C))(t).
We call lpoC the prefix and τ the follower step of the wrong continuation.
According to the specification (lpes, Cut), the prefix lpoC of a wrong continuation (C, τ, t) leads to marking enabling τ , but not enabling τ + t. Some of the wrong continuations of (lpes, Cut) shown in Figure 1 are: w1 = ({ e0} , {} , b) (prohibiting b in the initial marking), w2 = ({ e0} , {} , d) (prohibiting d in the initial marking) and w3 = ({ e0} , { e1} , a) (prohibiting 2a in the initial marking).
Theorem 1. A solution (N, m0) of the considered synthesis problem is an exact solution if and only if for each wrong continuation (C, τ, t) of (lpes, Cut) the prefix lpoC leads to marking not enabling τ + t.
Proof. Let (lpesu, x) be the maximal token flow unfolding of (N, m0) and lpesc be a completion of (lpes, Cut) such that the partial language corresponding to lpesu includes the partial language corresponding to lpesc.
”if”: Assume that (N, m0) is not an exact solution. Let lpo = (V ∪ { e} , ≺, l) belong to the partial language corresponding to lpesu, but not to the partial language corresponding to lpesc, such that (V, ≺, l) belongs to the partial language corresponding to lpesc. Let ≈ be the equivalence relation on lpesc from the definition of completions. Using the properties 3.(a),3.(b),3.(d) of the definition of completions and the properties of places defined by regions, it can be proven iteratively, that C ≈ C′ =⇒ Mark(C) = Mark(C′). By property 3.(c) there is a left-closed consistency set V ′ of lpes with V ′ ≈ V and containing no cutoff-events. Since lpo does not belong to lpesc and from property 2. of the definition of completions, there is a wrong continuation (C, τ, l(e)) with C ⊆ V ′ and l(C) + τ = l(V ′). From Mark(V ′) = Mark(V ) we deduce that the transition l(e) is enabled in Mark(V ′), i.e. lpoC leads to a marking enabling τ + l(e).
”only if”: Assume that there is a wrong continuation (C, τ, t) of (lpes, Cut), such that after occurrence of the prefix lpoC the transition step τ + t is enabled in (N, m0). Let lpoC = (C, ≺, l) and W ⊆ SD(C) be a subset of direct successors of lpoC in a maximal consistency set D of lpes such that l(W ) = τ and C ⊕ W ∈ Con (such W exists by the definition of wrong continuations). The LPO lpoC⊕W belongs to the partial language corresponding to lpes and, by assumption, its occurrence leads to a marking enabling t. That means, there is an extension C ⊕ W ⊕ e with l(e) = t such that lpoC⊕W ⊕e belongs to the partial language corresponding to lpesu. On the other side, according to the property 2. of the definition of completions, lpoC⊕W ⊕e does not belong to the partial language corresponding to lpesc. That means (N, m0) is not an exact solution.
Consider a wrong continuation (C, τ, t). Our aim is to compute a region x such that after the occurrence of the prefix lpoC the marking of px does not enable the transition step τ + t. This can directly be expressed by a linear constraint using the variables of the linear equation system defining regions:
In order to compute such a region x w.r.t. a wrong continuation (C, τ, t), we add the above constraint to the linear equation system defining regions. For each wrong continuation a separate constraint leading to a separate linear inequation system needs to be considered. Considering for example Figure 1, the wrong continuation w1 = ({ e0} , {} , b) is prohibited by the place in c• ∩ • b. 5
Before formulating the synthesis algorithm and presenting its implementation we
consider two parameters influencing the solution net resulting from a separation
representation [
Considering the linear inequation system corresponding to a wrong continuation, a
nonnegative integral solution can be computed which minimizes a given linear target
function φ. Such a target function can be used to produce “simple” places [
In the context of this paper, for example, it is possible to minimize the token flows ai,j along edges and the residual token flows ri,k . In our case, a target function has the following general form φ = α1 ·
X γi,k · ri,k + α2 · i,k
X βi,j · ai,j , i,j with αi, γi,k, βi,j ∈ R0+. The use of different target functions leads to different solutions. Our experiments have shown that the simple target function φrest = Pi,k ri,k is a good choice in most cases in order to compute “simple” places, since minimizing the residual token flows ri,k produces places prohibiting many wrong continuations at once. In several cases also the target function φpenalty = Pi,j βi,j · ai,j , where βi,j = 1 if d(ei, ej ) = 1 and βi,j = 50 else, yields good results, since it leads to places representing only local dependencies. It is also possible to distinguish between edges with different distances using βi,j = d(ei, ej ), or to combine these target functions. 5.2
In general, a place does not prohibit only one wrong continuation. If a wrong
continuation w is prohibited by a place, which was already computed previously, it is not
necessary to compute a separate solution for w. Consider two wrong continuations w1, w2. It
is possible that the solution p1 prohibiting w1 also prohibits w2, but that the solution p2
prohibiting w2 does not prohibit w1. In such a case, it is better to consider w1 first, since
this order leads to a net with less places. That means, the order in which wrong
continuations are considered, the so-called wct-ordering , has an influence on the synthesis
result [
Unfortunately, there is still no theory on optimizing the wct-ordering in the above sense. Therefore, in our experiments we considered several different orderings ≤wct based on the following definitions for wrong continuations w1 = (C1, τ1, t1), w2 = (C2, τ2, t2): – w1 <C w2 :⇔ | C1| < | C2| (can be used to consider small prefixes before big prefixes, or vice versa) – w1 <dC w2 :⇔ d(C1) < d(C2), where d(C) := max{ d(e0, ei) | ei ∈ C} (can be used to consider short prefixes before long prefixes, or vice versa) – w1 <τ w2 :⇔ | τ1| < | τ2| (can be used to consider small follower steps before big follower steps, or vice versa)
These components can be combined in different ways to derive orderings of wrong continuations for the synthesis algorithm. In our experiments we identified the following wct-ordering as a good choice:
≤wct=<dC ∪(=dC ∩ <C ) ∪ (=C ∩ =dC ∩ <τ )
Note that this is a partial order. Unordered wrong continuations are ordered randomely by the algorithm. As a reference, the tool also offers the possibility to use the completely random order ≤rwncdt . 5.3
We are now able to present the synthesis algorithm. First we construct the equation system defined by the basic constraints from table 1 (line 1) and start with an empty set S of solutions (line 2). In the next step we create the list of wrong continuations { w1, . . . , wn} ordered w.r.t. ≤wct (line 3; prefixes are computed using a breadth-first approach; for the follower step we consider the direct successors of a prefix, see Definition 9). Now we can iterate over this list (lines 4 - 19). In the i-th iteration we consider the wrong continuation wi: – first we test, whether wi is prohibited by one of the already computed solutions in
S (lines 6 - 11). – if this is the case, we consider the next wrong continuation (lines 12 - 13). – if this is not the case (lines 14 - 17), we add the constraint co rresponding to wi (table 2) to the inequation system (line 15), add the computed solution to S (if one exists; line 16), and remove the constraint (line 17). Require: LPES with cutoff list (lpes, Cut), target function φ , ordering ≤wct 1: litok ← getF lowConstraints(lpes, Cut) 2: S ← ∅ 3: { w1, . . . , wn} ← getW CT s((lpes, Cut), ≤wct) 4: for i = 1 to n do 5: redundant ← f alse 6: for s ∈ S do 7: if wcti.satisf ied(s) then 8: redundant ← true 9: break 10: end if 11: end for 12: if redundant then 13: continue 14: else 15: litok.add(wcti) 16: S ← S ∪ lpsolve(litok, φ) 17: litok.remove(wcti) 18: end if 19: end for 20: (N, m0) ← extractP N et(S) 21: return (N, m0)
Algorithm 1: Synthesis algorithm
Finally we retrieve the solution net from set of solutions S (line 20). All wrong continuations, which cannot be prohibited, are reported (this is not shown in the algorithm for a compact representation).
We use the following optimizations (adapted from [
Altogether, the runtime of the algorithm is exponential in the number of events of the LPES in general, since there are exponentially many prefixes to consider. The runtime can be reduced using heuristics and by grouping wrong continuations, but this is a topic of further research.
The synthesis algorithm is implemented in JAVA as a command line tool. For
computing solutions of linear inequation systems we used the free solver lp solve [
We now briefly present two kinds of experiments evaluating the presented tool. First we considered several p/t-nets and constructed the complete fi nite prefix of their maximal unfolding. This complete finite prefix then served as input LPES with cutoff-list for the synthesis of a new p/t-net, which we compared with the ori ginal net. We used nets which were drawn as simple and intuitive as possible. That means, our goal was to test, whether the used synthesis algorithm was able to reproduce the original net and to analyse the differences.
Figures 1 and 2 show two of the considered p/t-nets together w ith the complete finite prefix of their maximal unfoldings.
It turned out that using Φrest as target function and the wct-ordering ≤wct (from the
last section) it was possible to exactly rediscover the original p/t-net in both presented
examples and also for several other small nets. Note here that for the specification in
Figure 1 there is no other existing notion, which can be used for synthesis. In particular,
this specification cannot be expressed by an LPO-term [
In case of bigger nets with arc weights and more complicated dependency realtions, some additional and / or different places were computed due to a still not optimized combination of target function and wct-ordering (which is a topic of future research). For example, we considered the net in part (a) of Figure 3, constructed the complete finite prefix of its maximal unfolding and got the following result using different target functions: – Part (b): This net was computed using the target function Φrest and the wct-ordering ≤wct. It has one additional and unnessecary gray-coloured place . It prohibits the transition step 2c after the occurrence of a, while there is another place in the original net which prohibits the transition steps 2b, b+c and 2c after the occurrence of a. Fig. 3. A p/t-net (part (a)) and two synthesis result from the comple te finite prefix of its maximal unfolding (parts (b) and (c)) with additional places depending on the used target function.
That means, computing these places in a different order would result in the original net. In order to avoid such unnessecary places it is nessecary to find additional local rules for determining the wct-ordering. – Part (c): This net was computed using the target function Φpenalty and the wctordering ≤wct. It has three more additional and unnessecary gray-coloure d places. These places represent the conflict between the three transitions d, e, f . The original place representing this conflict is non-optimal w.r.t. Φpenalty , since it has more connections to transitions. On the other side, the three gray places are non-optimal w.r.t. Φrest, since tokens remain in some of them after ocurrence of d, e or f .
Another example is shown in Figure 4. Part (a) shows the original net and part (b)
the synthesis result using the target function Φrest and the wct-ordering ≤wct. It has
one additional and unnessecary gray-coloured place which p rohibits the transition step
e in the initial marking, but it is easy to see that also some other places of the original
net probit transition step e in the initial marking. That means (again) that computing
these places in a different order would result in the original net. Note that the gray place
is non-optimal w.r.t. Φpenalty , but on the other side, also several places of the original
net are non-optimal w.r.t. Φpenalty . The net was already considered in [
These first experiments show that it is possible to synthesize simple and intuitive nets using the presented approach, if the local dependency relations between events are simple. For several more complex situations the choice of the target function and the wct-ordering influences the synthesis result and it depe nds on the local dependency relations, which choice is the better on. The local choice of target function and wctordering will be a topic of further research.
Second we evaluated the runtime of the tool using several parametrized p/tnets and their unfolding. Figure 5 shows one of these nets, where the parameter is the number n of tokens in the place in • a ∩ • b. The net has 2n different runs and can be seen as one of the “worst cases” for the presented synthesis approach. Our algorithm was able to exactly rediscover the original p/t-net. Of course runti me increased rapidely when increasing the parameter n due to the amount of prefixes and wrong continuations which have to be computed.
The following table shows the runtime for different choices of n using Φrest as target function and the wct-ordering ≤rwncdt . The average runtime was computed over several runs of the algorithm using a system with i7-6500U CP U having 2.50 GHz. n WCT constraints Average runtime 1 8 ≈ 40 ms 2 24 ≈ 50 ms 3 64 ≈ 130 ms 4 160 ≈ 700 ms 5 384 ≈ 5200 ms 6 896 ≈ 76000 ms
This example shows that there is still work to do, but there are already first approaches to improve such situations (not implemented yet). For example, the above situation can be first considered as an infinite iteration (easy to solve, see above), and then the number of iterations can be restricted by an appropriate place. 7
In this paper we characterized exact solutions of the region based synthesis of bounded p/t-nets from LPES with cutoff-list using wrong continuati ons and presented an implementation of the according synthesis algorithm. Experimental results are promising, showing that simple dependency relations among transitions can be rediscovered exactly. For more complicated dependency situations there are two parameters of the algorithm - target function and wct-ordering - which can be adj usted. The local choice of these parameters is a topic of further research.
In order to improve runtime, we plan to develop heuristics for the grouping of wrong continuations (that means, a solution is searched prohibiting a group of several wrong continuation at once) and for the consideration of a small subset of the set of all wrong continuations (which is likely to “represent” the whole set). As a basis for both aspects we are working on a theory concerning an optimal ordering of wrong continuations.
Concerning practical applications, we are developing a two-step approach in the area of process mining using our synthesis framework: – First step (preprocessing): Construct an LPES with cutoff- list from an event log through detecting loops, causality, concurrency and noise. Since LPES with cutofflist is a more general model than p/t-nets, causal structure s can be detected with less loss of information than with approaches using directly Petri net based models. That means an LPES with cutoff-list has a low representation al bias in the context of process mining.
– Second step (synthesis): Synthesize a Petri net from the result of the first step.