Information Technology Reference
In-Depth Information
This means that the sender
is not delayed if the receiver is unready at the
time of sending. The subsequent actions of the sender proceed in parallel with
the journey undertaken by its message. A calculus with such a reduction rule
is called
asynchronous
, and output prexing is usually omitted from its syntax.
That is why the algebraic laws for an asynchronous calculus are dierent from
those of a synchronous one.
Structural laws are also used in addition to reductions to formalise the in-
tended meaning of the constructions of the language. For example, the repetition
operator (!
P
P
) denotes an unbounded set of parallel instances of the same process
P
. The addition of a new instance of
P
therefore makes no dierence, as stated
in the unfolding law
!
P
=
P j
(!
P
)
This law can be applied any number of times
P j
(!
P
)=
PjPj
(!
P
)=
:::
If each application allows a reduction, we can generate an innite reduction
sequence leading to potential non-termination. Consider for example the process
P
that reduces in one step to the empty process
P
=
df
(
e:
0
j e:
0
)
!
(
0
j
0
)=
0
This can be put into a repetition
!
P
=(
e:
0
j e:
0
)
j
!
P !
0
j
!
P
=!
P
It follows that !
can be subjected to an innite series of reductions, without
ever engaging in a useful interaction with its environment. This is just what is
known as divergence or livelock, and it is clearly and obviously denable on the
basis of an operational semantics. A top-down presentation cannot give such an
obviously appropriate
denition
of non-termination, and has to postulate that
the articial variable
!
P
is mysteriously allowed to take the value
false
whenever
there is a risk of divergence.
Another useful denition in operational semantics is that of a labelled tran-
sition, in which the transition relation
ok
is labelled by a trace of interactions
with the environment that can occur during the evolution of the process.
!
<>
−! Q
P ! Q
P
=
df
<e>
b
s
!e:P
0
^ P
0
s
9 P
0
:P
P
−! Q
=
df
! Q
where
!
. Now we can trace the evolution
of our vending machine, using a few structural laws which seem reasonable
is the reflexive transitive closure of
!
Search WWH ::
Custom Search