=Paper=
{{Paper
|id=Vol-1592/paper05
|storemode=property
|title=Synthesis of bounded Petri Nets from Prime Event Structures with Cutting Context
|pdfUrl=https://ceur-ws.org/Vol-1592/paper05.pdf
|volume=Vol-1592
|authors=Gabriel Juhás,Robert Lorenz
|dblpUrl=https://dblp.org/rec/conf/apn/Juhas016
}}
==Synthesis of bounded Petri Nets from Prime Event Structures with Cutting Context==
<pdf width="1500px">https://ceur-ws.org/Vol-1592/paper05.pdf</pdf>
<pre>
    Synthesis of bounded Petri Nets from Prime Event
             Structures with Cutting Context

                            Gabriel Juhás1 and Robert Lorenz2
                1
                  SLOVAK UNIVERSITY OF TECHNOLOGY in Bratislava
                Faculty of Electrical Engineering and Information Technology
                      Ilkovičova 3, 812 19 Bratislava, Slovak Republic
                                gabriel.juhas@stuba.sk
                              2
                                 UNIVERSITY OF AUGSBURG
                          Department of Applied Computer Science
                 robert.lorenz@informatik.uni-augsburg.de


       Abstract. In this paper we present token flow based synthesis of bounded Petri
       nets from labelled prime event structures (LPES) associated with a cutting con-
       text. For this purpose we use unfolding semantics based on token flows.
       Given an infinite LPES represented by some finite prefix equipped with a cutting
       context and cut-off events it is shown how to synthesize a bounded Petri net,
       such that the unfolding of the synthesized net preserves common prefixes and
       concurrency of runs of the LPES. The partial language of this unfolding is the
       minimal partial language of an unfolding of a Petri net, which includes the partial
       language of the LPES.
       This result extends the class of non-sequential behaviour, for which Petri nets can
       be synthesized, because finite representations of infinite LPES by a finite prefix
       equipped with a cutting context and cut-off events are more expressive than finite
       representations of infinite partial languages by terms.


1   Introduction
Non-sequential Petri net semantics can be classified into unfolding semantics, process
semantics, step semantics and algebraic semantics [11]. While the last three semantics
do not provide semantics of a net as a whole, but specify only single, deterministic com-
putations, unfolding models are a popular approach to describe the complete behavior
of nets accounting for the fine interplay between concurrency and nondeterminism.
    To study the behavior of Petri nets primarily two models for unfolding semantics
were retained: labelled occurrence nets and event structures. The standard unfolding
semantics for the general class of place/transition Petri nets or p/t-nets is based on
the developments in [12, 3] (see [7] for an overview) in terms of so called branch-
ing processes, which are acyclic occurrence nets having events representing transition
occurrences and conditions representing tokens in places. Branching processes allow
events to be in conflict through branching conditions. Therefore, branching processes
can represent alternative processes simultaneously (processes are finite branching pro-
cesses without conflict). Branching processes for p/t-nets individualize tokens having
the same ”history”, i.e. several (concurrent) tokens produced by some transition occur-
rence in the same place are distinguished through different conditions. One can define




                                              58
a single maximal branching process, called the unfolding of the system, capturing the
complete non-sequential branching behavior of the p/t-net.
    A problem with unfoldings is that they are infinite whenever the original p/t-nets
have infinitely many runs. It turns out that Petri net unfoldings can often be truncated
in such a way that the resulting prefixes, though finite, contain full information w.r.t.
some behavioral property. Such prefixes are complete for this property. In the case of
bounded nets, according to a construction by McMillan [10] a complete finite prefix
preserving full information on reachable markings can always be constructed. In the
case of bounded nets, the construction of unfoldings and complete finite prefixes is
well analyzed and several algorithmic improvements are proposed in literature [4, 8, 6].
The essential feature of the existing unfolding algorithms is the use of cut-off events,
beyond which the unfolding starts to repeat itself and so can be truncated without loss of
information. In [8] a generalized, parametric setup, called cutting context is proposed,
in which completeness can be discussed in a uniform and algorithm-independent way.
    By restricting the relations of causality and conflict of a branching process to events,
one obtains a labelled prime event structure (LPES) [18] underlying the branching pro-
cess, which represents the causality between events of the branching process. Events
not being in conflict define consistency sets, that is, an LPES is a partially ordered set
of events (transition occurrences) together with a set of (so called) consistency sets [18].
”History-closed” (left-closed) consistency sets correspond to processes and their under-
lying runs in the unfolding. Thus, event structures are in their nature a branching time
model of computation, which enable to specify common history of runs.
    In [1] we presented a new unfolding approach, so called token flow unfoldings based
on LPES, which avoid the representation of isomorphic processes or even processes
with isomorphic runs in many situations. The new unfolding semantics combines LPES
with so called token flows, which were developed in [5] for a compact representation of
processes. Token flows abstract from the individuality of conditions of a branching pro-
cess and encode the flow relation of the branching process by natural numbers, which
are assigned to the edges of the partially ordered run underlying a branching process for
each place. Such a natural number assigned to an edge (e, e ) represents the number of
tokens produced by the transition occurrence e and consumed by the transition occur-
rence e in the respective place. An LPES with assigned token flow information is called
a token flow unfolding if each process is represented through a left-closed consistency
set with assigned token flows corresponding to the process.
    Besides their importance as the fundamental model of concurrency, event structures
become also interesting to applications: Recently, Dumas in [2] advocates event struc-
tures, and in particular labelled prime event structures, as the unifying representation
of process models and event logs in the context of process mining. In the Outlook of
the paper [2], it is stated that ”the use of event structures for process model synthesis
would require new techniques to be developed or existing ones to be heavily adapted”.
The Outlook of the paper [2] also states that ”A key challenge is handling repeated be-
havior.” and later continues that ”synthesizing a process model from the event structure
derived from a log requires being able to detect and isolate repeated behavior.” In this
paper we propose such new techniques handling repeated behavior adapting our recent




                                            59
development in the area of synthesis of Petri nets from partial languages [9], which is
basically based on token flows.
    In section 2 we introduce basic mathematical notions and recall the definitions of
LPES and of Petri nets with token flow unfoldings, as they were described in [1]. Fur-
ther, we introduce complete finite prefixes of token flow unfoldings defined in [1].
    Given a labelled prime event structure, to handle repeated behaviour, we propose to
use cutting contexts and to equip the labelled prime event structure with cut-off events.
Then, given an infinite labelled prime event structure represented by some finite pre-
fix equipped with a cutting context and cut-off events it is shown in section 3 how to
synthesize a bounded Petri net, while preserving the shared history and concurrency of
runs. This result extends the class of non-sequential behaviour, for which Petri nets can
be synthesized, because finite representation of infinite labelled prime event structures
by finite prefix equipped with cutting context and cut-off events is more expressive than
finite representation of infinite partial languages by terms as given in [9].


2     Token Flow Unfolding Semantics of P/T-nets

