A graphical composition theorem for networks of LOTOS processes

An overview of some LOTOS (Language of Temporal Ordering Specification) constructs for expressing the behavior of distributed and concurrent systems is given. Some existing equivalence laws for LOTOS behavior expressions that involve the parallel composition operator and that are based on the notion of bisimulation equivalence are recalled. The graphical representation of the parallel composition of several LOTOS processes as a network of interconnected boxes is ambiguous. However, under sufficiently general conditions such graphical representation is sound; a method for deriving from any such graph a family of strongly equivalent LOTOS expressions that describe the intended process composition is introduced and proved correct. The method legitimizes the adoption of a graphical (or an equivalent textual) shorthand for such multiple compositions. It can be used for transforming the structure of parallel LOTOS expressions, and it is a generalization of previously known algebraic laws.