Finite Basis for CCS

After a long sabbatical from conference submission (at least by the standards of present day Computer Science), I have two papers accepted at ICALP'06 in Venice. I have already reported on one of them on this diary. The other paper, entitled A Finite Equational Base for CCS with Left Merge and Communication Merge is joint work with Wan Fokkink, Anna Ingólfsdóttir and Bas Luttik, and the full version is available as a BRICS report. In that paper, we provide a complete equational axiomatization of bisimulation equivalence over the relabelling-, restriction- and recursion-free fragment of CCS, enriched with the left and communication merge operators proposed by Jan Bergstra and Jan Willem Klop. The axiomatization is complete in the sense of classic universal algebra---that is, it can prove all of the valid equations, whose terms may contain variables---and consists mostly of standard equations that had been considered in previous related work. The proof strategy is also based on the classic approach based on normal forms. However, the devil and the pudding are in the details that need to be worked out in order to make the general proof strategy "work" in the specific setting. A lot of care needs to be taken in defining a suitable notion of distinguishing substitution, and in proving that our hunches do work.

I find this result satisfying, and look forward to hearing Bas's ICALP talk based on it. Once again, thanks a lot to my co-authors for a very pleasant and instructive collaboration.