Each Event-driven Process Chain (EPC) translates into a free-choice system if its control flow branches and joins only at AND- or XOR-connectors. This free-choice system defines the free-choice semantics of the AND/XOR-EPC. But free-choice systems are not capable to deal with OR-connectors. Therefore a general EPC with OR-connectors obtains a semantics not until it has been translated into a certain coloured Petri net, named a Boolean system. This Boolean system defines the Boolean semantics of the EPC. We show that for well-behaved AND/XOR-EPCs the Boolean semantics reduces to the free choice semantics in as far as the Boolean system contains the free-choice system. To prove this result we introduce the concept of non-blocking components in live and safe free-choice systems. For each nonblocking component of the free-choice system we then construct a well-behaved bipolar system (bp-system), which is a particular Boolean system. We link the bpsystems of all non-blocking components of a covering to a coloured Petri which is named a linked bp-system. Its semantics is the Boolean semantics of the AND/XOREPC.
Free-choice systems form an important class of ordinary Petri nets. They are best analyzed and understood, and the theory of free-choice systems is both deep and elegant [DE1995]. Also for commercial applications of information management freechoice systems play an important role. In the context of Business Process Management (BPM) they serve to formalize process languages which have been introduced in a more informal way and lacked a well-defined semantics before. The process modelling language most widespread in German commercial projects is the language of Event-driven Process Chains (EPC). It has been introduced by Keller, Nüttgens and Scheer in 1992 [KNS1992, Sch1994]. EPCs represent the control flow of a process as the interplay of three components: Events, functions and logical rules. The rules use connectors of logical type AND, XOR and OR. More specific, concurrency is represented by AND-splits and AND-joins. Strong or exclusive alternatives are modelled by XOR-splits and XOR-joins, while OR-splits and ORjoins model weak alternatives. All EPCs in this paper will be considered with a nonempty set of distinguished events, the initial events of the process.
The present paper deals mainly with AND/XOR-EPCs, i.e. with the restricted class of EPCs using only connectors of logical type AND or XOR. Each AND/XOR-EPC translates at once into a free-choice system FS : Functions and AND-connectors of the EPC translate into transitions while events and XOR-connectors translate into places of FS . Each initial event of the EPC is marked by a token on the corresponding place of FS . The free-choice semantics of the AND/XOR-EPC is defined as the semantics of FS [Aal1999].
But the language of free-choice system is not capable to formalize EPCs with ORconnectors. Therefore we have introduced in a previous paper Boolean systems, a class of simple coloured Petri nets [LSW1998]. Boolean systems have two types of tokens, high tokens and low tokens. The low tokens serve to skip actions and to complete the marking of all pre-sets of a logical transition before a decision about its actual firing mode is possible. With the help of formulas from propositional logic the transitions of Boolean systems control the flow of the high tokens (true) and the low tokens (false).
A general EPC translates at once into a Boolean system BS : Functions and logical connectors of the EPC translate into transitions and events translate into places of BS . Each initial event of the EPC is marked by a high token at the corresponding place of BS and if necessary a suitable set of low tokens is added.
Those Boolean systems, which are needed for the restricted class of AND/XOREPCs, have been invented already in 1984 by Genrich and Thiagarajan [GT1984]. They named them Bipolar Synchronization Schemes, today abbreviated as bipolar systems (bp-system).
How do these two types of Petri nets, bipolar systems and free-choice systems, relate? It turns out that each bp-system BS has a free-choice companion FS and a canonical morphism high : BS → FS which maps the flow of high tokens of the coloured Petri net BS onto the flow of tokens of the free-choice system FS . Both systems are equivalent in as far as FS is well-behaved if and only if BS is well-behaved. In that case the morphism has the lifting property, i.e., it lifts occurrence sequences of FS to occurrence sequences of BS [Weh2010].
Yet, this equivalence holds only under the restriction that the behaviour of the freechoice system is fair. Here fairness is conceived as the absence of frozen tokens. That type of fairness is even a structural property, named non-blocking.
Therefore the present paper investigates a generalization of the above mentioned relation between the two classes of Petri nets. Relinquishing the non-blocking condition we prove: For each well-behaved free-choice system FS system LBS and a morphism a
well-behaved linked bphigh : LBS → FS exist, which maps the flow of high tokens of the coloured Petri net LBS onto the token flow of the free-choice system FS and satisfies the lifting property (Theor. 17 and Prop. 19).
As a consequence: For an AND/XOR-EPC, which translates into a well-behaved freechoice system FS , a well-behaved linked bp-system LBS exists with high(LBS ) = FS . We define the Boolean semantics of the EPC as the semantics of the coloured Petri net LBS . As a consequence, the free-choice semantics and the Boolean semantics of well-behaved AND/XOR-EPCs are equivalent. And this results allows us to consider the Boolean semantics of general EPCs a proper generalization of the free-choice semantics of AND/XOR-EPCs.
During our way in this paper we introduce two new concepts for Petri nets: Firstly non-blocking components of well-behaved free-choice systems and secondly the linking of bp-systems with respect to a family of morphisms. 2.
For the convenience of the reader and to fix the notations we recall some fundamental concepts from the theory of ordinary Petri nets and define the subclass of free-choice systems.
A finite ordinary Petri net is a pair (N , μ ) : The net N = (P, T , F ) comprises a finite set P of places, a disjoint finite set T of transitions and a set F ⊆ (P × T ) ∪ (T × P) of directed arcs. The function μ : P → N is named the initial marking of the net.
supp(μ ) := { p ∈ P : μ ( p) > 0 } of all places marked at μ . All Petri nets in this paper will be assumed finite. A path from a node xini ∈ X := P ∪ T to a node x fin ∈ X is a sequence (x0 , x1,..., xn ) with nodes xi ∈ X , x0 = xini , xn = x fin and (xi , xi+1)∈ F . It is named elementary path, if xi ≠ x j for all pairs i ≠ j . The net N is strongly connected if for every two nodes x1, x2 ∈ X a path from x1 to x2 and a path from x2 to x1 exists. A transition with a single pre-place and two or more post-places is an opening transition, a transition with a single post-place and two or more pre-places is called a closing transition. Opening transitions with exactly two post-places and closing transitions with exactly two pre-places are called binary transitions. A net N is called binary if all its transitions are binary.
For a net N the firing rule defines the firing of a transition: A transition t ∈ T is enabled at a marking μ of N iff each place from its pre-set pre(t ) is marked at μ with at least one token. Being enabled, t may occur or fire. Firing t yields a new marking μ ' , which results from μ by consuming one token from each pre-place of t and by producing one additional token on each post-place of t ; this is denoted by μ t→μ ' .
A finite occurrence sequence from μ is a sequence σ = t1...tk , k ∈ N , such that μ t1 →μ1, ..., μ k −1 tk →μ k .
We denote by μ σ→μ k the fact, that firing σ yields the marking μ k . A reachable marking of a Petri net (N , μ ) is a marking, which results from firing a finite occurrence sequence from μ . If not stated the contrary, occurrence sequences in this paper will be considered finite occurrence sequences. The concatenation of two occurrence sequences σ 1 and σ 2 is denoted by σ 1 ⋅σ 2 .
A Petri net (N , μ 0 ) is live iff for each reachable marking μ and for each transition t ∈ T the Petri net (N , μ ) has a reachable marking which enables t . A Petri net is k -bounded iff a number k ∈ N exists bounding from above the token content of every place at every reachable marking. If the bound can be chosen as k = 1 then the Petri net is named safe. A live and safe Petri net is named wellbehaved. A net N is well-formed iff there exists a marking μ 0 of N such that the Petri net (N , μ 0 ) is live and bounded.
We will often dispense with an explicit notation for the set of places and transitions of a net and use the shorthand x ∈ N to denote a node of the net. 1.
Definition (P-system, T-system, free-choice system) i) A net N is a P-net if all transitions have exactly one pre-place and exactly one post-place, i.e.
card [pre(t )] = 1 = card [post(t )] for all transitions t ∈ N .
A P-system is a Petri net (N , μ ) with N a P-net. ii) A net N is a T-net if all places have exactly one pre-transition and exactly one post-transition, i.e.
card [pre( p)] = 1 = card[post( p)] for all places p ∈ N .
A T-system is a Petri net (N , μ ) with N a T-net. iii) A net N is a free-choice net if for every two transitions t1, t2 ∈ N either pre(t1 ) I pre(t2 ) = ∅ or pre(t1 ) = pre(t2 ) .
A restricted free-choice net is a net which satisfies the stronger condition: For every two transitions t1, t2 ∈ T
either pre(t1 ) I pre(t2 ) = ∅ or pre(t1 ) = pre(t2 ) = { p } with a single place p ∈ P . A marked (restricted) free-choice net (N , μ ) is named (restricted) free-choice system.
Well-behaved free-choice systems are one of the two classes of Petri nets studied in the present paper. By a theorem of Genrich each well-formed free-choice net FN has a marking μ , such that (FN , μ ) is even well-behaved ([De1995] Theor. 5.10). An important means for the examination of free-choice systems is the study of their P-components and T-components. 2. Definition (Components and their intersection) Consider a net N = (P, T , F ) . i) A subnet N P ⊆ N which is generated by a nonempty subset X ⊆ P ∪ T of nodes, is a P-component of N if N P is a strongly connected P-net with
pre( p) ∪ post( p) ⊆ X for all places p ∈ X .
Consider a marking μ of N . If a P-component N P ⊆ N is marked at μ with a single token then (N P ,μ P ) , μ P := μ | N P , is named a basic component of (N ,μ ) . ii) A subnet NT of N which is generated by a nonempty subset X ⊆ P ∪ T of nodes, is a T-component of N if NT is a strongly connected T-net with pre(t ) ∪ post(t ) ⊆ X for all transitions t ∈ X . iii) The net N is structurally non-blocking iff every P-component N P of N intersects every T-component NT of N in a non-empty set N P ∩ NT ≠ ∅ . Otherwise the net is named structurally blocking. A Petri net (N ,μ ) is non-blocking if its underlying net N is structurally non-blocking. Otherwise the Petri net is named blocking. 3.
Example (Well-behaved, but blocking free-choice system) 1 token e_1 t_9 e_9 e_12 t_1 e_2 t_2 t_8
e_10 1 token
e_8 1 token e_7 1 token e_3 t_3 e_4 t_5 t_7 t_4 e_11 e_5 t_6 e_6 generated by the set { e3, t3, e4 , t4 } are disjoint. generated by the set { e3, t3, e4 , t4 } are disjoint.
To prepare the introduction of the new concept of non-blocking components we recall some properties of well-behaved free-choice systems.
Each well-behaved free-choice system can be covered by basic components. Each occurrence sequence which fires only transitions from one of these basic components lifts to an occurrence sequence of the whole free-choice system. This has been observed by Thiagarajan and Voss first. After introducing the concept of a morphism of Petri nets we will formulate their result as the lifting property of a certain morphism.
Figure 1 shows a well-behaved restricted free-choice system FS . It is blocking: E.g., the P-component N P generated by the set { e7 , t7 , e8, t8 } and the T-component NT To prepare the introduction of the new concept of non-blocking components we recall some properties of well-behaved free-choice systems.
Each well-behaved free-choice system can be covered by basic components. Each occurrence sequence which fires only transitions from one of these basic components lifts to an occurrence sequence of the whole free-choice system. This has been observed by Thiagarajan and Voss first. After introducing the concept of a morphism of Petri nets we will formulate their result as the lifting property of a certain morphism. 4.
Remark (Morphisms of Petri nets) Within the category of coloured Petri nets the concept of a morphism f : PN1 → PN2 between two coloured Petri nets is well-defined, cf. [Weh2006]. Our concept of a morphism presupposes coloured nets for the domain and range of the morphism, because a morphism maps respectively, certain T-flows and P-flows of PN1 to binding elements and token elements of PN2 .
The reader, who is not interested in the general definition of a morphism, may use his own descriptive concept of a morphism PN1 f → PN2 to follow the examples of this paper. In most cases the domain of definition PN1 will be an ordinary Petri net and the coloured Petri net PN2 will be equivalent to an ordinary Petri net, too. In addition, all morphisms under consideration will be discrete, i.e. for any node y ∈ PN2 the fibre f −1(y) ⊂ PN1 has only isolated nodes.
Any discrete Petri net morphism PN1 f → PN2 maps occurrence sequences of PN1 to occurrence sequences of PN2 . The question about the surjectivity of this map is named the lifting problem. 5. Definition (Lifting property of a morphism) A Petri net morphism
PN1 f → PN2 has the lifting property iff for any enabled occurrence sequence σ 2 of PN2 an enabled occurrence sequence σ 1 of PN1 exists with f (σ 1 ) = σ 2 . The occurrence sequence σ 1 is named a lift of σ 2 against f .
Any enabled occurrence sequence of a basic component of a well-behaved free-choice system lifts to an enabled occurrence sequence of the whole system. 6. Proposition (Lifting property for basic components) Consider a well-behaved free-choice system FS = (N , μ ) and a basic component N B of FS . Then the projection
π B : FS →(N B , μ |N B ) has the lifting property.
Proof. [TV1984], Theor. 2.1 proves the claim under the additional assumption that the free-choice system FN is restricted. But any cluster from a free-choice net can be substituted by two clusters of a restricted free-choice net. Therefore it suffices to prove the claim for restricted free-choice systems, q. e. d. 7.
Corollary (Union of basic components) Consider a well-behaved free-choice system FS = (N , μ ) and a subnet N1 ⊂ N which is the union of basic components of FS . Then the projection
π 1 : FS → FS1 onto the restriction FS1 := (N1,μ | N1 ) has the lifting property and FS1 is wellbehaved.
Proof. Any union of P-components of a free-choice net is free-choice itself. Pcomponents are transition bounded. Therefore also the subnet N1 ⊂ N is transition bounded, which implies that the projection π 1 : FS → FS1 is a morphism of Petri nets. In order to verify its lifting property it suffices to consider an occurrence sequence σ 1 of FS1 with a single transition t ∈ N1 . By assumption the transition t belongs to one of the distinguished basic components FSB . We consider the composition of projections
FS π1 → FS1 πB → FSB According to Proposition 6 the occurrence sequence π B (σ 1 ) lifts against the composition π B oπ 1 : FS → FSB to an occurrence sequence σ of FS .
Therefore σ is also a lift of σ 1 against π 1 . The lifting property of π 1 : FS → FS1 and the liveness of FS imply that FS1 is live too. Safeness of FS1 follows from the fact that FS1 is a union of basic components of FS and that each of them is also a basic component of FS1 , q. e. d.
The first new concept of this paper is the concept of a non-blocking component. It is a maximal well-behaved and non-blocking subsystem of a well-behaved free-choice system. 8.
Definition (Non-blocking component) Consider a well-behaved free-choice system FS = (N , μ ) . i) For a connected subnet NB ⊆ N the restriction
NS := (NB,μ B ) , μ B := μ | NB , is named a non-blocking component of FS , iff NS is • a union of basic components of FS and • non-blocking and • maximal with respect to these two properties, i.e. no subsystem of FS exists with these properties and containing NS as a proper subsystem. ii) A family (NSi )i∈I of non-blocking components NSi of FS , i ∈ I , with FS = U NSi i∈I is named a non-blocking covering of FS .
Apparently any well-behaved free-choice system has a non-blocking covering because each basic component is non-blocking. In addition, each non-blocking component of FS is well-behaved itself due to Corollary 7. This will be a crucial means for the construction in Definition 14.
A covering of a free-choice system is named unshortenable if no proper subfamily is a covering too. Each covering contains an unshortenable covering as a subfamily: After successively cancelling covering elements contained in the union of other elements we eventually obtain an unshortenable covering.
Example (Non-blocking covering) The well-behaved blocking free-choice system FS from Figure 1 has an unshortenable non-blocking covering with two non-blocking components, cf. Figure 2. One non-blocking component is the union of three different basic components while the other non-blocking component is a single basic component. Bp-systems are a simple class of coloured Petri nets. As mentioned in the Introduction they can be used to define the Boolean semantics of AND/XOR-EPCs. For the present paper we do not need the concept of coloured Petri nets in full generality, the interested reader is referred to [Jen1992]. 10. Definition (bp-system) i) A bipolar synchronization graph (bp-graph) BG is a coloured net. It extends a T-net N = (P, T , F ) by attaching to each place p ∈ P the fixed set
C( p) = Boole := { high, low } with two token colours and provides each transition t ∈ T with one from two types of logic: • An AND-transition t = tAND has a set of firing modes B(t ) = { high, low } with two elements: The high mode (respectively low mode) is enabled iff all preplaces of tAND are marked with at least one high token (respectively low token). •
Its firing consumes one high token (respectively low token) from each pre-place and creates one high token (respectively low token) on every post-place. An XOR-transition t = tXOR with n pre-places and m post-places has a set of firing modes B(t ) = { b(i, j)} with n ⋅ m high modes and one low mode: The high mode with index (i, j) , 1 ≤ i ≤ n, 1 ≤ j ≤ m , is enabled iff the i -th pre-place is marked with at least one high token and all other pre-places with at least one low token. Firing the high mode consumes a high token from the i -th pre-place and a low token from every other pre-place and creates a high token at the j -th postplace and a low token at every other post-place. The low mode is enabled iff all pre-places are marked with at least one low token. Firing the low mode consumes a low token from each pre-place and creates a low token at every post-place. Adhering to the common notation of coloured nets we call a pair ( p, c) with p ∈ P, c ∈ C( p) , a token element and a pair (t, b) with t ∈ T , b ∈ B(t) , a binding element. A binding element is named low binding element, if its firing consumes and creates only low tokens. Otherwise it is named high binding element. ii) A bipolar synchronization system (bp-system) is a coloured Petri net BS = (BG,μ ) with a bp-graph BG and an initial marking μ with at least one high token. Bp-systems are a special case of Boolean systems which have been introduced in [LSW1998]. 11. Definition (Well-behavedness of a bp-system) i) A bp-system BS is safe iff each reachable marking marks every place with at most one token. ii) A binding element of a bp-system BS is live iff for every reachable marking μ1 of BS the bp-system (BG, μ1 ) has a reachable marking which enables the given binding element. BS is live with respect to all its high bindings iff every high binding element of BS is live. iii) A bp-system BS is well-behaved iff it is safe and live with respect to all its high bindings.
In a previous paper [Weh2010], Chap. 2, we have attached several ordinary Petri nets to a given bp-system BS = (BG,μ ) . Notably, a bp-system BS has a restricted free choice system the high-system of BS , together with a morphism high : BS → BS high as well as a
BS high = ( BG high , μ high ),
BS skel = ( BG skel , μ skel ), the skeleton of BS , together with a morphism skel : BS → BS skel . Conversely, each restricted free-choice system FS extends to a bp-system BS with BS high = FS . Hereby one introduces an AND-transition of BS for a branched transition of FS , an XOR-transition of BS for a branched place of FS and a high token of BS for each token of FS . 12. Example (Well-behaved bp-systems) high e_1
Boole AND t_9 e_9 Boole t_1 e_2 Boole t_2 t_1 e_2 Boole t_2 e_12 Boole
AND t_8 high
XOR
low
Boole high high e_10 Boole e_8 Boole e_7 Boole
XOR AND
Boole t_3 Boole Boole t_5 t_5 t_7
Boole t_4 Boole Boole e_11 Boole e_5 Boole t_6 t_6 e_6 Boole systems BSihigh are the two non-blocking components from the well-behaved freechoice system from Figure 2. Note the low token marking the post-place of transition t4 .
The following Proposition 13 shows the relation between well-behaved bp-systems and well-behaved restricted free-choice systems. The proposition has been proven in [Weh2010]. 13. Proposition (Bipolar systems and non-blocking free-choice systems) i) A bp-system is well-behaved iff its skeleton and its high system are well-behaved and its high-system is non-blocking. ii) The high-morphism high : BS → BS high of a well-behaved bp-system BS has the lifting property. iii) Any well-behaved, non-blocking restricted free-choice system FS is the highsystem of a well-behaved bp-system BS .
To obtain a marking such that the bp-scheme BS in Proposition 13, iii) is wellbehaved, possibly some low tokens have to be added in addition to the high tokens prescribed by the marking of FS .
On the other hand, if a restricted free-choice system FS is well-behaved but blocking, no well-behaved bp-system BS exists with BS high = FS .
It is our particular concern in this paper to remedy this situation. Therefore we will apply Proposition 13, iii) separately for each element from a non-blocking covering (FSi )i∈I of FS : For each non-blocking component FSi we obtain a wellbehaved bp-system BFSi
with BFSi high = FSi . For each pair of bp-systems (BFSi , BFS j ) we fuse those subsystems of BFSi and BFS j which project along the high morphisms onto the same subsystem of FS . In the Petri net BSi , which results from BFSi , we consider the low tokens from BFSi to belong to BSi exclusively. For each pair (FSi , FS j ) of non-blocking components of FS we substitute each branched transition t high ∈ ∂ (FSi ∩ FS j ) ⊂ FS from the boundary by a transition which fuses the corresponding bp-systems (BSi , BS j ). The fusing transition has to satisfy the following requirements: • When firing it consumes and creates high tokens from BSi and BS j in the same manner as t high processes tokens from FSi and FS j . •
It consumes and creates low tokens from BSi without synchronizing them with high tokens or with low tokens from BS j . Analogously it consumes and creates low tokens from BS j .
The resulting coloured Petri net is named a linked bipolar system (bp-system). It is the second new concept introduced in this paper. 14. Definition (Linked bp-system) Consider a well-behaved free-choice system FS and a covering (FSi )i∈I of FS by non-blocking components.
to
Corollary 7 each non-blocking component FSi , i ∈ I is a well-behaved free-choice system. It is the high-system of a well-behaved bp-system BFSi , and the high-morphism high i : BFS i → FSi has the lifting property according to Proposition 13. We define a coloured Petri net •
U BFSi
LBS := (hi∈iIgh i )i∈I by forming the quotient of the disjoint union of the bp-systems BFSi , i ∈ I , modulo the identification with respect to the family of high morphisms high i : BFS i → FSi . The coloured Petri net LBS is named a linked bipolar-system (bp-system) attached to FS with respect to the covering FSi , i ∈ I . The high morphisms induce a well-defined morphism of Petri nets
high : LBS → FS .
BSi := π i (BFSi ) ⊂ LBS .
Note that for each index i ∈ I a projection π i : BFSi → LBS onto the quotient exists. The image is a transition bounded subsystem
LBS = (LBN , μ ) , BFSi = (BFNi , μ i ) , BSi = (BNi ,μ i ) ,
FS = (FN ,ν ), FSi = (FNi ,ν i ) Definition 14 of a linked bp-system LBS can be made explicit as follows: • Nodes LBX : Two nodes xi ∈ BFX i and x j ∈ BFX j fuse to a node x ∈ LBX iff highi (xi ) = high j (x j )∈ (FX i ∩ FX j ) ⊂ FX . A well-defined map high : LBX → FX results. We define
I (x):= { i ∈ I : x has a representative xi ∈ BFX i } . • •
Token colours of LBN : A place p ∈ LBX gets the set of token colours
C( p) := { high }∪ { lowi : i ∈ I ( p) } .
Bindings and firing rules of LBN : For a transition t ∈ LBX the binding set B (t ) has as low bindings the low bindings of all representatives ti ∈ BFNi , i ∈ I (t ) , of t , each taken with its firing rule. On the other hand, the high bindings in B (t ) correspond bijectively to the high bindings of one arbitrary ti . Each high binding gets an unchanged flow of high • • tokens. If all representatives ti have logical type AND, then the firing rule of a high binding of t does not consider any low tokens. When all representatives ti have logical type XOR, then the firing rule of a high binding may change the flow of low tokens: When a high binding of ti0 consumes a single low token of type lowi0 at a pre-place of ti0 or creates a single low token of type lowi0 at a post-place, then the corresponding high binding from B (t ) respectively consumes and creates all low tokens of type lowi , i ∈ I (t ) , at the corresponding place of LBN .
Initial marking of LBS : At a place p ∈ LBN the initial marking μ is defined as μ ( p):= v( high ( p) ) + ∑
μ low ( pi )∈ C( p)N .
i∈I ( p) i High morphism: For each index i ∈ I the morphism high i : BFSi → FSi induces a morphism high i : BSi → FSi from the quotient BSi := π i (BFSi ) . These local morphisms fuse to a global morphism high : LBS → FS , such that LBS → LBSi ↓ high ↓ highi
FS → FSi commutes for all i ∈ I , the horizontal maps being the restrictions onto closed subsystems.
Boolei = { high, lowi }, i = 1, 2 , and Boole12 = { high, low1, low2 }.
BN_1 high low1 low2 high left high right low1 low2 high low1 low2 high low1 low2 high high low1 low2 high low1 low2 (high, high) (low1, −) ( −, low2 ) (high, low1 + low2 ) (low1 + low2 , high) (low1, low1 ) (low2 , low2 ) (high, high) (low1, low1 ) (low2 , low2 ) closing AND: reverse opening AND 15. Example (Linked bp-system) Figure 5 shows the linked bp-system attached to the well-behaved free-choice system from Example 3 and its non-blocking covering from Example 9.
UNITE t_1 e_2 Boole_12
t_2 SEP high
XOR
low_2 high e_1 t_6 e_6 high
Beo_o8le_1 Boole_1 e_7 high
UNITE
SEP 16. Remark (Non-uniqueness of a linked bp-system) According to the construction from Definition 14 a well-behaved free-choice system FS = (FN ,ν ) has more than one linked bp-system LBS = (LBN , μ ) in general.
A first reason for non-uniqueness is the choice of a non-blocking covering N = (NSi )i∈I of FS . In general FS has more than one non-blocking covering which is non-shortenable. Therefore the underlying net LBN = LBN (FS, N ) depends not only on FS but also on N .
This kind of dependency is similar to other situations from mathematics. E.g., compare the definition of a differentiable manifold, which is considered a pair (X , A ) formed by a topological space X and a maximal differentiable atlas A on X . But different from the situation of differentiable manifolds two non-blocking coverings N1 and N2 of a well-behaved free-choice system FS are compatible with each other: Their union N1 ∪ N2 is a non-blocking covering of FS again. Employing the definition of morphisms between coloured Petri nets from [Weh2006] one can show that the net of the corresponding linked bp-system is the fibre product
LBN (FS, N1 ∪ N2 ) = LBN (FS, N1) ×FS LBN (FS, N2 ) with respect to the high-morphisms
highi : LBN (FS,Ni ) → FN ,i = 1,2 .
As a consequence the covering Nmax formed by all non-blocking components of FS is the unique maximal non-blocking covering of FS and one can define LBN (FS, Nmax ) as the underlying net of any linked bp-system of FS . A second reason for non-uniqueness is the choice of the low tokens when considering a fixed non-blocking component FSi of FS . In general more than one marking μ i exists with BFSi = (BFNi , μ i ) well-behaved and BFSihigh = FSi . Two different markings differ by the distribution of low tokens. As a consequence, there may exist more than one marking μ on LBN = LBN (FS, Nmax ) with LBS = (LBN , μ ) a linked bp-system of FS .
The following Theorem 17 and its corollary Proposition 19 are the main results of the present paper. They prove that any linked bp-system of a well-behaved free-choice system is well-behaved too. 17. Theorem (High morphism of a linked bp-system) Consider a well-behaved free-choice covering (FSi )i∈I of FS . The high morphism system FS and a
non-blocking high : LBS → FS from a linked bp-system LBS attached to FS with respect to (FSi )i∈I has the lifting property.
Proof. We use the following notations from Definition 14
LBS = (LBN , μ ) , BFSi = (BFNi ,μ i ) , FS = (FN , μ high ), FSi = ( FNi ,μ ihigh ) and denote by the canonical projection.
pri : FN → FNi In order to prove the lifting property of high : LBS → FS we start considering an occurrence sequence
μ high σhigh→ν high of FS . Without loss of generality we may assume that σ high comprises only a single transition r ∈ FN . For each index i ∈ I we define the transition ri := pri (r )∈ FNi . The condition high(t, b) = r determines a unique transition t ∈ LBN and a unique high binding b ∈ B(t ) of t . Analogously, for each index i ∈ I the condition highi (ti , bi ) = ri determines a unique transition ti ∈ BFNi and a unique high binding bi ∈ B(ti ) of ti . In addition, according to Proposition 13 an occurrence sequence exists in the low-system BFSilow such that the marking μ~i of BFSi activates the binding element (ti , bi ) . By catenation we obtain an occurrence sequence σ low μi i→μ~i μi σi →ν i with σ i := σ ilow ⋅ (ti , bi ) . Because BSilow ⊂ LBS of BFSi is a place bounded subsystem the occurrence sequence π i (σ ilow ) of BSilow can be considered an enabled occurrence sequence of BS . Firing π j (σ ljow ) for an arbitrary index j ≠ i does not
μ σlow→μ~ with σ low := π 1(σ 1low )⋅ ... ⋅π n (σ nlow ) Due to Definition 14 the occurrence sequences of all bp-systems BFSi link to an occurrence sequence μ~i (ti,bi)→ν i , i ∈ I , μ~ (t,b)→ν μ σ→ν of LBS . By catenating σ := σ low ⋅ (t, b) we obtain the occurrence sequence of LBS sought-after satisfying high(σ ) = σ high , q.e. d.
For a linked bp-system the definition of liveness with respect to all its high bindings is literally the same as in Definition 11, part ii) for a bp-system. 18. Definition (Well-behavedness of linked bp-systems) Consider a linked bp-system LBS attached to a well-behaved free-choice system FS and a non-blocking covering of FS with k ≥ 1 elements. i) LBS is high-safe iff every reachable marking of LBS marks each place either with a single high token but no low token or with at most k low tokens but no high token. ii) LBS is well-behaved iff it is high-safe and live with respect to all its high bindings. 19. Proposition (Well-behavedness of a linked bp-system) Any linked bp-system LBS attached to a well-behaved free-choice system FS with respect to a non-blocking covering (FSi )i∈I is well-behaved.
Proof. With the notations of Definition 14 we set
LBS = (LBN , μ 0 ) , FS = (FN , high(μ 0 )) = LBS high and (BFSi )i∈I . i)
High-safeness of
LBS follows from the existence of the morphism high : LBS → FS and the safeness of each BFSi , i ∈ I . ii) For the proof that LBS is live with respect to all high bindings we employ the lifting property of high : LBS → FS . We consider an occurrence sequence μ 0 σ1 → μ1 and a transition t ∈ LBN with a high binding b ∈ B(t ) . By definition the binding element (t, b) of LBN is a transition of FN . Liveness of FS implies the existence of an occurrence sequence
high(μ1) σ2high →μ 2high such that the marking μ 2high
activates (t, b) . According to Theorem 17 the occurrence sequence σ 2high lifts to an occurrence sequence μ1 σ2 → μ 2 such that the following diagram commutes μ 0 ↓ high σ1 → μ1 ↓ high σ2 → μ 2 ↓ high high(μ 0 ) high(σ 1)→ high(μ1) σ2high=high(σ 2)→ μ 2high = high(μ 2 ) Therefore LBS is live with respect to all high bindings, q. e. d. 20. Remark (Semantics of AND/XOR-EPCs) Let EPC be an AND/XOR-EPC. As described in the Introduction a free-choice system FS exists, which defines the free-choice semantics of EPC . Also a translation of EPC into a bp-system BS exists. We have BS high = FS . behaved linked bp-system LBS with LBS high = FS , cf. Proposition 19. iii) If FS is non-blocking and well-behaved then LBS = BS , cf. Definition 14.
We have shown that any AND/XOR-EPC, which is well-behaved with respect to its free-choice semantics, can be provided with a Boolean semantics which is wellbehaved too. In order to obtain this result, we had to generalize bp-systems to linked bp-systems, a class of coloured Petri nets which is slightly more general. This step is necessary to tackle EPC with connectors of arbitrary logical type. Apparently one can translate every EPC literally into a Boolean system. But Example 15 indicates that the literal translation possibly has to be altered afterwards to avoid the blocking of low tokens.
Future investigations have to consider the literal translation of an EPC into a Boolean system only as a starting point. For the next step we need an algorithm which identifies well-behaved components of the Boolean system. Then it should link these components to a linked Boolean system, which avoids the blocking of low tokens from different components. These well-behaved components generalize the bpsystems of non-blocking components while linked Boolean systems generalize the concept of linked bp-systems introduced in the present paper.