INTRODUCTION
Due to the enhancement of reliability and safety of communication networks, the number of entities and the heterogeneity of cooperative systems are unprecedented and require new approaches to model and verify their correctness and temporal properties. It is inspiring that today’s workflow management systems support business processes of complex systems via electronic networks and are widely used by organizations to coordinate the execution of various applications representing their daytoday tasks. A workflow is a representation of a given process that consists of welldefined set of activities, referred to as tasks. Each of the tasks in the process represented by a workflow serves a given function and has some input requirements and may also generate information as a part of its output. The tasks in a workflow are usually related and dependent on one another. These task dependencies are called intraworkflow dependencies. Task dependencies may also exist across workflows where multiple organizations are involved in shared business processes, such task dependencies are referred to as interworkflow dependencies. In general, task dependencies are divided into three types: control dependencies, value dependencies and external dependencies.
Van der Aalst (2000) defined interorganizational workflow
nets (IOWF) to model loosely coupled interorganizational workflows. An IOWFnet
describes the local workflows and the coordination structure for their interaction.
XRL (eXchangeable Routing Language) language (Verbeek et
al., 2002), which based XML language, was used for the specification
of interorganizational workflows. Van der Aalst (2003)
described formally the PublicToPrivate (P2P) approach to construct interorganizational
workflows based on a notion of inheritance. The public parts are related to
each other, making up an interorganizational workflow. Each private workflow
corresponds to an actual workflow as it is executed in one of the domains. The
P2P approach guarantees that each private workflow is a subclass of the corresponding
public part under projection inheritance. A new approach on the modeling of
interorganizational workflows is presented based on nested Petri nets (Prisecaru
and Jucan, 2008). It deals with loosely coupled Interorganizational workflows:
there are n local workflow processes which can behave independently, but need
to interact at certain points in order to accomplish a global business goal.
Soundness is introduced and proved.
An objectoriented technology is used to analyze the soundness of interorganizational
workflows (Sun and Du, 2008). It focuses on interactive
messages in an interorganizational system. Each workflow entity is packaged
based on the objectoriented technologies. Each private workflow is considered
as one object. The study put more attention on the whole part and interactive
actions of the workflows. Some details inside one private workflow are neglected.
It investigates interactive messages need to satisfy the properties in a sound
interorganizational workflow.
An Interorganizational Logical Workflow Net (ILWN) (Du et
al., 2007) is presented for modeling and analyzing cooperative systems
based on Logical Petri Nets (LPN), workflow techniques and temporal logic. It
can model passing value indeterminacy and describe batch processing function
of cooperative systems which the existing formal techniques cannot model. Through
attaching logical expressions to some actions of an ILWN model, the size of
the model is reduced. Thus, ILWN can mitigate efficiently the state explosion
problem to some extent.
The modeling power of LPN and the equivalency between LPN and Petri Nets (PN)
with inhibitor arcs (IPN) are analyzed and verified (Du
and Guo, 2009). The equivalency is proved formally and a constructing algorithm
of equivalent IPN from LPN is proposed based on the disjunctive normal forms
of logic input/output expressions.
Soundness is an important property for ILWN. As a matter of fact, soundness
can be decided; however, it is EXPSPACE hard (Van der Aalst,
2000). Thereby, soundness is discussed for an important subclass in this
paper: Trestricted ILWN.
For the Trestricted ILWN, this study discusses how to compose ILWN to preserve
soundness. Our results can be more expediently used by the designers of cooperative
workflows in comparison with message sequence charts (Alur
and Yannakakis,1999) because the method in this study can reduce the analysis
complexity of ILWN consumedly. At last methods and concepts are illustrated
with a useful example of an auto gas station system.
PRELIMINARIES
Here, we briefly review the notations of Petri nets, workflow nets and logical Petri nets.
A Petri net (Murata, 1989) is a fourtuple PN = (P,
T, F, M_{0}), where P is a set of places, T is a set of transitions,
P∩T=φ, F⊆(PxT)∪(TxP) are the edges (flow relations) and M_{0}:
P→ N ∪{0} (N is a natural number set) is the initial marking of PN. R(M_{O})
represents the set of all markings reachable from M_{O}. x∈P∪T:
•x={y (y, x)∈F} and x•={y (x, y)∈F}. For Q⊂P∪T, •Q=∪_{q∈Q}
•q and Q•=∪_{q∈}q•.
Places are graphically drawn as circles, transitions are drawn as bars and the flow relations are drawn as directed arcs. A transition t is enabled if each place p∈Ct contains at least one token. When an enabled transition t fires, for ∀p∈Ct, one token is removed from p and for ∀p∈t•, one token is added to p. This results in a new marking M', denoted by M[t>M'.
A Petri net is strongly connected if and only if for every pair of nodes x and y, there is a path leading from x to y. It is bounded if and only if ∀p∈P, there is a natural number k such that ∀M∈R(M_{0}): M(p)≤k.
Definition 1: PN = (P, T, F, M_{0}) (Van
der Aalst, 1999) is a workflow net (WFnet) iff:
• 
PN has two special places: i and o. Place i is a source place:
•i =φ; Place o is a sink place: o•=φ 
• 
If a transition t^{#} is added to PN which connects
place o with i (i.e. •t^{#} ={o} and t^{#} •={i}),
the resulting PN is strongly connected 
Note that i (o) is used to denote place i (o) and the marking with only one
token in place i (o).
A workflow net is constructed by several basic building blocks: ANDsplit AndJoin,
ORsplit and ORjoin (Van der Aalst, 2000).
However, it is difficult that the passing value indeterminacy and batch processing function of cooperative systems are described in WFnets.
Definition 2: A Logical petri net (Du et al.,
2007) is a 7tuple LPN = (P, T, F, Dt, I, O, M), where P is a set of places;
T = T_{D}∪ T_{I}∪ T_{O }is a set of transitions;
T_{D} is a set of delay transitions; T_{I} is a set of logical
input transitions; T_{O }is a set of logical output transitions and
P, T_{D}, T_{I} and T_{O} are disjunct sets; F ⊆(Px(T_{D}
∪ T_{I}∪ T_{O}))∪((T_{D} ∪ T_{I} ∪
T_{O}) xP) is a set of arcs; Dt is a function such that ∀t∈T_{D},
Dt(t) ∈R, which denotes the delay time of t; I is a mapping function such
that t∈T_{I}, I(t) is a logical input expression f_{I}, while
O is a mapping function such that ∀t∈T_{O}, O(t) is a logical output
expression f_{O}; M is a marking function.
The LPN representations of logical input and output transitions are shown in
Fig. 1a and b.
Firing rules of the transitions in LPNs are as follows:
• 
∀t∈T_{D}, dt(t)=τ, t is said to be
enabled if ∀p∈Ct; M(p)=1; t is said to be firable if its enabled
time is equal to τ and firing t results in a new marking M': ∀p∈Ct:
M'(p)=M(p)1; ∀p∈t•: M'(p)=M(p)+1 
• 
∀t∈T_{I}, I(t)=f_{I}, t is said
to be enabled if f_{I}_{M} = _{•}T_{•},
i.e., all input places of t satisfy the logical input expression f_{I}
at M; if t is enabled, it can fire and firing t generates a new marking
M': ∀p∈Ct: M'(p)=0; ∀p∈t•: M'(p)=M(p)+1 
• 
∀t∈T_{O}, O(t)=f_{O}, t is said
to be enabled if ∀p∈Ct, M(p)=1; if t is enabled, it can fire
and generates a new marking M': ∀p∈Ct: M'(p)=M(p)1; for t•,
f_{O}_{M'} = _{•}T_{•} 
A logical input transition is enabled only if the available tokens of its all
input places satisfy a given logical expression and there exists no token in
its all input places after it fires.

Fig. 1: 
Representations of logical (a) input and (b) output transitions 
The notation f_{I }(f_{O}) is used to denote the logical expression
of a logical input (output) transition. Logical input or output transitions
are represented graphically by the rectangles in which mark I or O is embedded,
respectively. Figure 1 shows that task A is enabled only if
p1 has at least one token and p2 or p3 has at least one token. The enabling
conditions of logical output transitions are the same as ones of the transitions
in classical Petri nets. The output places of a logical output transition must
satisfy its logical expression f_{O} and depends on new generated values
when firing it. The output of logical output transitions is nondeterminate
in static structures. Figure 1b denotes that one token is
generated in p1 and there is one token in one of p2 and p3, or in each of them,
after executing task A.
Definition 3: Let M be a reachable marking in a LPN, α a firing sequence
at M, f and g LPN formulae. α= β_{i}Υ_{j}, β_{i}
is the prefix of α with length i and Υ_{j} is the postfix of α excluding
β_{i,} LPN formulas are defined recursively (Du
et al., 2008).
• 
=p iff there is at least one token in place
p at M 
• 
=t_{fir} iff transition tεT
is firable at M 
• 
=t iff transition t fires, t∈T_{D}∪T_{I}∪T_{O.} 
• 
= f⇒g iff =f implies
=g 
• 
=of iff α λ and 1,Υ_{1}>=f 
• 
=□f iff < M_{i},Υ_{i}
>=f for every i: 0≤i≤ α 
• 
=◊f iff _{i},Υ_{i}>=f
for some i: 0≤i≤ α 
• 
= fΔg iff if = f
and = g then
= f ∧ g,else =f ∨ g 
Here, symbols ¬, ∧ and ∨ are the Boolean connectives. Symbol Δ, as a substitutive operator, is used to describe the passing value indeterminacy. If f and g become true in M, then fΔg is replaced by f ∧ g and otherwise by f ∨ g. In this study, _{•}T_{•} is used to represent a logical true value in logical expressions.
TRESTRICTED ILWN
Definition 4: (T1live) A transition t in a Petri net (PN, M) is 1live
iff the following holds (Van der Aalst, 1999):
• 
For every marking M’ reachable without firing t, there
is a state M’N reachable from M’ which enables t 
• 
For every marking M’ reachable via a firing sequence
which fires t, there is no state reachable from M' which enables t 
Definition 5: A LWN=(P, T, F, DT, I, O, M) (Du et
al., 2007) is called a logical workflow net iff:
• 
The LPN has two disjunct subsets, P_{C }and P_{D}
and P = P_{C} ∪ P_{D}, where P_{C }is a set
of control places, P_{D} a set of interface data places 
• 
P_{C }includes two special places: i and o. Place
i is a source place: •i=Ø. Place o is a sink place: o•=Ø 
• 
∀tεT, •t and t• include one control
place at least, respectively 
• 
If we add a transition t^{#} to the LPN which connects
place o with i ( •t^{#} = {o} and t^{#} • ={i}),
then its inner logical net
is strongly connected, where =
F(P_{D}x T∪TxP_{D}) 
There are two types of places in LWN, control places and data places. Control places are used to deposit control tokens, data places to deposit data tokens. Data places are also called interface places.
Definition 6: An LWN (Sun and Du, 2008) is sound
iff in
• 
there exist a firing sequence α, such that 
• 
there exist a firing sequence α such that 
In the above definition, requirement 1 means that for
there exists a firing sequence α such that Requirement
2 means that there is no dead transition in the inner logical marking net Since,
the interface data places and their related arcs are omitted in an inner logical
net, we can think of the marking net
as its logical workflow process, i.e., the corresponding organization has full
control over the local part of the LWN.
We demand that each interface data place in P_{D} has one sender and one receiver. Moreover, each transition involved in interface data places between instances has to be T1live. A logical workflow net which meets these two requirements is called a Trestricted logical workflow net.
Definition 7: (Trestricted logical workflow nets) A Trestricted logical workflow net is a logical workflow net which satisfies the following requirements:
• 
p∈P_{D}, C p= p• =1 
• 
t∈CP_{D}∪ P_{D}•, t is T1live 
Definition 8: Let LWN_{j} = (P_{j}, T_{j}, F_{j},M_{0j,} DT_{j}, I_{j},O_{j}) be an LWN of the jth cooperative organization, j = 1, 2, . . .,n. ILWN = (P, T, F,M_{0},DT, I,O) is an ILWN iff the following hold.
• 
P = ∪_{1≤j≤n} P_{j} ; T = ∪_{1≤j≤n}
T_{j} ; F =∪_{1≤j≤n} F_{j} 
• 
tεT_{j}, DT(t) = DT_{j}(t), j = 1, 2,
. . .,n 
• 
tεT_{Ij}, I_{(t)} = I_{j(t)}
and ∀tεT_{Oj},O(t) = O_{j(t)} 
Where, T_{Ij} is a set of logical input transitions in T_{j} and T_{oj} is a set of logical output transitions in T_{j}, j =1, 2, . . .,n.
• 
M_{0} is the initial marking and ∀p ε
P_{j} : M_{0(p)} =M_{0j(p)}, j = 1, 2, . . .,n 
• 
The transition firing rules of the ILWN are the same as in
Definition 3 
If an additional transition t^{#}_{j} is added to LWN_{j},which connects place o_{j} with i_{j}, j = 1, 2, . . ., n, ILWN^{#} = (P, T^{#},F^{#},M_{0},DT, I,O) is called an extended ILWN, where T^{# } = T ∪ {t^{#}_{1}^{,} . . ., t^{#}_{n} } and F^{# }= F ∪ {(o_{1}, t^{#}_{1}), (t^{#}_{1}, i_{1}), . . ., (o_{n}, t^{#}_{n }), (t^{#}_{n}, i_{n})}.
Definition 9: (Trestricted ILWN) A ILWN is called Trestricted ILWN if each of its LWNs is Trestricted.
An ILWN can be obtained through superposing the interface data places among
the related LWNs by the definition if the local workflow processes of each cooperative
organization are modeled by an LWN. However, the correctness of an ILWN may
be destroyed due to asynchronous communication since the passing values between
organizations may be subjected to order errors of some sending and receiving
actions or incorrect choice of firing sequences. In Fig. 2,
LWN1 and LWN2 are both sound, but their ILWN is not live, because t11, t12,
t21 and t22 are dead transitions. But if the order of a receiving action and
a sending action is exchanged in one of two LWNs, the ILWN is live. For example,
if (p2, t21) and (t22, p1) are replaced with (p2, t22) and (t21, p1), respectively,
the ILWN becomes live.

Fig. 2: 
An ILWN composed of two LWNs 
Definition 10: An ILWN is sound (Du et al.,
2007) iff
• 
Each of its LWNs is sound 
Definition 11: Let LWN be a logical workflow net. C is a path leading from a node n_{1} to a node n_{k} iff there is a node sequence _{1},n_{2},…,n_{k}> in the LWN such that (n_{i},n_{i+1})ε(TxP)∪(PxT), i = 1,2,…,k1. Assume that & (C) denotes the alphabet of a path C, i.e., & (C) = {n_{1},n_{2},…,n_{k}}.
Soundness analysis of ILWNs: Here, soundness of Trestricted ILWN is analyzed. In the following, this study discusses soundness of a Trestricted ILWN composed of two Trestricted LWNs. The output transition of p is denoted by s(p). The input transition of p is denoted by r(p)._{ }
Theorem 1: Let ILWN be Trestricted and composed of two sound LWNs: LWN1 and LWN2. ∀p, qεP_{D}, s(p)εT_{1}, s(q)εT_{2}, c1 is an arbitrary path leading from i_{1} to s(p). c2 is an arbitrary path leading from i_{2} to s(q).T_{i1} is the set of input transitions on path c1. T_{i2} is the set of input transitions on path c2.ILWN is sound iff r(q) ∉ T_{i1} or r(p) ∉ T_{i2}.
Proof
Necessity: Since LWN_{1} and LWN_{2} are sound, each
of their is
live. If both LWNs in an ILWN are sound,the correctness of the ILWN depends
on the liveness of the transitions related to the places in P_{D} and
their precedence order in every local workflow process. Based on definition
of ILWN, however, the order cannot be updated when an ILWN is constructed, i.e.
the structural order of the transitions in every LWN is the same as in the ILWN.
Consequently, when both LWNs are sound in an ILWN, if the ILWN is not live,
this means that the incorrect order of the transitions related to the interface
data places in some LWNs leads to some dead ones in the ILWN.
Case 1: If t∈T∩(•P_{D}∪P_{D}•) is not in conditional routing structures, this means that the sending and receiving actions between LWN_{1 }and LWN_{2} are only in sequential routing constructions and parallel routing constructions in LWN_{1 }and LWN_{2.} By means of the conditions of the theorem, p∈P_{D}, Cp= p•*=1, r(q) ∉ T_{i1} or r(p) ∉ T_{i2}, i.e., r(q) ∈ T_{i1} and r(p) ∈ T_{i2} are not satisfied simultaneously. That is to say, it will not happen that s(p) ∈T_{1} waits to receive the data q to be not sent by LWN_{2} and s(q) ∈T_{2} waits to receive the data p to be not sent by LWN_{1}. Thereby, each transition in c_{1 }and c_{2} is live in the ILWN.
Case 2: If t∈T∩(•P_{D}∪P_{D}•) is in conditional routing structures, there exist two cases.
• 
For t∈T∩CP_{D}, if the branch that contains
t is not selected, t will not fire. It is possible r(T•1P_{D})
will not fire. Thus, r(T•1P_{D}) is not live 
• 
For t∈T∩P_{D}•, if the branch that
contains t is not selected, t will not fire. It is possible •T⊆P_{D}
still contains one token even when one workflow finishes 
However, by means of the conditions of the theorem, t∈CP_{D}∪ P_{D}•, t is T1live, i.e.,t∈CP_{D}∪ P_{D}• must fire once. So the above two cases will not happen. In addition, by means of the other conditions of the theorem, the analysis is similar to case 1.So t∈T∩(•P_{D}∪P_{D}•) in conditional routing structures is also live in the ILWN.
Sufficiency: Let ILWN be sound, but r(q) ∉ T_{i1} ∨ r(p) ∉ T_{i2}=.F., i.e., r(q)∈T_{i1}∧ r(p)∈T_{i2.}This means that s(p) ε T1 waits to receive the data q to be not sent by LWN_{2} and s(q)εT2 waits to receive the data p to be not sent by LWN_{1.}This causes a deadlock. ILWN is not sound. This conclusion conflicts with conditions. So, the assumption is false, i.e., r(q) ∉ T_{i1} or r(p) ∉ T_{i2}.
Corollary 1: An ILWN composed of n LWNs (LWN_{1, }LWN_{2}, ….. LWN_{n }) is sound if and only if:
• 
LWN_{i}, LWN_{j}(1i and LPN_{j }is sound 
• 
ILWN composed of ILWN' and other n2 LWNs (LWN_{m1, }LWN_{m2},
….. LWN_{m(n2)}. m_{k}≠ i and m_{k}≠ j)
is sound 
Proof: It is similar to the Theorem 1. Based on Theorem 1,it is easy to verify the corollary 1.
Corollary 2: An ILWN composed of n LWNs (LWN_{1, }LWN_{2}, ….. LWN_{n }) is sound if and only if:
• 
LWN_{i}, LWN_{j}(1i and LWN_{j }is sound 
• 
For every two LWNs :LWN_{i}, LWN_{j}, an ILWN_{m}
is obtained through the combination of them. Thus, n/2 ILWNs are gotten.
The ILWN composed of these n/2 ILWNs is sound 
Proof: It is similar to the Theorem 1.Based on Theorem 1, it is easy to verify the corollary 2.
THE EXAMPLE OF AN AUTO GAS STATION SYSTEM
An auto gas station example is modeled and analyzed to illustrate concepts
and techniques proposed in this study. It is designed based on an auto gas station
example (Corbett, 1996). The model is as follows:
An auto gas station system is made up of three parts: a customer, an operator and a pump. In the example, an operator first accepts a customer’s prepaid and then accepts charge of pump.
The workflow model of a customer is described by Fig. 3.
The workflow model of an operator is shown in Fig. 4. The
workflow model of a pump is shown by Fig. 5. In Fig.
3, some logical input expressions and logical output expressions must be
satisfied: f_{o}(t_{3}) = wait acko4∧ackentryo4,f_{I}(t_{4})=ackaccepto4∧
wait acko4, f_{o}(t_{5})=waitackp5∧ackentryp5,
f_{I}(t_{6})=ack acceptp5∧ waitackp5, f_{o}(t_{7})=wait
ackp6∧ack entryp6, f_{I}(t_{8})=ackacceptp6∧
wait ackp6∧ack entryc29, f_{o}(t_{9})=endloop8∧ackacceptc29.
In Fig. 4, some logical input expressions and logical output expressions must
be satisfied: f_{I}(t_{23})=select23 ∧ackentryo4,f_{o}(t_{24})=ackentryp25∧waitackp25,
f_{I}(t_{25})=waitackp25∧ackacceptp25, f_{o}(t26)=ack
accepto4∧endselect31, f_{I}(t_{28})=select23∧ackentryo16,f_{o}(t_{29})=ackentryc29∧waitackc29,f_{I}(t_{30})=
endaccept30∧ackacceptc29. In Fig. 4, some logical input expressions
and logical output expressions must be satisfied: f_{I}(t_{13})=accept13∧ackentryp25,f_{o}(t_{13}^{'})=
ackacceptp25∧accept14,f_{I}(t_{14})=ackentryp5∧accept14,f_{o}(t_{14}^{'})=ackacceptp5∧
accep15,f_{I}(t_{15})=accep15∧ackentryp6,f_{0}(t_{16})=ackentryo16∧waitacko16,f_{I}(t_{17})=
waitacko16∧ackaccepto16,f_{0}(t_{18})=ackacceptp6∧endloop18.

Fig. 3: 
The LWN model of a customer 

Fig. 4: 
The LWN model of an operator 
According to Definition 7, we can judge that three logical workflow nets in
Fig. 35 are sound. In the following, how
to combine the three LWNs into one ILWN and how to verify the soundness of the
ILWN are illustrated.

Fig. 5: 
The LWN model of a pump 
Based on Corollary 1, firstly, the LWN of an operator and the LWN of a pump may be combined into one ILWN and the soundness of the ILWN can be verified by Theorem 1. Second, the LWN of an customer and the ILWN of an operator and an pump may be combined into one new ILWN and the soundness of the newly combined ILWN can be verified by Theorem 1:
(1) 
Combine the LWN of an operator and the LWN of a pump into
one ILWN. There are four interface data places between the LWN of an operator
and the LWN of a pump: let P_{D}={ackentryp25,ackaccepto16,ackacceptp25,ackentryo16}.
s(ackentryp25)=t24∈T(operator),s(ackaccepto16)=t31∈T(operator),s(ackacceptp25)=t13'∈T(pump),s(ackentryo16)=t16∈T(pump).r(ackentryp25)=t13∈T(pump),r(ackaccepto16)=t17∈T(pump),r(ackacceptp25)=t25∈T(operator),r(ack
entryo16)=t28∈T(operator). there is one path c_{o1} from
begin21operator to s(ackentryp25)=t24.c_{o1}:begin21operator→t20→loop22→t21→select23
→t23→ entryp25→t24. 
There are four paths from begin21operator to s(ackaccepto16)= t31∈T(operator).c_{o2}:begin21operator→t20→loop22→t21→select23→t23→entryp25→t24→waitackp25→t25→endaccept26→t26→endselect31→t32→end loop32→loop32→t21→select23→t28→entryc29→t29→waitackc29→t30→ endaccept30→t31.c_{o3}:begin21operator→t20→loop22→t21→select23→t23→ entryex244→t26→endselect31→t32→endloop32→loop32→t21→select23→t28→entryc29→t29→waitackc29→t30→endaccept30→t31.c_{o4}:begin21operator→t20loop22→t21→select23→t23→entryp25→t24→waitackp 32→loop32→t21→select23→t28→entryex2816→t31.c_{o5}:begin21operator→t20→loop22→t21→select 23→t23→entryex244→t26→endselect31→t32→endloop32→loop32→t21→select23→t28→entryex2816→t31.
There is one path from begin11pump to s(ack ent ry o16)=t13'∈T(pump).c_{p1}: begin11pump →t11 → loop12→t12→accept13→t13→accept14'→t13'.
There is one path from begin11pump to s(ack entryo16)=t16∈T(pump).c_{p2}: begin11pump→t11→loop12→t12→accept13→t13→accept14'→t13'→accept14→t14→accept15'→t14'→accept15→t15→entryo16→t16.
T_{o1} denotes the set of transitions receiving interface data places of & (c_{o1}). T_{o1}=ø.T_{o2} denotes the set of transitions receiving interface data places of & (c_{o2}). T_{o2}={t_{25},t_{28}}.T_{o3} denotes the set of transitions receiving interface data places of & (c_{o3}). T_{o3}={t_{28}}.T_{o4} denotes the set of transitions receiving interface data places of & (c_{o4}). T_{o4}={t_{25},t_{28}}.T_{o5} denotes the set of transitions receiving interface data places of & (c_{o5}). T_{o5}={t_{28}}.T_{p1} denotes the set of transitions receiving interface data places of & (c_{p1}). T_{p1}={t_{13}}.T_{p2} denotes the set of transitions receiving interface data places of & (c_{p2}). T_{p2}={t_{13}}.
r(ackacceptp25)=t25∈T(operator)∉T_{o1,}r(ackacceptp25)
= t25∈T(operator) ∈T_{o2}, r(ackacceptp25)=t25∈T(operator)∉T_{o3,}r(ackacceptp25)=t25∈T(operator)
∈T_{o4,} r(ackacceptp25) = t25∈T(operator) ∈T_{o5,
}r(ackentryo16)=t28∈T(operator)∉T_{o1,} r(ack entry
o16)=t28∈T(operator) ∈T_{o2,} r(ackentryo16) = t28 ∈T(operator)
∈T_{o3,} r(ackentryo16) = t28∈ T(operator) ∈T_{o4,}
r(ackentryo16) = t28∈T(operator) ∈T_{o5, }r(ackentryp25)
= t13∈T(pump)∈T_{p1,}r(ackentry p 25) = t13∈T(pump)∈T_{p2
}r(ackaccepto16) = t17∈T(pump)∉T_{p1,}r(ackaccepto16)
= t17∈T(pump)∉T_{p2.}

Fig. 6: 
The ILWN composed of an operator and a pump 
For ackentryp25∈P_{D}, ackacceptp26∈P_{D}, s (ackentryp25) = t24∈T (operator), s(ackacceptp25) = t13' ∈T(pump),r(ackentryp25)=t13∈T(pump)∈T_{p1},r(ackacceptp25)=t25∈T(operator)∉T_{01}.
In the same way, we can include for s (ackentryp 25) = t24∈T(operator), s(ackentryo16) = t16∈T(pump). r(ackentryp25) = t13∈T(pump)∈T_{p2}, r(ackentryo16)= t28∈T(operator)∉T_{01}.
For s(ackaccepto16) = t31∈T(operator),s(ack acceptp25) = t13'∈T(pump). r(ackaccepto10) = t17∈ T(p ump)∈T_{p2},r(ackacceptp25) = t25∈T(operator)∉T_{01, }r(ackaccepto10) = t17∈T(pump)∉T_{p1},r(ackentryp25) = t25∈T(operator)∈T_{0i} = .T. i∈{2,3,4,5}.
For s(ackaccepto16) = t31∈T(operator),s(ackentryo16) = t16∈T(pump). r(ackaccepto10) = t17∈T(pum p)∈T_{p2},r(ackentryo16) = t28∈T(operator)∉T_{01,} r(ackaccepto10) = t17∈T(pump)∉T_{p1},r(ackentryo16) = t28∈T(operator)∈T_{0i} = .T. i∈{2,3,4,5}.
Thereby, the conditions of Theorem 1 are satisfied. According to Theorem 1, the soundness of the ILWN composed of an operator and a pump can be verified. The ILWN composed of an operator and a pump is shown in Fig. 6.

Fig. 7: 
The ILWN composed of a customer,an operator and a pump 
(2) 
In the same way, combine the ILWN of a customer and the ILWN
composed of an operator and a pump into one new ILWN. There are eight interface
data places between the LWN of a customer and the ILWN composed of an operator
and an pump: let P_{D}={ackentryo4, ackaccepto4, ackentryp5,
ackacceptp5, ackentryp6, ackacceptp6, ackentryc29, ackacceptc29}.Based
on Theorem 1, soundness of the ILWN can also be verified. The ILWN composed
of a customer, an operator and a pump is shown in Fig. 7 
So, according 1 and 2, it can be included that the ILWN composed of an operator, a pump and a customer is sound.
CONCLUSION
In this study, soundness of Trestricted ILWN is analyzed. A simple analysis
approach is given and the inheritable conditions of soundness are obtained.
Theorem 1 shows that an ILWN composed of two LWNs will preserve soundness if
some conditions are satisfied.
Table 1: 
Symbols and abbreviations 

Corollary 1 and corollary 2 give the constructing algorithm of ILWN composed
of n LWNs to ensure soundness. The use of the methods and techniques is demonstrated
by analyzing the example of an auto gas station system.
Further research work is to study synthesis and propertypreservation of other subclasses of ILWN and LPN.
For clarity of symbols, some symbols and abbreviations are listed in Table 1.
ACKNOWLEDGMENTS
This research is supported in part by the National Natural Science Foundation of China under Grants 60773034, 90818023, 90718012 and 60803032; the Taishan Scholar Construction Project of Shandong Province, China; the Scientific and Technological Developing Program of Shandong Province of China under Grant 2008GG30001024 and the Open Project of the State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences under Grant SYSKF0804; the Research Project of SUST Spring Bud in Shandong University of Science and Technology in 2009 and the Graduate Innovation Fund of Shandong University of Science and Technology.