Opening the PDF files on this page may require you to download Adobe Reader or an equivalent viewer (GhostScript).

Contents

LOTOS

LOTOS::="ISO Standard language that combines CSP/CCS with algebraic ADT to describe telecommunication systems", [ lotos-synt.pdf ] (LOTOS Vade Mecum) [ index.php?topic=Lotos ] [ http://www.cs.stir.ac.uk/~kjt/research/well/ ] [ lookup?from=methods&search=LOTOS ]
Formal Definition of LOTOS in MATHS
Please Fix [click here LOTOS if you can fill this hole]
LOTOS::=following
Net
1. Process::Sets.
2. Action::Sets.
  P,Q,R,S:Process.
  a,b,c,d:Action.
  A,B:@Action.
3. P-a->Q::@=P can be observed executing action a and then behaving like Q.
4. STOP::Process, takes part in no actions.
5. |- (LOTOS_stop): for no a:Action, P:Process( STOP-a->P).
6. δ::Action=observable termination of a Process.
7. EXIT::Process, a process that always leads to an observable termination.
8. |- (LOTOS_exit1): EXIT -δ->STOP.
9. |- (LOTOS_exit2): for no a:Action~δ, P:Process( EXIT-a->P).
10. Process Descriptions
11. a;P::Process= a prefix P. P[>Q::Process=P disabled by Q.
12. P|A|Q::Process=`P and Q synchonizing on A".
  Structural Operational Semantics
13. |- (LOTOS_a2): a;P-a->P
  Rules
14. |- (LOTOS_r1): P[>Q-a->R[>Q :- a<>δ, P-a->R.
15. |- (LOTOS_r2): P[>Q-δ->R :- P-δ->R.
16. |- (LOTOS_r3): P[>Q-a->R :- Q-a->R.
17. |- (LOTOS_r4): P|A|Q-a->R|A|Q :- a not_in A| δ, P-a->R.
18. |- (LOTOS_r5): P|A|Q-a->P|A|R :- a not_in A | δ, Q-a->R
19. |- (LOTOS_r6): P|A|Q-a->R|A|S :- a in A | δ, a=b, P-a->R, Q-b->S.
  
  LOTOS example
  1. Proc::= Pdcc |ctrlc| Edcc.
  2. Pdcc::= Ping[>CtrlC.
  3. Ping::=ping; EXIT.
  4. CtrlC::=ctrlc; EXIT.
  5. Edcc::=EXIT[>CtrlC.
    then can show
  6. (above)|-Ping-ping->EXIT.
  7. (above)|-Pdcc-ping->EXIT[>CtrlC
  8. (above)|-Proc-ping->(EXIT[>CtrlC)[ctrlc]Edcc.
  . . . . . . . . . ( end of section LOTOS example) <<Contents | End>>
(End of Net LOTOS)

. . . . . . . . . ( end of section LOTOS) <<Contents | End>>

End