"Axiomatisations of Weak Equivalences for De Simone Languages",
Extended abstract in the Proceedings of the 6th Conference on Concurrency Theory CONCUR'95, Philadelphia, 1995. Springer, LNCS 962.
Aceto, Bloom and Vaandrager proposed in [ABV92] a procedure for generating a complete axiomatisation of strong bisimulation for process languages in the GSOS format. However, the choice operator +, which the procedure uses, as well as other auxiliary GSOS operators, which it introduces to obtain a finite axiomatisation, do not preserve many of weak equivalences.
We propose a modification of this procedure, which works for a subclass of process languages in the De Simone format with a special treatment of silent actions. A choice of such a subclass of process languages guarantees that all the considered and auxiliary operators preserve many of weak equivalences. Our procedure generates a complete axiomatisation of refusal simulation preorder and it can be easily adapted to coarser preorders. The completeness result depends on the completeness result for the basic process language, which we prove. This language does not use prefixing with tau and the choice operator +. Instead, we employ the CSP external and internal choice operators as well as the third choice operator.This paper is available in dvi form.