Compositional logic semantics and lotos

A branching temporal semantics for a subset of LOTOS is proposed in order to provide a formal tool to verify properties of LOTOS specifications. The semantics is defined using a compositional approach, to provide modularity in the verification process, by which it is possible to associate a CTL * formula to each language construct. The relations between the equivalence defined on LOTOS and the equivalence induced by the temporal semantics have been studied, proving that the compositionality requiremement does not permit to preserve the discriminating power of bisimulation. We succeed however in reaching a weaker equivalence, simulation, which appears to be the strongest one with respect to which it is possible to give a fully abstract compositional semantics using standard temporal logics.