**INTRODUCTION**

**Petri net**s (PNs) (Murata, 1989) are a well-founded procedure
modeling technique and have been used to model and analyze all kinds of procedures
with applications ranging from protocols, hardware and embedded systems to flexible
manufacturing systems and business processes. PNs are a graphical language.
As a result, PNs are intuitive and easy to learn. Also, the semantics of PNs
and several enhancements (color, time, hierarchy) have been defined formally
(Wang *et al*., 2000).

PNs provide a solid framework for modeling and analyzing workflow processes
(Vander Aalst, 2000; Derks *et al.*,
2001). Workflow management is becoming a mature technology that can be applied
within organizations and across organizational boundaries. It is very important
to use an established framework for modeling and analyzing workflow processes
(Vander Aalst, 1998), since processes are a main factor
in workflow management systems. However, the existing Petri-net-based approaches
are mainly used to investigate functional and secure properties of workflows.
With rapid increase in the number of workflow processes where multiple organizations
are involved, a batch processing function is urgently needed in cooperative
systems, i.e., a batch data of the same type from different organizations need
to be processed before a deadline. Also, the arrival times of these data are
indeterminable, i.e., some data arrive before a given deadline, but others may
not arrive. One usually requires that, to enhance the efficiency of workflows,
all arrived data be processed at a same time slice, while late received data
after the deadline be processed in the next workflow cycle. This situation is
called passing value indeterminacy (Yuyue and Changium, 2002; Du
*et al*., 2007). Therefore, a good formalism of cooperative systems
should be able to model and analyze both the batch processing function and the
passing value indeterminacy.

However, it is very difficult to apply **Petri net**s to the description of the
batch processing function and the indeterminacy (Hao and
Wang, 2003). Because the processing transition doesn’t been fired until
all its input places contain tokens strictly. However, in that situation the
transition needs a flexible trigger condition, i.e., some of its input places
containing tokens are also able to fire the transition. **Petri net**s with weights
of flow arcs may offer the batch processing function, but cannot easily represent
the data arrival indeterminacy as the weights are not less than 1. **Petri net**s
with inhibitor arcs (IPN) have the modeling power of a Turing machine (Suzuki
and Lu, 1989). Although IPNs may model the batch processing function and
the data arrival indeterminacy, the models of systems with these properties
are very complex. To tackle the above problems, therefore, a new formal method-
Logic Petri Net (LPN), an extend **Petri net** with logic transitions, is proposed
and applied efficiently to the modeling and analysis of stock trading systems
and electronic commerce systems (Yuyue and Changium, 2002, 2003; Du
*et al*., 2007). It is illustrated sufficiently that LPNs can model
explicitly and represent compactly the batch processing function and the data
arrival indeterminacy and mitigate the state explosion problem to some extent.

LPNs sort the indeterminacy from interactive across organizational boundaries
into the input and output indeterminacy and describe them respectively
by logic input and output transitions. Firing them is subject to the constraints
from logic expressions. In fact, the indeterminacy is implied by the logic
expressions attached to logic transitions. Doubtless this will enhance
the expression ability of PNs and cater to more application needs. Moreover,
LPNs are able to reduce the size of system models. The objective of this
study is to investigate the equivalence between LPNs and IPNs and to propose
a constructing algorithm of an equivalent IPN from an LPN.

**
**LOGIC PETRI NETS

To apply LPNs to the description of cooperative systems with the batch processing
function and the passing value indeterminacy, two types of places in LPNs, control
and data places are introduced. Control places are used to store control tokens
within an organization, while data places to store data tokens forwarded from
other organizations. Thereby, data places are also called interface places.
Also, there are two kinds of logic transitions in LPNs, logic input and output
transitions. Logic transitions are restricted by logic expressions that can
efficiently describe the batch processing function and the passing value indeterminacy,
such as the indeterminacy of arrival orders or actual trading quantities in
electronic commerce. The transitions cannot be usually expressed in high-level
PNs (Atluri and Huang, 2000), since the type of the data
passed or generated is explicitly fixed by the variable symbol sums.

