CCS with Hennessy's Merge has no Finite Equational Axiomatization
Luca Aceto
November 2003 |
Abstract:
This paper confirms a conjecture of Bergstra and Klop's from
1984 by establishing that the process algebra obtained by adding an auxiliary
operator proposed by Hennessy in 1981 to the recursion free fragment of
Milner's Calculus of Communicationg Systems is not finitely based modulo
bisimulation equivalence. Thus Hennessy's merge cannot replace the left merge
and communication merge operators proposed by Bergstra and Klop, at least if
a finite axiomatization of parallel composition is desired
Available as PostScript, PDF, DVI. |