Information Technology Reference
In-Depth Information
We take
fv
(
M
),
fv
(
patt
(
x ϕ
)),
fv
(
IM
) to be the set of variables appeared
free in
M
,
patt
(
x ϕ
),
IM
. The free variables of process terms are defined as
follows:
fv
(
out
(
newxM
)
.P
)=(
fv
(
P
)
∪
fv
(
M
))
\{
x
}
fv
(
in
(
patt
(
x ϕ
))
.P
)=(
fv
(
P
)
∪
fv
(
patt
(
x ϕ
)))
\{
x, ϕ
}
fv
(
P
|
Q
)=
fv
(
P
)
∪
fv
(
Q
)
fv
(
Id
[
P, IM
]) =
fv
(
P
)
∪
fv
(
IM
)
fv
(
A
|
B
)=
fv
(
A
)
∪
fv
(
B
)
2.3 A Transition Semantics
The semantics of the GSPM is given in terms of a transition relation
.
Similar to the approach in [3], we model the state of the protocol system as
apair
−→
,where
s
records the current environment's message base
EM
(Because the environment has 'seen' the sequence of messages traveling on
the network up to the moment), and
System
is the protocol agent composed
of some agents. An action is a term of the form
Id
[
in
(
M
)](input action) or
Id
[
out
(
M
)](output action), which means a participant
Id
inputs or outputs a
message
M
. The set of actions
s, System
A
∗
A
is ranged over by
α, β,
···
, while the set
of strings of actions is ranged over by
s, s
,
···
. String concatenation operator is
written as '
'. We denote by
act
(
s
)and
msg
(
s
) the set of actions and messages,
respectively, appearing in
s
.Astring
s
is closed if
fv
(
s
) is nil. In what follows,
we write s
·
EM
0
).
We now define paths, sequences of actions that may result from the inter-
action between an agent and its environment. In paths, each message received
by a agent can be synthesized from the knowledge the environment has previ-
ously acquired. A path is a closed string
s
M
for
EM
M
(
EM
=
msg
(
s
)
∪
)
∗
such that for each
s
1
,s
2
and
∈
(
A
Id
[
in
(
M
)], if
s
=
s
1
·
Id
[
in
(
M
)]
·
s
2
,then
s
1
M
.
, is a pair consisting of a path
s
and
a
system
. Configurations are ranged over by
C, C
,
A configuration, written as
s, system
,and
C
0
stands for the
initial configuration. The transition relation on configuration is defined by the
following rules:
···
patt
(
n M
)
EM
(input)
in
(
patt
(
n M
))
−→
s, Id
[
in
(
patt
(
x ϕ
))
.P, IM
]
Id
[
in
(
patt
(
n M
))]
,Id
[
P
[
n/x,
M/ϕ
]
,IM
patt
(
n M
)]
s
·
∪
IM
M
[
n/x
]
(
n
are fresh in
s
)
(output)
out
(
M
[
n/x
])
−→
s, Id
[
out
(
newxM
)
.P, IM
]
s
·
Id
[
out
(
M
[
n/x
])]
,Id
[
P
[
n/x
]
,IM
∪
n
]
α
−→
s
,Id
[
P
,IM
]
s, Id
[
P, IM
]
(internal par)
α
−→
s
,Id
[
P
|
Q, IM
]
s, Id
[
P
|
Q, IM
]
