Information Technology Reference
In-Depth Information
Theorem 5.1.
Let
W
i
=(
P
i
,
T
i
;
F
i
,
M
0
i
,
P
fi
) (
i
{1, 2, 3…
k
}) be the WF-net of a
workflow process and
W
CW
=(
P
,
T
;
F
,
M
0
,
P
f
) is their corresponding cross-organization
workflow net with task synchronization pattern. We have
L
(
W
CW
)=
∈
ʘ
1≤
i
≤
k
L
(
W
i
).
Proof.
Let
M
f
ↆ
R
(
M
0
), and
∀
M
∈
M
f
such that
∀
p
∈
P
−
P
f
,
M
(
p
)=0,
M
fi
= {
ʓ
Pi
|
M
∈
M
f
},
P
ₒ
L
(
W
CW
)={
M
f
)}.
Next, we prove this theorem by induction on |
ʴ
|
ʴ∈
T
*
∧
M
0
[
ʴ
>
M
∧
(
M
∈
ʴ
|.
(1) If |
ʴ
|=1,
ʴ
i
=
ʠ
T
ₒ
Ti
(
ʴ
)=
ʴ
if
ʴ∈
T
i
and
ʴ
i
=
ʠ
T
ₒ
Ti
(
ʴ
)=
ʵ
otherwise, (
i
∈
{1, 2, 3…
k
}).
With
ʴ∈
L
(
W
CW
) iff
M
0
[
ʴ
>
M
1
∧
M
1
∈
M
f
, and iff (
ʓ
Pi
(
M
0
)[
ʴ
i
>
ʓ
Pi
(
M
1
))
∧
P
ₒ
P
ₒ
(
ʓ
P
ₒ
Pi
(
M
1
)
{1, 2, 3…
k
}).
(2) Suppose the conclusion is correct when|
∈
M
fi
),
ʴ
i
∈
L
(
W
i
) (
i
∈
ʴ
|=
n
. In the following, we prove that
the conclusion is also correct when|
ʴ
|=
n
+1.
Let
ʴ
=
ʴ′•
t
′
, where
t
′
is the (
n
+1)
th
element of
ʴ
and |
ʴ′
|=
n
.
Based on
ʴ∈
L
(
W
CW
) iff (
M
0
[
ʴ′•
t
′
>
M
n
+1
)
∧
(
M
n
+1
∈
M
f
),
M
0
[
ʴ′
>
M
n
[
t
′
>
M
n
+1
iff
M
n
ↆ
R
(
M
0
); and
M
f
′
={
M
n
|(
M
0
[
ʴ′
>
M
n
[
t
′
>
M
n
+1
)
∧
(
M
n
+1
∈
M
f
)},
M
fi
′
={
ʔ
P
ₒ
Pi
M
n
|
M
n
∈
M
f
′
} (
i
∈
{1, 2, 3…
k
}).
According to the supposition,
∃ʴ
′
=
ʠ
Ti
(
ʴ′
) and
ʴ
′∈
L
(
W
i
) such that
i
T
ₒ
i
ʴ
i
=
ʠ
T
ₒ
Ti
(
ʴ
)=
ʴ′•
t
′
if
t
′∈
T
i
and
ʴ
i
=
ʠ
T
ₒ
Ti
(
ʴ
)=
ʴ′
otherwise; and
ʴ
i
∈
L
(
W
i
) iff
M
0
i
[
ʴ
i
′
>
M
i
′
∧
M
i
′∈
M
fi
′
; iff
M
0
i
[
ʴ
i
>
M
(
n
+1)
i
∧
M
(
n
+1)
i
∈
M
fi
, such that
ʴ
i
∈
L
(
W
i
) and
ʴ
i
=
ʠ
T
ₒ
Ti
(
ʴ
).
Therefore, the theorem is proved.
According to Theorem 5.1, we know that
L
(
W
CW
)=
k
L
(
W
i
) is the language ex-
pression of the cross-organization workflow with task synchronization pattern if the
language expression
L
(
W
i
) (
i
ʘ
1
≤
i
≤
{1, 2, 3…
k
}) of each WF-net can be obtained.
Take the CWF-net of the medical diagnosis cross-organization workflow with syn-
chronous collaboration patterns in Fig. 3 as an example, its language behaviors can be
obtained with the above-mentioned approach. Assume that its end place set is defined
as
P
f
={
O
1
,
O
2
}. Then the behavior description of the
W
CW
in Fig. 3 can be obtained
with the following steps:
(1) The language expression of
W
S
and
W
C
as shown in Figs. 1-2 are easy to
present, which are formally expressed as
L
(
W
S
)=
t
1
t
2
t
3
t
4
(
t
6
//
t
5
t
9
t
10
)
t
12
and
L
(
W
C
)=
t
7
t
8
t
9
t
10
t
11
; and
(2) Based on the Theorem 5.1, the behaviors for the cross-organization medical di-
agnosis workflow with task synchronization pattern in Fig. 3 can be expressed as
L
(
W
CW
)=
L
(
W
S
)
∈
ʘ
L
(
W
C
), i.e.
L
(
W
CW
)= (
t
1
t
2
t
3
t
4
(
t
6
//
t
5
t
9
t
10
)
t
12
)
ʘ
(
t
7
t
8
t
9
t
10
t
11
).
6
Conclusion and Future Work
This paper presents the behavior description approach for a kind cross-organizational
workflow with task synchronization pattern using Petri net language, which mainly
includes the following three steps: (1) modeling the cross-organizational workflow
with task synchronization pattern, we present the CWF-net by extending traditional
WF-net; (2) obtaining the behavior expressions of WF-net for each organization; and
(3) obtaining the behavior description of the CWF-net using the synchronized shuffle
operation of Petri net language.