In this section we recall the definitions of place/transition Petri nets, the unfolding se-
mantics based on token flows as they were described in [1], we recall the theory of
region based synthesis [9], and the theory of complete prefixes of unfoldings proposed
in [8]. We begin with some basic mathematical notations.


2.1   Basic Notions

We use N to denote the nonnegative integers. A multi-set 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. 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 amd 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 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 . By <s ⊆ < we
denote the smallest subset <s of < which fulfils (<s )+ = <, called the skeleton of <.
     A labelled partial order (LPO) is a triple (V, <, l), where (V, <) is a partial order,
and l is a labelling function on V . We use all notations defined for partial orders also
for LPOs. LPOs are used to represent partially ordered runs of Petri nets. Such runs are
distinguished only up to isomorphism [1].




                                           60
2.2   Petri Nets
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 .

Definition 1 (Place/transition-net). A place/transition-net (p/t-net) N is a quadruple
(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) ∈ F by W ((x, y)) = 0. A transition t ∈ N is enabled to occur
in a marking m of N if ∀p ∈ P : m(p) ≥ W ((p, t)). If t is enabled to occur in
a marking m, then its occurrence leads to the new marking m defined by m (p) =
m(p) − W ((p, t)) + W ((t, p)) for all p ∈ P .

2.3   Prime Event Structures
A prime event structure (PES) consists of a set of events, a partial order representing
an “earlier than”-relation between events and a set of so called consistency sets, where
left-closed consistency sets represent single runs. 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 action names.

Definition 2 (Prime event structure). A prime events structure (PES) is a triple pes =
(E, Con, ≺) consisting of a set E of events, a partial order ≺ on E and a set Con of
finite subsets of E satisfying:
 – ∀e ∈ E : {e | e ≺ e} is finite.
 – ∀e ∈ E : {e} ∈ Con.
 – Y ⊆ X ∈ Con =⇒ Y ∈ Con.
 – ((X ∈ Con) ∧ (∃e ∈ X : e ≺ e )) =⇒ (X ∪ {e} ∈ Con).
A consistent subset of E is a subset X satisfying ∀Y ⊆ X, Y finite : Y ∈ Con. The
conflict relation # between events of pes is defined by e#e ⇔ {e, e } ∈ Con.
    A tuple (E, Con, ≺, l), where (E, Con, ≺) is a PES and l is a labelling function on
E, is called labelled prime event structure (LPES).

    Notice that the conflict relation expresses that the respective events are always in
conflict. A PES definition using a binary conflict relation instead of consistency sets
can also be found in the literature [12]. The definition according to [18] used in this
paper is more expressive. Imagine a trivial example with two PES pes = (E, Con, ≺),
pes = (E, Con , ≺) differing just in consistency sets, with E = {a, b, c}, ≺= ∅, Con
given by all subsets of E except {a, b, c} and Con given by all subsets of E including
{a, b, c}. Obviously, the conflict relation for both pes and pes coincide: It is empty. But
intuitively, pes represents a system with three different runs, where in each run at most




                                           61
two events from three will occur in parallel, but never three events can occur in parallel
in a run. On the contrary, pes represents a system where all three events can occur
in parallel in one single run. This difference cannot be captured by a binary conflict
relation.
     As LPOs, LPES are distinguished only up to isomorphism [1]. An LPES, where its
whole set of events E forms a consistent set, we interpret as an LPO, i.e. in this case we
omit the set of consistency sets Con.
     We denote the set of left-closed consistency sets of a LPES lpes = (E, Con, ≺, l)
by Conpre ⊆ Con. If C ∈ Conpre is a left-closed consistency set, then lpoC = (C, ≺
|C×C , l|C ) is an LPO which we interpret as a run given by lpes. We define partial lan-
guage corresponding to lpes as the sequentialization closure of {lpoC | C ∈ Conpre }.
It is denoted by L(lpes). For every event e ∈ E, the finite left-closed consistency set
[e] = {f | f ≺ e} is called a local consistency set.
     For a set of events E  and C ∈ Conpre we denote by C ⊕ E  the fact that 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.
     Finally, we introduce a new notion of history and concurrency preservation of LPES.
Definition 3 (History and concurrency preservation). Let lpes = (E, Con, ≺, l) and
lpes = (E  , Con , ≺ , l ) be two LPES. If there exists a function b : E → E  such
that for each left-closed consistency set C of lpes there holds that b(C) is a left-closed
consistency set of lpes and b|C defines an isomorphism between lpoC and a sequential-
ization of lpob(C) , then we say that lpes preserves common prefixes and concurrency
of runs of lpes.
    In particular, if lpes preserves common prefixes and concurrency of runs of lpes,
then the partial language of lpes includes the partial language of lpes. Basically, the
existence of function b also means, that whenever some runs of lpes share a common
prefix with events in their intersection equal to X, then their b-images in lpes share at
least the prefix with events given by b(X). The runs of lpes are sequentializations of
their b-images, i.e. at least the same amount of concurrency is preserved in each run.
    Later on we will show that, given an LPES lpes as specification, the token flow un-
folding of the synthesized net (as defined in the following subsection) preserves com-
mon prefixes and concurrency of runs of lpes.

2.4   Token Flow Unfolding of Petri Nets
In this section we recall one of the unfolding semantics of p/t-nets based on token
flows from [1]. Let lpes = (E, Con, ≺, l) be an LPES and N = (P, T, W, m0 ) be
a marked p/t-net. We want to interpret lpes as a model of the behavior of N , where
the events in E represent transition occurrences. A token flow function x :≺→ NP
is a function assigning multisets of places of N to the arcs of lpes. For an arc (e, e )
between transition occurrences e and e the multiset x(e, e ) is intended to represent the
token flow between these transition occurrences, that is to represent for each place the
number of tokens which are produced by e and then consumed by e .
    For a token flow function x, a consistency set C ∈ Conpre and an event e ∈ C we
denote




                                           62
                       
 – IN x (e) = e ≺e x(e , e) the x-intoken flow of e.
 – OU TC (e) = e≺e , e ∈C x(e, e ) the x-outtoken flow of e w.r.t. C.
         x


    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 analogous requirement for the
outtoken flow. It is assumed that there is a unique initial event producing the initial
marking.

Definition 4 (Prime token flow event structure). A prime token flow event structure
over T is a pair (lpes, x), where lpes = (E, Con, ≺, l) is an LPES with a unique
minimal event einit w.r.t. ≺ with l(einit ) = l(e) for all e = einit and l(E \{einit }) ⊆ T
and x :≺→ NP is a token flow function satisfying ∀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 by the same action name and depend on the same events with identical to-
ken flow. In [1] we showed that strong identical events that are in conflict always lead
to isomorphic processes, i.e. omitting strong identical events lead to a more compact
representation of behavior without loss of information.

