Complete sets of axioms for finite basic LOTOS behavioural equivalences

LOTOS is a specification language which has been developed within the International Oroanization for Standardization (ISO) and standardized as a formalism for specifying concurrent systems, specially suited to run on Open System Interconnection (OSI) computer network architecture. Like all process algebras, LOTOS can be used to describe concurrent systems at different levels of abstraction. The semantics of LOTOS is defined in terms of labelled transition systems, according to the Structural Operational Semantics (SOS) approach. Transition systems are then factorized through the notions of observational equivalence and testing preorders, which permit proving that two different LOTOS specifications are equivalent when "uninteresting" details are ignored and that a low level specification is a satisfactory implementation of a more abstract one.