Information Technology Reference
In-Depth Information
2
BPA Processes and Operational Semantics
Assume a set of variables
V
and a set of actions
Act
, we consider the set of BPA
expressions
E
given by the following syntax; we shall use
E,F,...
as metavari-
ables over
E
.
E
::=
a
(action,
a
∈
Act
)
| X
(variable,
X ∈V
)
|
Σ
i∈I
E
i
(summation,
I
is a finite set)
|
E
1
;
E
2
(sequential composition)
|
μX.E
(recursion,
X
∈V
).
We shall use
fv
(
E
) to stand for the set of variables occurring free (i.e., not
bounded by
μ
)in
E
. We shall write
E
for the result of substituting
F
for each free occurrence of
X
in
E
, renaming bound variables as necessary. BPA
processes are closed BPA expressions, i.e. those
E
{
F/X
}
.Moreover
(bound) variables in BPA processes must be guarded by action prefixing.
∈E
with
fv
(
E
)=
∅
Table 1.
Transition rules
a
−→
act
a
a
−→
a
−→
E
j
α
E
α
sum
seq
j ∈ I
a
−→
a
−→
Σ
i∈I
E
i
α
E
;
F
αF
a
−→
a
−→
E
{
μX.E/X
}
α
E
α
rec
state
a
−→
a
−→
μX.E
α
Eβ
αβ
The operational semantics of processes can be described by a labelled transi-
tion system
S
,Act,
−→
wherethestatespace
S
consists of finite sequences of BPA processes, and the
transition relation
−→ ⊆ S ×
Act
×S
is generated by the rules in Table 1, in which (as also later) we use Greek
letters
α,β,...
as meta variables ranging over elements of
,write
for empty
sequence, write
Eα
forthestatestartingwith
E
andfollowedby
α
,write
αβ
for the state obtained by concatenating the sequences
α
and
β
,write
α
S
a
−→
β
. We will write
α
a
1
...a
n
a
1
−→
a
2
−→
a
n
−→
for (
α, a, β
)
∈−→
−→
β
if
α
α
1
,α
1
...
β
,and
say
β
is reachable from
α
.
Search WWH ::
Custom Search