Analysis and Composition of Partially-Compatible Web Services - Business and Scientific Workflows - page 87

Theorem 4.1 claims that CRG is equivalent to the reduced state
space generated using the set of mediation transitions as stubborn sets.
Because we are only interested in terminal states in the state space, the
reduced state space preserves all relevant properties. In other words,
CRG is well formed if the two services can be composed with the help
of a mediator.

Proof of Theorem 4.1. ) We are to prove that if Gð N 1 ; N 2 ; I Þ is

well formed, a mediator that conforms to I exists. Note that in

Section 4.4, we will give the method to derive a mediator based on the
information from a well-formed CRG, and denote the mediator as
M ¼ð

M

.
When we build the reachability graph of N 1

P m ; T m ; F m Þ

M

P C2 N 2 (denoted P C1

Gð N 1 M P C2 N 2 Þ ), if we use the stubborn set defined in the follow- P C1

ing equation,

T 1 t m g; when 9 t m 2 T m ; t m is enabled at m

Sð m Þ¼ (4.1)

[ [ ;

T 2 T m otherwise

we obtain a reduced reachability graph of Gð N 1 P C1 M P C2 N 2 Þ ,

denoted G R ð N 1 P C1 M P C2 N 2 Þ .

is explained as follows. When there is a
mediation transition enabled, choose it as the single enabled transition
in the stubborn set at marking m. If there are multiple mediation
transitions enabled, choose any one of them as the single enabled
transition in the stubborn set. When there is no mediation transition
enabled,

The meaning of function S

the stubborn set equals to the set of all transitions in

N 1 M P C2 N 2 . By this means, we obtain a subgraph of P C1

Gð N 1 .

According to Lemmas 4.1 and 4.2,

M P C2 N 2 Þ P C1

G ð N 1 M P C2 N 2 Þ contains R P C1

all terminal markings and one infinite path if there is one in

Gð . Because the verification of well-formedness

only involves the terminal markings,

N 1 M P C2 N 2 Þ P C1

G ð M Þ

preserves
all the information we require. On the other hand, it is easy to see
Gð

N 1 P C2 N 2 R P C1

N 1 ; N 2 ; I Þ is equivalent to G R ð N 1 P C1 M P C2 N 2 Þ with respect to

marking M 0 (M 0 ¼

M 1 M 2 ). Hence, if Gð N 1 ; N 2 ; I Þ is well formed,

G R ð N 1 P C1 M P C2 N 2 Þ is also well-formed, and ultimately,

Gð N 1 P C1 M P C2 N 2 Þ is well-formed. Therefore, we conclude that M

serves as a mediator to make N 1 compatible with N 2 .