ON AXIOMATISING FINITE CONCURRENT PROCESSES

In his pioneering paper [Axiomatising finite concurrent processes, SIA M J. Comput., 17 (1988), pp. 997-1017], Hennessy gave complete axiomat izations of Milner's observational congruence and of t-observational c ongruence which made use of an auxiliary operation to axiomatize paral lel composition. Unfortunately, those axiomatizations tum out to be fl awed due to the subtle interplay between Hennessy's auxiliary parallel operator and synchronization. The aim of this paper is to present cor rect versions of the equational characterizations given in Hennessy's paper. Some of the problems which arise in giving operational semantic s to the auxiliary operators used by Bergstra and Klop and Hennessy in the theory of congruences like Milner's observational congruence are also discussed.