Split-2 Bisimilarity has a Finite Axiomatization over CCS with<br> Hennessy&#39;s Merge

TL;DR

This paper demonstrates that split-2 bisimulation equivalence admits a finite axiomatization over a specific process algebra extended with Hennessy's merge, contrasting with previous non-finite results for bisimulation.

Contribution

It shows that adding Hennessy's merge to CCS allows a finite axiomatization of split-2 bisimulation, unlike standard bisimulation.

Findings

Finite axiomatization achieved with Hennessy's merge

Contrasts with non-finite axiomatization for bisimulation

Highlights the power of auxiliary operations in process algebra

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, relabelling and restriction 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.