Abstract:

Our proposal deals with the algebraic study of a temporal extension of Basic LOTOS, and addresses in particular issues related to the definition of strong and weak bisimulation and the collection of equations associated with them. ET-LOTOS represents the basic model, for which we investigate the strong bisimulation and propose some equations to strengthen the collection given by Leduc and Leonard. We also define the observational equivalence which preserves choice, establish the condition for which it is a congruence and characterise this equivalence by a set of equations.