Definition 5 (Strongly identical events). Let ((E, Con, ≺, l), x) be a prime token flow
event structure. Two events e, e ∈ E fulfilling (l(e) = l(e )) ∧ ( • e = • e ) ∧ (∀f ∈
•
  e : x(f, e) = x(f, e )) are called strongly identical.

    A token flow unfolding of a marked p/t-net is a prime token flow event 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 6 (Token flow unfolding). Let (N, m0 ), N = (P, T, F, W ), be a marked
p/t-net. A token flow unfolding of (N, m0 ) is a prime token flow event structure (lpes, x)
over T , lpes = (E, Con, ≺, l), satisfying:

 – (Uin ): ∀e = einit , ∀p ∈ P : IN x (e)(p) = W (p, l(e)).
 – (Uout ): ∀C ∈ Conpre , ∀e ∈ C \ {einit }, ∀p ∈ P : OU TCx (e)(p)  W (l(e), p).
 – (Uinit ): ∀C ∈ Conpre , ∀p ∈ P : OU TCx (einit )(p)  m0 (p).
 – (Umin ): ∀(e, e ) ∈≺s : (∃p ∈ P : x(e, e )(p)  1).
 – (Uid ): There are no strongly identical events e, e (w.r.t. x) satisfying {e, e } ∈ Con.

    As LPOs and LPES, token flow unfoldings are distinguished only up to isomorphism
([1]).

Example 1. Figure 1 shows a marked p/t-net (N, m0 ) (right side) together a finite token
flow unfolding (left side). As usual, places of a p/t-net are drawn as circles and transi-
tions as big squares with transition names shown inside. Markings are represented by




                                            63
                                                        
                                                             
                                                                      
                                                          
                     
                         
                  
                                                                       

                                                      
                                              

                             
                     
                                                    


              
                                                    



                      
                                        

Fig. 1. A marked p/t-net (right side) together with a finite prefix of its maximal token flow un-
folding (left side) and the canonical prefix of its maximal token flow unfolding w.r.t. ≈=≈mar
and  =⊂ (in the middle).


dots inside places. Arc weights are represenetd by numbers assigned to arcs, where the
arc weight 1 is not shown.
    Events of an LPES are drawn as small squares with event names shown inside and
event labels shown outside. Note that usually not all transitive arcs are shown, but only
those establishing the partial order.
    Different maximal consistency sets are distinguished by different colors. The token
flow unfolding of figure 1 has the two maximal consistency sets C = Cgrey = {0, 4}
(color grey) and C  = Cwhite = {0, 1, 2, 3, 5, 6} (color white).
    The token flow function is graphically represented by numbers in small circles of
different colors assigned to arcs. The colors belong to the places of the net. In figure 1
there is a white place and a grey place. Token flows of value 0 are not shown.
    It is easy to see, that in figure 1 (left side) the defining properties of token flow
unfoldings are satisfied, for example: If p = pgrey is the grey place then IN x (3)(p) =
1 = W ((p, b)), OU TCx  (3)(p) = 0 < 1 = W ((b, p)) and OU TCx (0)(p) = 1 = m0 (p).
    Note that the maximal unfolding (defined below) of (N, m0 ) is infinite and contains
the shown unfolding as a finite prefix.
    There exists a maximal (in general infinite) token flow unfolding Unfmax (N, m0 )
(w.r.t. given prefix relation), which is unique up to isomorphism. If (lpes, x) is the
maximal token flow unfolding of a Petri net, then L(lpes) is called Petri net unfolding
partial language. For each finite left-closed consistency set C of Unfmax , the LPO lpoC
is a run of N and for each run lpo of N there is a left-closed consistency set C of
Unfmax with lpo = lpoC .
    For each finite left-closed
                                consistency set C of Unfmax the multi-set of places
