Open AccessSplit-2 Bisimilarity has a Finite Axiomatization over CCS with Hennessy's Merge
Author(s) -
Luca Aceto,
Willem Jan Fokkink,
Anna Ingólfsdóttir,
Bas Luttik
Publication year - 2004
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v11i1.21826
Subject(s) - modulo , process calculus , bisimulation , mathematics , equivalence (formal languages) , logical equivalence , merge (version control) , recursion (computer science) , pi calculus , discrete mathematics , algebra over a field , pure mathematics , computer science , algorithm , theoretical computer science , information retrieval
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.