Assume that this research is based on the elementary net system, i.e.,
the capacity of each place is limited to 1. A brief introduction to PNs
and IPNs is reviewed as follows.

**Definition 1:** PN = (P, T, F, M_{0}) is a PN if and only
if

• |
P is a finite nonempty set of places; |

• |
T is a finite nonempty set of transitions; |

• |
P∩T = ø; |

• |
F⊆(TxP) ∪ (PxT) is a set of arcs, i.e. flow relations; |

• |
M_{0}: P→{0, 1} is the initial marking. |

In the graphic representation, places are drawn as circles or ellipses,
transitions as bars. The flow relations between the nodes (i.e., places
and transitions) are represented as directed arcs and the tokens of the
marking as dots inside places. This study uses the following symbols for
the pre-set and post-set of a node xεP∪T: ^{•}x
= {y|(y, x)εF}, x^{•} = {y|(x, y)εF}, respectively.
R(M_{0}) represents a set of all markings reachable from M_{0}.
A transition t is enabled if each pε^{C}t contains one token
at the current marking Mε R(M_{0}). If t is enabled, it can
fire and a new marking M’ is generated from the current marking M, represented
by M[t>M’, where when pε^{C}t-t^{•}, M’(p)
= M(p)-1; when pεt^{•}-^{•}t, M’(p) =
M(p)+1; otherwise, M’(p) = M(p).

**Definition 2:** IPN = (P, T, F, I, M_{0}) is a PN with inhibitor
arcs if and only if

• |
P is the set of places; |

• |
T is the set of transitions; |

• |
F⊆(PxT)∪(TxP) is a set of the edges (flow relations); |

• |
I⊂PxT is the inhibitor arc set, I∩F = φ and (p, t)εI
is represented as a non-directed arc with a small circle at t side; |

• |
M_{0}: P→ {0,1} is the initial marking of IPN; |

• |
Transition firing rules: ∀tεT, t is enabled if ∀pεP:
(p, t)εF ^{•}t and (p, t)εF: M’(p) = M(p)-1;
^{•}: M’(p) = M(p)+1; otherwise: M’(p) = M(p). |

In the following, LPNs are first defined formally. Then an example is
given to show expressive ability of logic transitions.

**Definition 3:** LPN = (P, T, F, I, O, M_{0}) is a logic
PN if and only if

• |
(P, T, F, M_{0}) is a PN; |

• |
T includes three subsets of transitions, i.e., T = T_{G}∪T_{I}∪T_{O},
∀tεT_{I}∪T_{O}: ^{•}t∩t^{•}
= φ where |

• |
T_{G} denotes a set of traditional transitions; |

• |
T_{I} denotes a set of logic input transitions; |

• |
T_{O} denotes a set of logic output transitions; |

• |
I is a mapping from a logic input transition to a logic input expression,
i.e., _{I}, I(t) = f_{I}(t); |

• |
O is a mapping from a logic output transition to a logic output
expression, i.e., _{O}, O(t) = f_{O}(t); |

• |
Transition firing rules: |

• |
∀tεT_{G}, the firing rules of t are the same
as in PNs; |

• |
∀tεT_{I}, t is enabled only if f_{I}(t)|_{M}
= ^{ •}T^{•}. M [t> M’,∀pε^{•}t,
if M(p) = 1, then M’(p) = M(p)-1; ^{•}: M’(p) = M(p)+1;
∀p∉^{•}t∪t^{•}: M’(p)
= M(p). |

• |
∀tεT_{O},, t is enabled only if ∀pε^{C}t:
M(p) = 1. Firing t will generate a new marking M’, notation M[t>M’
and ∃S⊆t^{•}, S must satisfy f_{O}(t)|_{M’}
= ^{•}T^{•}; ∀pεS: M’(p) =
M(p)+1;∀pε^{•}t: M’(p) = M(p)-1; ∀p∉t^{•}∪^{•}t
or ∀pεt^{•}-S: M’(p) = M(p). |

Fig.1: |
Representation of logic input\output
transitions in LPNs, (a) in put and (b) out put |

Usually such S is not unique, but only one case is selected and the selection
is random. The randomness of S can describe the output indeterminacy of
cooperative systems.

In Fig. 1, t_{1}/t_{2} is a logic input/output
transition and it is restrained by a logic input/output expression f_{I}
(t_{1})/f_{O }(t_{2}). p_{1 }is the control
place; p_{2 }and p_{3 }are the data places. According
to logic input expression f_{I}(t_{1}) = p_{1}Λ
(p_{2}ν p_{3}), in Fig. 1a t_{1}
is enabled if place p_{1} has one token and one or each of places
p_{2} and p_{3} includes one token. In Fig.
1b, p_{3} is the control place; p_{1 }and p_{2
}are the data places. t_{2} is enabled once p includes one
token and firing t_{2} will generate one token in place p_{3}
and one or each of places p_{1} and p_{2} respectively
based on logic output expression f_{O} (t_{2}) = (p_{1}ν
p_{2})Λp_{3}.

In the application situation, when the control place in Fig.
1a contains a token, starting the business processing (transition
t_{1}) requires at least one of the data places whose tokens come
from other organizations contains tokens, instead of each of the data
places must contain tokens rigidly in general **Petri net**s. The situation
in Fig. 1b is similar to that in Fig. 1a.
So, LPNs can describe clearly the batch processing function and the indeterminacy
of data arrival with the corresponding logic expressions. In fact, the
logic expressions can enhance the representation ability of LPNs. With
respect to LPN expressivity, this study will prove that there is the equivalence
between LPNs and IPNs.

**
**EQUIVALENCE OF LPNS AND IPNS

In order to prove the equivalence between LPNs and IPNs, their isomorphism
and equivalent definitions are introduced first.

**Definition 4 (Isomorphism):** Let Σ_{1} = (P, T, F,
I, O, M_{0}) be an LPN and Σ_{2} = (P, T’, F’, I’,
M_{0}) an IPN. RG (Σ_{i}) is the reachable marking
graph of Σ_{i} and R_{i} is the vertex set of RG
(Σ_{i}), i = 1, 2. If there exists a bijective function f
: R_{1}→R_{2}, such that ∀M_{1}, M_{2}ε
R_{1} , tεT, M_{1}[t> M_{2}, → ∃t’0T’,
f(M_{1})[ t’ >f(M_{2}). Then RG(Σ_{1})
and RG(Σ_{2}) are isomorphic.

**Definition 5 (Equivalence):** Let Σ_{1} = (P, T, F,
I, O, M_{0}) be an LPN and Σ_{2} = (P, T’, F’, I’,
M_{0}) an IPN. Σ_{1} and Σ_{2} are equivalent
if and only if RG(Σ_{1}) and RG (Σ_{2}) are
isomorphic.

**Theorem 1:** For any LPN, there exists an equivalent IPN.

Proof: Given an LPN Σ_{1} = (P, T, F, I, O, M_{0})
and IPN Σ_{2 }= (P, T’, F’, I’, M_{0}) is equivalent
to Σ_{1}.

For ∀tεT, we transform each transition of Σ_{1}
into a corresponding transition or a subnet of Σ_{2} on the
basis of the following three cases.

**tεT**_{G}=T-T_{I }∪T_{O}: Let
tεT’; ∀pεP, if (p, t) εF, then (p, t) ε F’;
and if (t, p)εF, then (t, p)ε F’.

**tεT**_{I} : Let ^{•}t = {p_{i1},
p_{i2}, …, p_{ik}}, f_{I}(t) is its logic
input expression. t is enabled once the value of f_{I}(t) is true
on the basis of the token change of places p_{i1}-p_{ik}.
In fact, there may be several situations of places p_{i1}-p_{ik}
where f_{I}(t) is true. However, f_{I}(t) can be transformed
into a disjunctive normal form and the disjunctive normal form is unique,
i.e., each disjunctive clause in the disjunct is a conjunct which consists
of all positive or negative places p_{i1}-p_{ik} and each
conjunct corresponds to a situation of places p_{i1}-p_{ik}
where f_{I}(t) is true.

Thus, the disjunctive normal form of *f*_{I}(*t*) can
be represented as follows:

where, τ_{lj }= p_{ij }or ¬ p_{ij}. f_{I}(t)
is true if and only if one of m disjunctive clauses is satisfied. Any
two disjunctive clauses are mutually exclusive. In the following, m transitions
in Σ_{2} corresponding to m kinds of the true value states
are constructed in the disjunctive normal form respectively. That is,
a logic input transition t with logic expression f_{I}(t) in Σ_{1}
can be represented equivalently by a subnet including m transitions in
Σ_{2} and m transitions correspond to m disjunctive clauses
in the disjunctive normal form of f_{I}(t) respectively. The subnet
is constructed in detail as follows:

For any disjunctive clause lε{1,
2, …, m}

Assume that the disjunctive clause corresponds to a transition t_{l}’
in Σ_{2}, i.e., t_{l}’0T’. Then the arc set of this
subnet is defined. , then (p_{ij},
t_{l}’)εF’; if τ_{lj} = ¬ p_{ij},
then (p_{ij}, t_{l}’)εI’.

If ∀pεt^{•}, then (t_{l}’, p)εF’.
Therefore, firing a logic input transition of Σ_{1} corresponds
to firing a transition of Σ_{2}, i.e., if a logic input transition
is enabled in Σ_{1}, then there must be an enabled transition
in the corresponding subnet of Σ_{2} and it is unique.

**tεT**_{O}: Let t^{•} = {p_{i1},
p_{i2}, …, p_{ik}}, f_{O}(t) is its logic
output expression. t is enabled once its input place p includes a token.
Firing t will generate a token in all or some output places and must assure
that f_{O}(t) is true at the next state of places p_{i1}-p_{ik}..

Similarly, f_{O}(t) can be transformed into a unique disjunctive
normal form. Without loss of generality, assume that the disjunctive normal
form consists of r disjunctive clauses. Thus,

* * where τ_{lj }= p_{ij }or ¬ p_{ij}.
f_{O}(t) decides all possible states of places p_{i1}-p_{ik}
and each disjunctive clause corresponds to a possible state in which f_{O}(t)
is true. Thus r transitions in Σ_{2} corresponding to r kinds
of the possible states are constructed in the disjunctive normal form
respectively. That is, a logic output transition t with logic expression
f_{O}(t) in Σ_{1} can be represented equivalently
by a subnet including r transitions in Σ_{2} and r transitions
correspond to r disjunctive clauses in the disjunctive normal form of
f_{O}(t) respectively. The subnet is built as follows.

For any disjunctive clause,

lε{1, 2, …, r}. Assume that the disjunctive clause corresponds
to a transition t_{l}’ in Σ_{2}, i.e., t_{l}’0T’.
Then the arc set of this subnet is defined.,
then (t_{l}’, p_{ij})εF’; if τ_{lj }=
¬ p_{ij}, then (t_{l}’, p_{ij})∉F’. ∀pε^{
•}t, then (p, t_{l}’)εF’. Therefore, firing a
logic output transition of Σ_{1} corresponds to the occurrence
of a transition in Σ_{2}, i.e., firing a logic output transition
t is functionally equivalent to the occurrence of one of transitions t_{1}’-
t_{r}’.

Therefore, the place set P in Σ_{1} is the same as that
in Σ_{2}. But T≠ T’, F≠ F’ and |T|#*T’*, |F|#*F’*,
where |T |denotes the size of set T. Since Σ_{1}
and Σ_{2} have the same initial marking M_{0}, the
equivalence between Σ_{1} and Σ_{2} are now
proved based on the reachable marking graph.

In Σ_{1}, for ∀M_{1}, M_{2}εR(Σ_{1}),
tεT and M_{1}[t> M_{2}. Then there is a mapping
function f: R(Σ_{1})→R(Σ_{2}) based on
the construction of Σ_{2}, such that f(M_{1}) = M_{1}
and f(M_{2}) = M_{2} and in Σ_{2}, if tεT_{G},
then ∃t’0T’: t’ = t and f(M_{1}) [t’ >f(M_{2});
if tεT_{I} ∪T_{O}, then ∃t_{l}’0T’:
t_{l}’ = t and f(M_{1}) [t_{l}’>f(M_{2}).
Accordingly, f is an identity mapping and satisfies injective and surjection
requirements at MεR(M_{0}). That means that Σ_{1}
and Σ_{2} have the same behavior characteristics. Moreover,
the structure of Σ_{2} is unique since the disjunctive normal
form is only one. So f is a bijective function and RG(Σ_{1})
and RG(Σ_{2}) are isomorphic.

Consequently, Σ_{1} and Σ_{2} are equivalent
based on definition 5. The conclusion holds.

From Theorem 1 and the construction of Σ_{2}, the following
constructing algorithm of an equivalent IPN from an LPN can be obtained.

**Algorithm 1 (Constructing Algorithm):** Transforming an LPN into
an equivalent IPN

Input: an LPN Σ_{1} = (P, T, F, I, O, M_{0})

Output: an equivalent IPN Σ_{2}=(P, T’, F’, I’, M_{0})

(2) |
For each transition t in LPN.T_{G} |

(3) |
IPN.T’ = IPN.T’ ∪{t}; |

(5) |
IPN.F’ = IPN.F’ ∪{(p, t)}; |

(8) |
IPN.F’ = IPN.F’ ∪{(t, p)}; |

(11) |
For each t in LPN.T_{I} |

(12) |
For each disjunctive clause of
f_{I}(t) |

(13) |
IPN.T’ = IPN.T’ ∪{ t_{l}’}; |

(14) |
For each p_{ij} in ^{•}t |

(15) |
If τ_{lj }= p_{ij} then IPN.F’
= IPN.F’ ∪{( p_{ij}, t_{l}’)}; |

(16) |
else IPN.I’ = IPN.I’ ∪{( p_{ij}, t_{l}’)}; |

(19) |
IPN.F’ = IPN.F’ ∪{( t_{l}’, p)}; |

(23) |
For each t in LPN.T_{O} |

(24) |
For each disjunctive clause of
f_{O}(t) |

(25) |
IPN.T’ = IPN.T’ ∪{ t_{l}’}; |

(26) |
For each p_{ij} in t^{•} |

(27) |
If τ_{lj }= p_{ij} then IPN.F’
= IPN.F’ ∪{( t_{l}’, p_{ij})}; |

(30) |
IPN.F’ = IPN.F’ ∪{(p, t_{l}’)}; |

Fig. 2: |
Equivalent IPN subnet of a logical
input transition, (a) logical Input transition and (b) equivalent
IPN subnet |

Fig. 3: |
Equivalent IPN subnet of a logical
output transition (a) logical output transition and (b) equivalent
IPN subnet |

For any LPN, therefore, its equivalent IPN can be easily built based
on theorem 1 and algorithm 1. In the following, the transformation processes
from a logic transition in LPN to an equivalent subnet in IPN are illustrated
with two examples (Fig. 2, 3).

**Example 1:** Transforming a logic input transition in LPNs to an
equivalent subnet in IPNs. In Fig. 2a, t_{1}
is a logic input transition in an LPN and f_{I}(t_{1})
= p_{1}Λ(p_{2}νp_{3}) is its logic input
expression. t_{1}^{•} = {p} and ^{•}t_{1}
= {p_{1}, p_{2}, p_{3}}. f_{I}(t_{1})
is transformed into a disjunctive normal form as follows.

f_{I}(t_{1}) |
= |
p_{1}Λ(p_{2}νp_{3}) |

Â |
= |
(p_{1}Λp_{2})ν(p_{1}Λp_{3}) |

Â |
= |
((p_{1}Λp_{2})Λ(p_{3}ν5p_{3}))ν((p_{1}Λp_{3})Λ(p_{2}ν5p_{2})) |

Â |
= |
(p_{1}Λp_{2}Λ5p_{3})ν(p_{1}Λ5p_{2}Λp_{3})ν(p_{1}Λp_{2}Λp_{3}) |

By means of the proof process of theorem 1 and algorithm 1, logic input
transition t_{1} can be transformed equivalently into the subnet
of an IPN in Fig. 2b. From the proof process of theorem
1, three disjunctive clauses of f_{I}(t_{1}) correspond
with three transitions in the IPN subnet, i.e., (p_{1}Λp_{2}Λ5p_{3})→t_{11},
(p_{1}Λ5p_{2}Λp_{3}) →t_{12}
and (p_{1}Λp_{2}Λp_{3}) →t_{13}.
That is, the disjunctive normal form of f_{I}(t_{1}) decides
fully the structure of the corresponding IPN subnet. (p_{3}, t_{11})
and (p_{2}, t_{12}) are two inhibitor arcs. The place
sets in Fig. 2a and Fig. 2b are the
same, i.e., ^{•}t_{1}∪t_{1}^{•}
= ^{•}t_{11}∪t_{11}^{•}∪
^{•}t_{12}∪ t_{12}^{• }∪
^{•}t_{13}∪t_{13}^{•}
= {p_{1}, p_{2}, p_{3}, p}.

**Example 2:** Transforming a logic output transition in LPNs to an
equivalent subnet in IPNs. In Fig. 3a, t_{2}
is a logic output transition in an LPN and f_{O}(t_{2})
= (p_{1}νp_{2})Λp_{3} is its logic output
expression. t_{2}^{•} = {p_{1}, p_{2},
p_{3}} and ^{•}t_{2} = {p}. The disjunctive
normal form of f_{O}(t_{2}) is deduced as follows.

f_{O}(t_{2}) |
= |
(p_{1}νp_{2})Λp_{3} |

Â |
= |
(p_{1}Λp_{3})ν(p_{2}Λp_{3}) |

Â |
= |
((p_{1}Λp_{3}) Λ(p_{2}ν5p_{2}))ν((p_{2}Λp_{3})Λ(p_{1}ν5p_{1})) |

Â |
= |
(p_{1}Λ5p_{2}Λp_{3})ν(¬ p_{1}Λp_{2}Λp_{3})ν(p_{1}Λp_{2}Λp_{3}) |

Similarly, Fig. 3b shows the equivalent IPN subnet of
t_{2}. By the constructing method of IPNs, three disjunctive clauses
of f_{O}(t_{2}) correspond with three transitions in the
IPN subnet. Therefore, the disjunctive normal form of f_{O}(t_{2})
decides fully the structure of the corresponding IPN subnet.

From the examples, it is a fact that the size of an IPN model can be
reduced in its equivalent LPN model, since many transitions are capsulized
into an equivalent logic transition. Their modeling power and behaviors
are same, because IPNs and LPNs have the same reachable marking graph
in essence and IPNs and LPNs are isomorphic.

**
**CONCLUSION

With the rapid progress of cooperative and network extent of interorganizational
workflows, batch processing function and passing value indeterminacy of workflow
processes need often to be considered in the design of workflow systems. Moreover,
formal modeling and analysis technologies should have the modeling ability of
these functions. To deal with the problems, a new extension of PNs, i.e., LPNs,
is proposed in (Yuyue and Changium, 2002; Du *et al*.,
2007) and its practical application is illustrated with some nontrivial
examples. This study focuses on the analysis of the modeling power of LPNs and
the equivalency between LPNs and IPNs. The equivalency is proved formally and
a constructing algorithm of equivalent IPNs from LPNs is proposed based on the
disjunctive normal forms of logic input/output expressions. Moreover, the size
of LPN models is smaller than that of the equivalent IPN models.

Further study will be the investigation of fundamental properties of LPNs,
such as liveness, state equivalency and reachability. Moreover, the analysis
technologies of LPNs will be studied and its developmental tool is considered
and designed.

**
**ACKNOWLEDGMENTS

This study was supported in part by the National Natural Science
Foundation of China under Grant 60773034 the Taishan Scholar Construction

Project of Shandong Province, China; the National Basic Research Program
of China (973 Program) under Grants 2007CB316502 and 2004CB318001-03;
and the Open Project of the State Key Laboratory of Computer Science,
Institute of Software, Chinese Academy of Sciences under Grant SYSKF0804.