Information Technology Reference
In-Depth Information
labeled transitions with a grammatical term. The description of models is done by
defining the set of states made up of the terms of the grammar and a relation of
transition
between these terms. The actions are the
a
elements of set
A
.Let
P
,
P
,
Q
and
Q
be terms of the grammar and
a
,
a
1
and
a
2
actions of set
A
.
→
P
a
→ Q
reads:
P
has a transition by
a
leading to
Q
, and signifies that in the
behavior of
P
we observe action
a
and that the later behavior corresponds to that of
Q
. The transition system of a term of the grammar is obtained by a structural induction
according to the style of [PLO 81] by the means of rules of the form:
Premises
Conclusion
.
We present the semantic rules of the following operators:
- The stop
δ
is a term that expresses the state of arrest. It corresponds to the STOP
process of the CCS algebra [MIL 80]. It is a state from which no action is possible.
- The prefixing operator; is an operator borrowed from CCS. A state
corresponding to the term
a
;
P
can carry out a transition by executing the action
a
and passing to the state corresponding to the term
P
.
- The choice operator [] is an operator of CCS and Lotos. There are two transition
rules for this operator: one rule to define the composition on the left; and another
to define the composition on the right. If a transition is possible from a state
corresponding to the term
P
(resp.
Q
) to go to the other corresponding to the term
P
(resp.
Q
), then in the composed system corresponding to the term
P
[]
Q
,thesame
transition remains possible and moves the system to the state corresponding to the
term
P
(resp.
Q
).
P −−→ P
P
[]
Q
a
Q −−→ Q
P
[]
Q
a
−−→ P
−−→ Q
is an operator borrowed from Lotos. The rules of this
operator express the behavior of the sequencing of two terms
P
followed by
Q
.The
two rules express the fact that
P Q
behaves like
P
until it reaches the end of its
execution then it will behave like
Q
:
- The sequence operator
a
−−→ P
and
P
a
−−→ P
and
P
=
δ
P Q
a
P
=
δ
P
P Q
a
−−→ P
Q
−−→ Q
is an operator borrowed from Lotos. The rules of this
operator express the parallel interleaving behavior by two terms. If, from the state
P
,
the system transits by
a
to
P
, then the state composed of
P |||Q
transits by
a
to the
state composed of
P
|||Q
. Similarly, if from state
Q
the system transits by
a
to the
- The interleaved operator
|||