M ark(C) = m0 (·)+ e∈C (W (l(e), ·)−W (·, l(e)) is a reachable marking of (N, m0 ),
called the final marking of C. Every final marking in Unfmax is reachable in (N, m0 ),
and every reachable marking is a final marking in Unfmax .

2.5   Region based Synthesis
In this paper we follow the traditional region based synthesis approach (see for example
[9]), which we briefly describe now.




                                                             64
    Given a specification of the behavior of a system based on runs over a finite set
of action names, the action names are used as the transitions of the searched Petri net.
It remains to find a suitable finite set of places, each place with initial marking and
connections via arcs and arc-weights to all transitions. Places are found in a three-step-
approach.
    First the set of feasible places is defined. A place is feasible, if it does not prohibit
some of the specified behavior. The set of feasible places usually is infinite.
    Second so called regions of the behavioral specification are defined as non-negative
integral solutions of a linear homogenous equation system A · x = 0, such that each
region defines a feasible place and each feasible place is defined by a region.
    Adding all feasible places to the net leads to the so called saturated net, which has
the following properties:
 – Its behavior includes the specified behavior.
 – There is no net with less behavior having the first property.
    Third, for practical application, it remains to define a finite representation, i.e. a
finite set of regions such that the corresponding finite net has the same behavior as the
saturated net. One possibility of a finite representation, used in this paper, is to use
the fact that the set of solutions of a linear homogenous equation systems always has
a finite set of integral basis solutions [15]. There is a well-established mathematical
theory to compute these basis solutions. Since each solution can be represented as a
non-negative linear combination of the basis solutions, the finite set of basis solution is
a finite representation, calles basis representation.
    Summarized, in order to get a concrete synthesis algorithm for a behavioral specifi-
cation based on runs over action names, it is enough to
 – define feasible places.
 – define regions as solutions of a linear homogenous equation system, and
 – show that each regions defines a feasible place and each feasible place is defined
   by a region.

2.6   Complete Prefixes of Unfoldings
Since the maximal unfolding is infinite whenever the original net has infinite behavior,
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 [8] a parametric setup, called cutting context, is proposed in which completeness and
cutoff events can be discussed in a uniform, general and algorithm-independent way.
    In the following, we briefly recall the notions which are relevant in the context
of this paper. Let Unfmax 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 sets of Unfmax . A cutting context is a triple Θ = (≈, , {Ce }e∈E ), where:
 1. ≈ is an equivalence relation on Conpre , capturing the information which is in-
    tended 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 M ark(C) = M ark(C  ).




                                            65
 2.   is a so called adequate order on Conpre which refines ⊂. All -minimal left-
    closed consistency sets in each equivalence class of ≈ will be preserved in a com-
    plete prefix (see [10, 4] for concrete choices of ).
 3. ≈ and are preserved by finite extensions C ⊕ E of left-closed consistency sets C
    by suffixes E.
 4. {Ce }e∈E is a family of subsets of Conpre specifying the set of left-closed consis-
    tency 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 Unfmax .
     Roughly spoken, a prefix of Unfmax 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 prefix.
     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 Unfmax . In [1] it is shown that UnfΘ is uniquely determined by the
cutting context Θ, complete and finite if (N, m0 ) is bounded, {Ce }e∈E contains all
local left-closed consistency sets and ≈=≈mar .

Example 2. Figure 1 shows a marked p/t-net (right side) together with the canonical
prefix of its maximal token flow unfolding w.r.t. ≈=≈mar and =⊂ (in the middle).
The equivalence relation ≈ is shown below the canonical prefix. The set of cutoff events
is {2, 4}. The canonical prefix has the two maximal consistency sets C = Cgrey =
{0, 3} (color grey) and C  = Cwhite = {0, 1, 2, 4} (color white).


3     Synthesis of bounded p/t-nets
In this section we first define regions and feasible places and prove their one-to-one
correspondence for a finite LPES lpes and then extend this result by the handling of
repeated behavior.
    From subsection 2.5 we know that, in order to get a concrete synthesis algorithm, it
is enough to
    – define regions as solutions of a linear homogenous equation system,
    – define feasible places, and
    – show that each region defines a feasible place and each feasible place is defined by
      a region.
    We assume that a finite lpes has a unique minimal event einit with empty label.
    We define a token flow region of a finite lpes as a tuple r = (rk )k∈K of non-negative
integers with
                         K = (≺ ∪(       (Conepre × {e}))),
                                       e∈E




                                             66
    satisfying properties (Rinit ), (Rin ) and (Rout ) as defined below, where Conepre is the
    set of all maximal left-closed consistency sets of Con containing event e. As shown
    on the left side in figure 2, the values of a token flow region are graphically illustrated
    through numbers asigned to arcs.
        The intuition behind the choice of the range K is as follows: A region r defines a
    place pr . Each event may produce an amount of tokens in this place. Considering a con-
    crete run, there are the following two possibilities: A produced token is consumed from
    this place by a subsequent event of the run, or it is not further consumed by any subse-
    quent event. A token flow region represents the amounts of tokens for both possibilities
    as follows:
      – r(e,f ) represents the number of tokens produced by e in pr and subsequently con-
        sumed by f from pr in each run containing the edge (e, f ) ∈≺.
      – r(C,e) represents the number of tokens produced by e in pr and not consumed from
        pr by any subsequent event belonging to the run lpoC .
        For an event e and a consistency set C ∈ Conepre , we denote
      – IN r (e) = Σe ≺e r(e ,e) , the (r-)intoken flow of e.
      – OU TCr (e) = rC,e + Σe≺e ,e ∈C r(e,e ) , the (r-)outtoken flow of e w.r.t. C. The
        outtoken flow of einit we call initial token flow.
        Let Conmax
                pre denote the set of all maximal left-closed consistency sets.
        The defining properties of a token flow region r of lpes, giving a homogeneous
    linear inequation system with variables (rk )k∈K , are as follows:
(Rinit ) OU TCr (einit ) = OU TCr  (einit ) for C, C  ∈ Conmax
                                                             pre (different runs have the same
         initial token flow).
  (Rin ) IN r (e) = IN r (e ) for events e, e with l(e) = l(e ) (equally labelled events have
         the same intoken flow).
 (Rout ) OU TCr (e) = OU TCr  (e ) for events e, e with l(e) = l(e ), C ∈ Conepre and
                     
         C  ∈ Conepre (equally labelled events have the same outtoken flow).
        Then r defines a p/t-net-place pr in the following way:
      – m0 (pr ) := OU TCr (einit ) for some C ∈ Conmax
                                                      pre .
      – W (pr , t) := IN r (e) for some e ∈ E with l(e) = t.
      – W (t, pr ) := OU TCr (e) for some e ∈ E with l(e) = t and C ∈ Conepre .
    Observe that the properties (Rinit ), (Rin ) and (Rout ) ensure that the definition of pr is
    well-defined.

    Example 3. Figure 2 shows, among other things, an LPES lpes with assigned token
    flow region r (left side) and a marked p/t-net (N, m0 ) (right side). Maximal consis-
    tency sets are distinguished using the colors grey and white: There are the maximal
    consistency sets C = Cwhite = {0, 1, 2, 4} and C  = Cgrey = {0, 3}. The token
    flow region defines place p of (N, m0 ), where only non-zero token flows are shown.
    For example IN r (2) = IN r (4) = 1 = W ((p, b)), OU TCr (1) = 1 = W ((a, p)) and
    OU TCr (0) = OU TCr  (0) = 1 = m0 (p).




                                                67
    We call a place p with weight function Wp (p, ·)∪Wp (·, p) (with corresponding flow
relation Fp ) and initial marking mp (p) feasible w.r.t. a finite lpes, if p does not prohibit
any run of lpes, i.e. if there is a token flow function x on E such that (lpes, x) fulfills
properties (Uin ), (Uout ) and (Uinit ) from Definition 6 for (Np , mp ) = ({p}, T, Fp , Wp ,
mp ).3
    Given a finite lpes, there is a one-to-one correspondence between token flow rea-
gions of lpes and feasible places w.r.t. lpes.
Theorem 1. (1) If p is a feasible place w.r.t. lpes, then there is a token flow region r of
    lpes with p = pr .
(2) If r is a token flow region of lpes, then pr is a feasible place w.r.t. lpes.
Proof. (1): Let p be a feasible place w.r.t. lpes and (lpes, x) fulfill properties (Uin ),
(Uout ) and (Uinit ). We define a token flow region r of lpes as follows:
  (i) r(e,f ) := x(e, f ) for e ≺ f (the value is an integer since the net has exactly one
      place).                 
 (ii) rC,einit := mp (p) − e∈C r(einit ,e) for C ∈ Conmax  pre (the value is non-negative
      from the definition of  token flow unfoldings).
(iii) rC,e := W (l(e), p) − e<f,f ∈C r(e,f ) for e = einit and C ∈ Conepre (the value is
      non-negative from the definition of token flow unfoldings).
Then the defining properties of token flow regions can be seen for r as follows (where
C, C  are given as in the definition of token flow regions):
  – (Rinit ):                                                           
    OU TCr (einit ) = rC,einit + e∈C r(einit ,e) = mp (p) = rC  + e∈C  r(einit ,e) =
    OU TCr  (einit ) (the second and second to last equation follow from (ii)).
  – (Rin ):                                                       
    IN r (e) = f ≺e r(f,e) = W (p, l(e)) = W (p, l(e )) = f ≺e r(f,e ) = IN r (e )
    for l(e) = l(e ) (the second and second to last equation follow from (i) and the
    definition of token flow unfoldings).
  – (Rout ):                   
    OU TCr (e) = rC,e + e≺f,f ∈C r(e,f ) = W (l(e), p) = W (l(e ), p) = rC  ,e +
                                   r                     
       e ≺f,f ∈C  r(e ,f ) = OU TC  (e ) for l(e) = l(e ) (the second and second to last
    equation follow from (iii) and the definition of token flow unfoldings).
Moreover, we get by construction p = pr .
    (2): Let r be a token flow region of lpes and p = pr . We define a token flow function
x on lpes by x(e, f )(p) := r(e,f ) for e ≺ f . Then the defining properties of feasible
places (Uin ), (Uout ) and (Uinit ) from Definition 6 can be seen for x and (Np , mp ) as
follows: If e ∈ E, C ∈ Conpre and C ⊆ C max ∈ Conepre , then
                                        
  – IN x (e)(p) = f     ≺e x(f, e)(p) =   f ≺e r(f,e)
                                                            r
                                                  = IN (e) = W (p, l(e)).
  – OU TC (e)(p) = e≺f,f ∈C x(e, f )(p)  e≺f,f ∈C max x(e, f )(p)  rC max ,e +
           x
                                      r
        e≺f,f ∈C max r(e,f ) = OU TC max (e) = W (l(e), p) (the first inequality follows,
     since the numbers x(e, f )(p) are non-negative and C ⊆ C max ).
 3
     We will explain in the proof of Theorem 3 why feasible places do not necessarily fulfill prop-
     erties Uit and Umin .




                                                68
                                                         
 – OUTCx (einit )(p) =     einit ≺e∈C x(einit , e)(p)      einit ≺e∈C max x(einit , e)(p)
    einit ≺e,e∈C max r(einit ,e) + rC max ,einit = OU TCr max = mp (p) (the first in-
   equality follows, since all x(einit , e)(p) are non-negative and C ⊆ C max ).
In each case, the last equation follows from the definition of token flow regions.
    We now extend this approach by considering repeated behavior. To this end, we
consider a specification given by a finite LPES lpes and a list of cutoff-events w.r.t.
some cutting context Θ = (≈, , {Ce }e∈E ) with ≈=≈mar and =⊂.
    It is easy to see that ≈mar can be represented by a linear equation in terms of a
token flow region r = (rk )k∈K of lpes. If C ∈ Conpre , then the marking reached after
the execution of lpoC is given by the tokens produced by events in C, which are not
consumed by other events in C. In other words, roughly spoken, the marking is given
by the sum of token flows on edges leaving C. This can be formalized as in the case of
partial languages [9]: If C max ∈ Conmax
                                     pre is some maximal left-closed consistency set
with C ⊆ C max , then
                                                    
              M ark(C)(pr ) =      rC max ,e +                    r(e,f ) .
                                 e∈C             e∈C, f ∈C max \C , e≺f

Note that the result of the above sum is (by definition of token flow regions) independent
of the choice of C max .
    The basic idea for the representation of repeated behavior is to specify addition-
ally, that after some maximal events a repeated marking is reached, which was already
seen before. These maximal events are given by a subset Ecut = {e1 , . . . , en } of the
set of maximal events of E. For each event ei , the corresponding repeated marking
is specified by a left-closed consistency set Ci ∈ Cei with Ci ⊂ [ei ]. The aim is
to synthesize a net fulfilling M ark(Ci ) = M ark([ei ]). Altogether, the specification
consists of a finite LPES lpes = (E, Con, ≺, l) together with a so-called cutoff-list
Cut = (Ci , ei )ei ∈Ecut .
    This specification represents an infinite LPES lpesmax , called completion of (lpes,
Cut). The cutoff-list Cut specifies that exactly the extensions of Ci should also be
possible extensions of [ei ] in lpesmax .
Definition 7 (Completion). A completion of (lpes, Cut) is a minimal LPES lpesmax
containing lpes and satisfying:
    Let ≈ be the smallest equivalence relation on left-closed consistency sets of lpesmax
satisfying [ei ] ≈ Ci which is preserved by finite extensions. Then for C ≈ C  , C ⊂ C 
and each extension E = {e} of C in lpesmax there is an extension E  = {e } of C  in
lpesmax with l(e) = l(e ).
    Note that it is not defined, how extensions are appended to [ei ]. Thus, there are many
possible completions of (lpes, Cut), or, in other words, (lpes, Cut) represents a family
of inifinte completions. By definition, different completions have the same set of events
and only differ in the set of arcs used to append extensions.
    Note also, that not all maximal events of lpes need to be in Ecut . If e is maximal, but
not in Ecut , then the final marking of [e] is indended not to enable any further transition
occurrence.




                                            69
       It turns out, that a net (N, m0 ) synthesized from a specification (lpes, Cut) in gen-
   eral does not satisfy several plausible conjectures:
     – In general, lpes is not a complete prefix of the maximal unfolding of (N, m0 ), since
       it may be longer than the complete prefix.
     – In general, lpes is not a prefix of the maximal unfolding of (N, m0 ) at all, since it
       may contain strong identical events.
     – In general, lpesmax is not a prefix of the maximal unfolding of (N, m0 ), since it
       may contain strong identical events.
   Nevertheless, the maximal unfolding of the synthesized net (N, m0 ) has a very strong
   relation to a completion lpesmax of (lpes, Cut): it perserves common prefixes and con-
   currency of runs of lpesmax as given by definition 3. The formal problem statement,
   which we consider, is:

     – Given: A finite LPES lpes = (E, Con, ≺, l) over a finite alphabet of transition
       names T together with a cutoff-list Cut.
     – Searched: A marked p/t-net (N, m0 ) with set of transitions T such that there is a
       completion lpesmax of (lpes, Cut), satisfying:
         • the maximal token flow unfolding of (N, m0 ) preserves common prefixes and
           concurrency of runs of lpesmax ;
         • the partial language of this unfolding is the minimal partial language of an
           unfolding of a Petri net, which includes the partial language given by lpesmax .

   Definition 8 (Token Flow Region). A tuple r is a token flow region of (lpes, Cut) , if
   it satisfies the properties (Rinit ), (Rin ), (Rout ) and additionally
(Rcut ) M ark([ei ])(pr ) = M ark(Ci )(pr ) for all ei ∈ Ecut .
       A token flow region r defines a place pr in the same way as in the finite case.
   Example 4. Figure 2 shows an LPES and the cutoff-list Cut = {([1], 2), ([0], 4)} and
   with assigned token flow region r (left side) and a marked p/t-net (N, m0 ) (right side).
   The token flow region defines place p of (N, m0 ), where only non-zero token flows
   are shown. For example M ark([2])(p) = 1 = M ark([1])(p). Note that all places of
   (N, m0 ) are feasible (see following definitions).
       We call a place pr potentially feasible w.r.t. lpes and Cut, if adding this place to the
   net does not prohibit any run of some completion of lpes.
   Definition 9 (Potentially Feasible Place). Let lpes = (E, Con, ≺, l) and Cut be
   given as in the formal problem statement. A place p with weight function Wp (p, ·) ∪
   Wp (·, p) (with corresponding flow relation Fp ) and initial marking mp (p) is potentially
   feasible w.r.t. (lpes, Cut), if there is a completion lpesmax of (lpes, Cut) and a token
   flow function x such that (lpesmax , x) fulfills properties (Uin ), (Uout ) and (Uinit ) from
   Definition 6 for the marked p/t-net (Np , mp ) = ({p}, T, Fp , Wp , mp ).
       We are interested in bounded nets, so we will consider only such potentially feasible
   places to be truly feasible, which, together with other potentially feasible places, form
   a bounded net.




                                               70
                                                    
                                                      
                                                                 
                                                         
                                      
                                            
                
                                                                  

                                                               
                                            
                          
 
                                         


                                                


                
                                                



                      
                              

Fig. 2. Left: Graphical illustration of a token flow region for a maximal left-closed consistency
set C. Middle: An LPES wit a cutoff-list and assigned token flow region. Right: A marked p/t-net
with several feasible places. The place p corresponds to the token flow region.


Definition 10 (Feasible Place). Let p is a potentially feasible place; then p is feasible
iff there is a set of potentially feasible places P such that p ∈ P and the marked p/t-net
(NP , mP ) = (P, T, ∪p∈P Fp , ∪p∈P Wp , ∪p∈P mp ) is bounded.
Theorem 2. (1) If p is a feasible place w.r.t. (lpes, Cut), then there is a token flow
    region r of (lpes, Cut) with p = pr .
(2) If r is a token flow region of (lpes, Cut), then pr is a feasible place of (lpes, Cut).
Proof. (1): Let p be a feasible place w.r.t. (lpes, Cut), lpesmax be a completion of
(lpes, Cut) and (lpesmax , x) fulfill properties (Uin ), (Uout ) and (Uinit ). Since lpes is a
part of lpesmax , we deduce from Theorem 1 that there is a token flow region r of lpes
with p = pr . In particular, r satisfies the defining properties (Rinit ), (Rin ) and (Rout ).
    Property (Rcut ) follows from the fact that lpesmax contains the parts [ei ] \ Ci in-
finitely often. Namely, by definition of lpesmax the non-empty part [ei ] \ Ci is an exten-
sion of Ci which occurs iteratively in lpesmax after [ei ]. The existence of a token flow
function of lpesmax shows that after the occurrence of lpoCi , the part [ei ]\Ci can occur
arbitrarily often in an iterated way in (Np , mp ). This means the occurrence of [ei ] \ Ci
does not decrease the number of tokens in p. Suppose that the occurrence of [ei ] \ Ci
increases the number of tokens in the place. This would imply that p is unbounded.
Because each potentially feasible place will preserve that [ei ] \ Ci can occur arbitrarily
often, p will remain unbounded for any set of potentially feasible places which includes
p. This contradicts with the fact that p is feasible. Thus, the occurrence of [ei ] \ Ci does
not change the number of tokens in p.
    (2): Let r be a token flow region of (lpes, Cut) and p = pr . We deduce from
Theorem 1 that there is a token flow function x on lpes, such that (lpes, x) fulfills
properties (Uin ), (Uout ) and (Uinit ).
    From property (Rcut ) we deduce that there is a completion lpesmax of lpes such
that x can be extended to a token flow function on lpesmax and (lpesmax , x) fulfills
properties (Uin ), (Uout ) and (Uinit ). Namely, it can be seen by an easy inductive proof
that for arbitrary C ≈ C  , C ⊂ C  we have M ark(C) = M ark(C  ) (for C = Ci
and C  = [ei ] this corrsponds to (Rcut )). This means that after the occurrence of C  ,




                                                    71
there are enough tokens in p for the occurrence of each transition, which can occur
after the occurrence of C, i.e. (lpes, x) can be extended as required by the definition of
completions, and therefore p = pr is potentially feasible.
    Let max be the maximum of the set {M ark(C) | C ∈ Conpre }. Let p be a
complement place w.r.t. place p (i.e. W (p, t) = W (t, p ) and W (t, p) = W (p , t)
for each t ∈ T ) with initial marking mp = max − mp . One may observe that p is
potentially feasible and the net ({p, p }, T, Fp ∪ Fp , Wp ∪ Wp , mp ∪ mp ) is bounded,
and therefore p is feasible.
Theorem 3. Let lpes = (E, Con, ≺, l) be a finite LPES together with a cutoff list
Cut and let (N, m0 ) be the finite p/t-net derived from the basis representation of
the set of all token flow regions of lpes. Let Unfmax (N, m0 ) =: (lpes , x ), lpes =
(E  , Con , ≺ , l ), be the maximal token flow unfolding of (N, m0 ). Then there is a
completion lpesmax of (lpes, Cut) satisfying:
(1) lpes preserves common prefixes and concurrency of runs of lpesmax .
(2) The partial language of lpes is a minimal Petri net unfolding partial language,
    which includes the partial language of lpesmax .
Proof. Throughout the proof, we use the following notions:
  – Let {r1 , . . . , rn } be the set of basis regions of the set of all token flow regions of
    (lpes, Cut) and pi = pri the corresponding places for i = 1, . . . , n.
  – Let (N, m0 ), N = (P, T, F, W ), P = {p1 , . . . , pn , be the finite p/t-net derived
    from the basis representation of the set of all token flow regions of lpes.
  – Let (Ni , mi ), N = ({pi }, Ti , Fi , Wi ), be the the net derived from (N, m0 ) by
    restricting P to the place pi .
    The outline of the proof is the following:
(A) First we construct a completion lpesmax = (E max , Conmax , ≺max , lmax ) of (lpes,
    Cut) and a token flow function x on lpesmax , such that (lpesmax , x) is a prime
    token flow event structure and satisfies properties (Uin ), (Uout ) and (Uinit ) from
    Definition 6 w.r.t. the net (N, m0 ).
(B) Second we construct a function b : E max → E  such that for each left-closed
    consistency set C of lpesmax there holds that b(C) is a left-closed consistency set
    of lpes and b|C defines an isomorphism between lpoC and a sequentialization of
    lpob(C) . This gives property (1).
(C) Third we show that the partial language of lpes is a minimal Petri net unfolding
    partial language, which includes the partial language of lpesmax . This gives prop-
    erty (2).
    ad (A): For each computed basis region ri the corresponding place pi is feasible
w.r.t. (lpes, Cut) by Theorem 2. That means, in particular, that for each i there is a
completion lpesmax
                 i     = (Ei , Coni , ≺i , li ) of (lpes, Cut) and a token flow function xi
on lpesmax
         i    such that (lpesmax
                             i   , xi ) is a prime token flow event structure and satisfies
properties (Uin ), (Uout ) and (Uinit ) w.r.t. the net (Ni , mi ). All these completions have
the same set of events, the same set of consistency sets and the same labelling and
can be combined into one completion lpesmax = (E max , Conmax , ≺max , lmax ) in the
following way:




                                            72
 – E max = Ei for some i,
 – Conmax   = Coni for some i,
              n
 – ≺max = i=1 ≺i ,
     max
 – l     = li for some i.

Moreover, if we extend each xi to the set ≺max by xi (e, e ) = 0 for (e, e ) ∈≺max
\ ≺i , we can combine the token flow functions xi into a token flow function x on
≺max by
                                          n
                                   x = Σi=1 xi .
By construction, the properties of the completions (lpesmax
                                                        i   , xi ) carry over to
(lpesmax , x):

 – (lpesmax , x) ist a prime token flow event structure: We have to show that IN x (e) =
   IN x (e ) for lmax (e) = lmax (e ). This follows by construction from IN xi (e) =
   IN xi (e ).
 – (lpesmax , x) satisfies property (Uin ) w.r.t. the net (N, m0 ): We have to show that
   IN x (e)(pi ) = W (pi , l(e)) for each i. This follows by constructiuon from
   IN x (e)(pi ) = IN xi (e)(pi ) and IN xi (e)(pi ) = W (pi , l(e)).
 – (lpesmax , x) satisfies property (Uout ) w.r.t. the net (N, m0 ): Follows analoguously
   to (Uin ).
 – (lpesmax , x) satisfies property (Uinit ) w.r.t. the net (N, m0 ): Follows analoguously
   to (Uin ).

    ad (B): We first show the desired property for the finite LPES lpes and then extend
the result to infinite LPES lpesmax .
    Note that the properties (Uin ), (Uout ) and (Uinit ) correspond to feasability of places
w.r.t. the finite partial language corresponding to lpes as defined in [9]. That means,
lpoC is a run of (N, m0 ) for each left-closed consistency set C of lpes. Moreover,
there is a corresponding process of (N, m0 ) such that lpoC is a sequentialization of this
process and x(e, e ) corresponds to the set of conditions connecting the events e and e
of the process for each edge (e, e ). Note that lpoC is a proper sequentialization of the
corresponding process if and only if x(e, e ) = 0 for some edge (e, e ). In this case,
(lpesmax , x) does not satisfy (Umin ) and the synthesis problem does not have an exact
solution - this is one of two cases where (lpesmax , x) is not a token flow unfolding.
    We fix a total order on the set E of events of lpes respecting ≺ and try to build a
finite prefix of lpes by appending the events in this order starting with einit . In fact,
since on each run x is a token flow corresponding to some process (as seen above), it is
always possible to append the next event e except in one case: If there is an event eid
already appended which is strong identical to e w.r.t x, then e is not appended according
to the appending proceedure defined in [1], since it leads to isomorphic runs. In this case
(lpesmax , x) does not satisfy (Uid ) - and this is the second case where (lpesmax , x) is
not a token flow unfolding.
    We define b : E → E  inductively in the order of appending events as follows:

 – (Induction basis) Let einit be the initial event of lpes and einit be the initial event
   of lpes . Then b(einit ) = einit .




                                            73
 – (Induction step) Let e be the next event of lpes in the appending procedure. Then
   we try to append the following event e to the actual prefix of lpes :
     • l (e ) = l(e),
     • • e = b({f ∈ • e | x(f, e) = 0}),
     • x (b(f ), e ) = x(f, e).
   If it is possible to append e , then conistency sets are updated w.r.t. e (see below)
   and we define b(e) = e . If it is not possible to append e since there is a strong
   identical event eid of the actual prefix of lpes , then then conistency sets are updated
   w.r.t. eid (see below) we define b(e) = eid .
 – (Updating consistency sets) Let e be the next event of lpes in the appending pro-
   cedure and let C be a left-closed consistency set which is a subset of the events
   appended so far, such that C ∪ {e} is also a left-closed consistency set. We claim
   that b(C) ∪ {b(e)} is a left-closed consistency set and b|C∪{e} defines an isomor-
   phism between lpoC∪{e} and a sequentialization of lpob(C)∪{b(e)} . This can be seen
   inductively as follows:
     • (Induction hypothesis for C) b(C) is a left-closed consistency set of lpes and
         b|C defines an isomorphism between lpoC and a sequentialization of lpob(C) .
         By construction, x(e, e ) = x (b(e), b(e )) for each edge (e, e ) with x(e, e ) =
         0, i.e. both runs have the same corresponding process.
     • (b(C) ∪ {b(e)} is left closed) Since C ∪ {e} is left-closed, we deduce • e ⊂ C.
         By construction, this implies • b(e) ⊂ b(C), i.e. b(C) ∪ {b(e)} is left-closed.
     • (Induction step for C ∪ {e}) Since C ∪ {e} is a consistency set, lpoC is a run
         which enables e, and lpoC∪{e} is also a run. By induction hypothesis, lpoC
         is (isomorphic to) a sequentialization of lpob(C) . Moreover, lpoC and lpob(C)
         correspond to the same process. Therefore, lpob(C) enables b(e). By construc-
         tion, b(e) is appended to b(C) using the same token flow as for the connection
         between e and C. This gives the induction hypothesis also for C ∪ {e}.
In particular, two runs of (lpes, x) which are isomorphic due to strong identical events
are mapped onto the same run of (lpes , x ).
    Finally, observe that the above argumentation for lpes holds for each finite prefix of
lpesmax . Since the construction of the maximal unfolding is independend of the order
in which events are appended [1], this gives the desired result for lpesmax .
    ad (C): This classical result of region based synthesis follows by construction from
Theorem 2, the considerations in subsection 2.5 and the fact, that the basis representa-
tion of the set of all token flow regions of (lpes, Cut) is used.
    For a specification which is itself a complete prefix of a maximal token flow unfold-
ing of a p/t-net we get:
Corollary 1. Let lpes be the LPES underlying the complete finite prefix of the maximal
token flow unfolding of a bounded net (N, m0 ) w.r.t. ≈=≈mar and =⊂. Moreover, let
Ecut = {e1 , . . . , en } be the set of static cutoff events of lpes and Ci be left-closed con-
sistency sets with Ci ∈ Cei , Ci ≈ [ei ] and Ci ⊂ [ei ], and let Cut = (Ci , ei )ei ∈Ecut .
            
Let (N  , m0 ) be the finite p/t-net derived from the basis representation of the set of
                                                                  
all token flow regions of (lpes, Cut). Let Unfmax (N  , m0 ) = (lpes , x ) be the maxi-
                                         
mal token flow unfolding of (N  , m0 ). Then lpes and a completion of lpes have equal
partial languages.




                                             74
    Note that we used the choice =⊂ only in order to simplify the presentation.
The results can be generalized to each choice of and each choice of ≈ allowing its
representation by a linear inequation in terms of token flows.


4   Related works

In [16] a one-to-one correspondence between finite 1-safe Petri nets and infinite regular
trace event structures is established. On the one side in [16] more restrictive models
as in this paper are considered (binary conflict relation, static concurrency relation).
On the other side, the problem solved in [16] is stronger than the synthesis problem
considered in this paper, since we neither give a characterization of LPES representing
p/t-net behavior, nor answer the question, whether a given LPES corresponds to a p/t-
net unfolding. Altogether, in [16] and in our paper different problems are considered
which cannot be compared directly. There are several other works, which uses a Petri
net as a final result and uses event structures as an intermediate representation [13, 14].
These works use folding methods and do consider a more restrictive setting (binary
conflict relation, nets without arc weights).


                               
                                   

                              
            


                                           
                                                          
          
                              
             

                                                                
                                           
                                               


                                  



                          
                             

                                  




Fig. 3. Net with behavior which cannot be expressed by finite representations of infinite partial
languages using terms from [9]


     Up to now, several finite representations of infinite partial languages equipped with a
corresponding notion of regions were developed. The most general one was given in [9]
using terms with operations for the union, the parallel composition and the sequential
composition of runs and partial languages. For each of these representations there are
still examples of inifinite Petri net languages which cannot be represented, whereas we
show in this paper, that each Petri net language can be specidied by means of a finite
LPES together with a cut-off list.
     Figure 3 shows on the left side an LPES with one maximal left-closed consis-
tency set, together with a cutoff-list {e3 , e7 } and corresponding consistency sets Ce3 =
[e1 ] and Ce7 = [e5 ]. It represents exactly the behavior of the Petri net on the right
side and has assigned the token flow region r corresponding to place p. For example




                                                       75
IN r (e3 ) = IN r (e1 ) = 1 = W (p, a), OU T r (e5 ) = OU T r (e7 ) = 1 = W (b, p),
M ark([e3 ])(p) = 0 = M ark([e1 ])(p) and M ark([e7 ])(p) = 1 = M ark([e5 ])(p).
Note that it is not possible to represent the behavior of the shown net by other finite
representations of infinite partial languages as for example terms [9].


5   Conclusion and future research

The main contribution of the paper is that it enables to handle arbitrary cyclic behaviour
of bounded p/t nets. Moreover, it gives a basic result for both history (conflict) and con-
currency preserving synthesis of Petri nets from a true concurrent and branching time
behaviour specification - labelled prime event structures. The topic of branching time
history preserving or conflict preserving synthesis remain full of non-trivial unsolved
problems. One may for example ask for synthesis which preserves the absence of com-
mon prefixes. In general, analogously to a spectrum of behavioural equivalences [17]
(and simulations), one can define a similar spectrum of history preserving synthesis
methods w.r.t. given behavioural equivalences.



                                   
                                           
                                                

                                                   
                                 
                       

                                                             
                                                               

                                                    



                                         



                                         



                             
                           

Fig. 4. Net with behavior which cannot be overapproximated by a bounded net with nonempty
set of places [9].



    With one modification, our mechanism may also serve for the synthesis of un-
bounded nets. As for bounded case, we represent an infinite partial language by an
LPES lpes together with a cutoff-list {(e1 , C1 ), . . . , (en , Cn )}. In contrast to the case
of bounded nets, we do not require, that the consistency sets Ci represent repeated
markings, but increased markings, i.e. M ark([ei ]) ≥ M ark(Ci ). Figure 4 shows
on the right side an unbounded net whose behavior can be represented by the LPES
shown on the left side together with the cutoff-list {(e2 , [e1 ]), (e3 , [e1 ])}. The LPES
has assigned the token flow region r corresponding to place p of the net, for example:
IN r (e1 ) = IN r (e2 ) = 1 = W (p, a), OU T r (e1 ) = OU T r (e3 ) = 2 = W (a, p) and
M ark([e3 ])(p) = M ark([e2 ])(p) = 3 ≥ 2 = M ark([e1 ])(p).
    Note that the specification on the left side does not have a nonempty bounded so-
lution, that means in general there are specifications such that there is no bounded net
with nonempty set of places whose behavior overapproximates them.




                                                     76
References
 1. R. Bergenthum, S. Mauser, R. Lorenz, and G. Juhás. Unfolding semantics of petri nets based
    on token flows. Fundam. Inform., 94(3-4):331–360, 2009.
 2. M. Dumas and L. Garcı́a-Bañuelos. Process mining reloaded: Event structures as a unified
    representation of process models and event logs. In R. Devillers and A. Valmari, editors,
    Application and Theory of Petri Nets and Concurrency, volume 9115 of Lecture Notes in
    Computer Science, pages 33–48. Springer International Publishing, 2015.
 3. J. Engelfriet. Branching processes of petri nets. Acta Informatica, 28(6):575–591, 1991.
 4. J. Esparza, S. Römer, and W. Vogler. An improvement of mcmillan’s unfolding algorithm.
    Formal Methods in System Design, 20(3):285–310, 2002.
 5. G. Juhás, R. Lorenz, and J. Desel. Can i execute my scenario in your net?. In G. Ciardo and
    P. Darondeau, editors, ICATPN, volume 3536 of Lecture Notes in Computer Science, pages
    289–308. Springer, 2005.
 6. V. Khomenko and M. Koutny. Towards an efficient algorithm for unfolding petri nets. In
    K. G. Larsen and M. Nielsen, editors, CONCUR, volume 2154 of Lecture Notes in Computer
    Science, pages 366–380. Springer, 2001.
 7. V. Khomenko and M. Koutny. Branching processes of high-level petri nets. In H. Garavel
    and J. Hatcliff, editors, TACAS, volume 2619 of Lecture Notes in Computer Science, pages
    458–472. Springer, 2003.
 8. V. Khomenko, M. Koutny, and W. Vogler. Canonical prefixes of petri net unfoldings. Acta
    Inf., 40(2):95–118, 2003.
 9. R. Lorenz, J. Desel, and G. Juhás. Models from scenarios. In Transactions on Petri Nets and
    Other Models of Concurrency VII, pages 314–371. Springer Berlin Heidelberg, 2013.
10. K. L. McMillan. Using unfoldings to avoid the state explosion problem in the verification
    of asynchronous circuits. In G. von Bochmann; D. K. Probst, editor, CAV, volume 663 of
    Lecture Notes in Computer Science, pages 164–177. Springer, 1992.
11. J. Meseguer, U. Montanari, and V. Sassone. On the model of computation of place/transition
    petri nets. In R. Valette, editor, Application and Theory of Petri Nets, volume 815 of Lecture
    Notes in Computer Science, pages 16–38. Springer, 1994.
12. M. Nielsen, G. Plotkin, and G. Winskel. Petri nets, event structures and domains, part i.
    Theoretical Computer Science, 13:85–108, 1981.
13. A. Polyvyanyy, L. Garcı́a-Bañuelos, D. Fahland, and M. Weske. Maximal structuring of
    acyclic process models. The Computer Journal, 2012.
14. H. Ponce de León, C. Rodrı́guez, J. Carmona, K. Heljanko, and S. Haar. Unfolding-based
    process discovery. CoRR, abs/1507.02744, 2015.
15. A. Schrijver. Theory of Linear and Integer Programming. Wiley, 1986.
16. P. S. Thiagarajan. Regular event structures and finite petri nets: A conjecture. In Formal
    and Natural Computing - Essays Dedicated to Grzegorz Rozenberg, volume 2300 of Lecture
    Notes in Computer Science, pages 244–256. Springer, 2002.
17. G. U. van Glabbeek, R. Refinement of actions and equivalence notions for concurrent sys-
    tems. Acta Informatica, 37(4-5):229–327, 2001.
18. G. Winskel. Event structures. In W. Brauer, W. Reisig, and G. Rozenberg, editors, Advances
    in Petri Nets, volume 255 of Lecture Notes in Computer Science, pages 325–392. Springer,
    1986.




                                               77

</pre>