In this study it is proposed a formal semantics for Basic LOTOS (Language
Of Temporal Ordering Specification). The subset of LOTOS, where processes
interact with each other by pure synchronizations, without exchanging
values. In basic LOTOS the expressiveness of all the LOTOS process constructors
(operators) can be appreciated without being distracted by interprocess
value communication. LOTOS is an FDT generally applicable to distributed,
concurrent information processing systems. During the last decade, a lot
of works have been devoted to compilation and verification of LOTOS specifications.
While using extended Petri nets as tool for compile a subset of LOTOS
has already been pointed out. In this research it is proposed to extensively
make use of a specific kind of high level Petri nets: the M-nets. Such
nets, allowing for compositionality, appear particularly well-suited to
give a formal semantics for basic LOTOS.