Model checking for LOTOS

In this paper we present a prototypal environment to analyse LOTOS specifications, based on the integration between Squiggles, an equivalence verifier, and EMC, a model cheker for CTL formulae. Hence, the functionalities of our environment range from the reduction of a finite state LOTOS specification into its corresponding Labelled Transition System, possibly minimized with respect to an equivalence relation, to the verification of equivalence between specifications and to the check of validity of properties expressed in a temporal logic as CTL.