On the soundness of graphical representations of interconnected processes in LOTOS

The graphical representation of the parallel composition of several LOTOS processes as a network of interconnected boxes is ambiguous, due to the nature of the LOTOS binary parallel operator. However, under suitable and sufficiently general conditions, such graphical representation is sound; a method for deriving from these graphs a family of strongly equivalent LOTOS expressions that describe the intended process composition is introduced and proved correct. The method can be used for transforming the structure of parallel LOTOS expressions, and is a generalization of previously known algebraic transformation laws.