Split-2 Bisimilarity has a Finite Axiomatization over CCS withbr Hennessy's Merge

摘要

This note shows that split-2 bisimulation equivalence (also known as timedequivalence) affords a finite equational axiomatization over the processalgebra obtained by adding an auxiliary operation proposed by Hennessy in 1981to the recursion, relabelling and restriction free fragment of Milner'sCalculus of Communicating Systems. Thus the addition of a single binaryoperation, viz. Hennessy's merge, is sufficient for the finite equationalaxiomatization of parallel composition modulo this non-interleavingequivalence. This result is in sharp contrast to a theorem previously obtainedby the same authors to the effect that the same language is not finitely basedmodulo bisimulation equivalence.