|
Split-2 Bisimilarity has a Finite Axiomatization over CCS with
Hennessy's Merge
Luca Aceto
January 2004 |
Abstract:
This note shows that split-2 bisimulation equivalence (also
known as timed equivalence) affords a finite equational axiomatization over
the process algebra obtained by adding an auxiliary operation proposed by
Hennessy in 1981 to the recursion free fragment of Milner's Calculus of
Communicating Systems. Thus the addition of a single binary operation,
viz. Hennessy's merge, is sufficient for the finite equational axiomatization
of parallel composition modulo this non-interleaving equivalence. This result
is in sharp contrast to a theorem previously obtained by the same authors to
the effect that the same language is not finitely based modulo bisimulation
equivalence.
Available as PostScript, PDF, DVI. |