Split-2 bisimilarity has a finite axiomatization over CCS with Hennessy's merge

L. Aceto, W.J. Fokkink, A. Ingólfsdóttir, B. Luttik

Research output: Book/ReportReportAcademic

82 Downloads (Pure)


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.
Original languageEnglish
Place of PublicationAarhus
PublisherBRICS, University of Aarhus
Number of pages16
Publication statusPublished - 2004

Publication series

NameBRICS Report Series
ISSN (Print)0909-0878

Fingerprint Dive into the research topics of 'Split-2 bisimilarity has a finite axiomatization over CCS with Hennessy's merge'. Together they form a unique fingerprint.

Cite this