16 March 2004Split-2 Bisimilarity May be Equationally Easier then Standard Bisimilarity
I may be the only dinosaur left treading this planet, but I am still fascinated by the study of equational characterizations of the parallel composition operation modulo (variations on) the classic notion of bisimulation equivalence. In particular, I am spending some time on the study of axiomatizations for parallel composition that use auxiliary operators, aiming at showing that the left and communication merge operators of Bergstra and Klop have somehow a canonical status in the finite equational axiomatization of parallel composition.
Last November, Wan Fokkink, Anna Ingólfsdóttir, Bas Luttik and I produced the paper CCS with Hennessy's Merge has no Finite Equational Axiomatization in which we showed that the language obtained by adding Hennessy's merge operator from the paper "Axiomatising finite concurrent processes" (SIAM J. Comput. 17 (1988), no. 5, 997-1017) to CCS does not afford a finite equational axiomatization modulo bisimulation equivalence. This is due to the fact that, in strong bisimulation semantics, no finite collection of equations can express the interplay between interleaving and communication that underlies the semantics of Hennessy's merge.
A natural question to ask, at least for us, was whether the same negative result holds true for "reasonable congruences" (in the sense of Moller) finer than standard bisimulation equivalence. The paper Split-2 Bisimilarity has a Finite Axiomatization over CCS with Hennessy's Merge shows that Hennessy's merge suffices to give a finite equational characterization of parallel composition with respect to non-interleaving equivalences. So parallel composition can be finitely axiomatized using a single auxiliary binary operator with respect to non-interleaving equivalences like split-2 and ST-bisimulation semantics. (We conjecture that this is not possible in standard bisimulation semantics.)
Is this surprising? I don't know, but I, for one, did not expect that we would obtain this positive result. We were looking for a proof of a negative result, and when we got stuck we realized we had a positive result staring at us. That's the way things go sometimes.
Working on the problem also brought back memories of my PhD work, in which split and ST-semantics played a major role, and so did some of the techniques that were brought to bear on the proof of the main result in Split-2 Bisimilarity has a Finite Axiomatization over CCS with Hennessy's Merge. No matter how small that result is, it was good to work on those topics again.
I may have something to say about the importance of "proof techniques", and "technique" in general, in a later posting.
Last modified: Tuesday, 16-Mar-2004 18:55:41 CET.