Complete set of axioms for finite basic LOTOS behavioural equivalences

In this paper we provide complete sets of axioms which characterize observational congruence and testing congruence for finite basic LOTOS behaviours. Actually, we prove something stronger which allow us to extend our result to other behavioural equivalences. In fact, we provide a set of laws, which will be referred to as Basic Axioms, that we show to be sound with respect to strong bisimulation. Then, we prove that these laws allow one to rewrite any finite basic LOTOS behaviour into a strong equivalent one containing only the action, choice and stop operators, i.e. a term over the signature ??basic = {; , [],stop}. Since strong bisimulation is the most discriminating congruence in a set which includes observational, branching, trace and testing congruences [8, 7,3], rewriting with Basic Axioms preserves all these equivalences. The last step, in order to derive the corresponding complete set of axioms for finite basic LOTOS, consists of showing that ??basic and ??Simple_CCS (with their operational semantics) are isomorphic. Thus we can obtain various complete axiomatisations for T???basic (and then for the whole finite basic LOTOS) by simply rephrasing those existing for Simple CCS into the signature ??basic.