Axiomatizing Restriction and Relabelling

Time flies somehow. At some point in late February I posted the following paper:

Luca Aceto, Anna Ingolfsdottir, Bas Luttik and Paul van Tilburg. Finite Equational Bases for Fragments of CCS with Restriction and Relabelling. Technical Report CSR-08-08, TU/Eindhoven, February 2008.

I meant to write a blog entry on the paper then, but that intention has not materialized until now.

So what is the above study about? We investigate the equational theory of several fragments of Milner's CCS modulo (strong) bisimilarity with special attention to restriction and relabelling. The largest fragment we consider includes action prefixing, choice, parallel composition without communication, restriction and relabelling. We present a finite equational base (i.e., a finite ground-complete and omega-complete axiomatisation) for it, including the left merge from ACP as auxiliary operation to facilitate the axiomatisation of parallel composition.

Perhaps surprisingly, no complete axiomatisations of bisimilarity over languages including restriction and relabelling have been given to date. In a classic paper, Milner studied an algebra of flowgraphs with operations of (parallel) composition, restriction and relabelling, and provided a complete axiomatisation for it. In that reference, however, the notion of equivalence between expressions is purely “structural”, since two expressions are equated when they denote the same flowgraph up to isomorphism.

I hope that some of you will find the paper worth looking at. I enjoyed working on it a lot, thanks to my co-authors.