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
|||
Search WWH ::




Custom Search