The Equational Theory of Timed CCS

A couple of weeks ago, I posted a paper on my recent publications page presenting some negative results on the equational theory of Wang Yi's Timed CCS (TCCS) modulo timed bisimilarity. The paper, Impossibility Results for the Equational Theory of Timed CCS, is coauthored with Anna Ingolfsdottir and MohammadReza Mousavi. (So my Mousavi number is now 1.)

The aim of the paper is to revisit the study of the equational theory of parallel composition in TCCS by obtaining results in the spirit of those that Faron Moller showed for Milner's CCS. We prove that timed bisimilarity is not finitely based over TCCS. Moreover, unlike in the setting of CCS, adding two "natural" variations on the (timed) left-merge operator to TCCS does not yield a finitely axiomatizable theory.

In passing, we sharpen the so-called Gap Theorem of J.-C. Godskesen and Kim G. Larsen by showing that it holds also in the setting when the set of actions is a singleton. Unlike the proof of the original result by those authors, which goes via a translation to timed automata, ours is entirely process algebraic.

Thanks to Anna and Mohammad for a pleasant, instructive and humbling collaboration. I, for one, am always overawed by the fragility of these results. One has to be very careful in making sure that the technical details work. An apparently innocuous change in the semantics of the operators can make a huge difference in their properties, and thus in the validity of the statements one is trying to prove. Our ICE-TCS seminar speaker yesterday, Freyja Hreinsdóttir, quoted a mathematician as referring to a conjecture as being "obviously true, but unproven". I am afraid that I do not trust those statements. For what it is worth, my "obviously true, but unproven" conjectures turn out to be false more often than not :-(.