Milner Session at CONCUR 2010

During CONCUR 2010, the concurrency-theory community paid a small tribute to Robin Milner by dedicating a session of its flagship conference to him. The so-called Milner Session was held on Wednesday, 1 September, from 2pm till 4pm. It consisted of a talk by Jos Baeten and of three presentations of papers that were selected for the conference by the PC.

Jos kicked off the session with a talk devoted to Milner's contributions to concurrency theory. He focused on his seminal Calculus of Communicating Systems, providing an overview of its syntax, of some of the design decisions Milner made in that calculus and of its semantics. The presentation by Jos was followed by a short discussion, with remarks from Ugo Montanari, Kohei Honda and myself, amongst others.

My two readers might be interested in reading a short note  by Samson Ambramsky entitled Robin Milner's Work on Concurrency that was published yesterday in the Proceedings of MFPS 2010. According to Samson,

Robin’s ideas have become part of the air we breathe in our scientific community.....

CCS was not just a new calculus, but a new paradigm — that has played a central role in the subsequent development of our subject. It opened up the world of compositional behavioural modelling.

I have always found that one of the red threads in Milner's work was the, I believe novel, emphasis on behavioural semantics and on his standpoint that a process is an equivalence class of process descriptions (be they terms in a process algebra/calculus or states in a labelled transition system/automaton) modulo some notion of behavioural equivalence. Milner himself reiterated this point in several of his writings/talks, and I am glad to see this mentioned in Samson's piece.

We knew what functions were already! But what are processes? CCS established the fundamental methodological point of studying them through their observational behaviour (defined in terms of labelled transition systems via SOS).

This led inexorably in turn to notions of observational equivalence.

Thanks to Jos and Samson for their tributes to Milner's work.

Amongst the contributed talks in the Milner Session, let me mention the excellent talk by Edsko de Vries, who presented joint work with Vasileios Koutavas and Matthew Hennessy on Communicating Transactions. Communicating transactions are obtained by dropping the isolation requirement from standard transactions and can be used to model automatic error recovery in distributed systems. Edsko presented a behavioural theory for a version of CCS with communicating transactions that  is sound and complete with respect to the may-testing preorder. The technical work looked really impressive.

I really enjoyed Silvia Crafa's talk entitled A Logic for True Concurrency, which presented joint work with Paolo Baldan. Perhaps, I was biased since Silvia's talk brought me back in time some twenty years, when a different version of myself was working on topics related to true concurrency. However, I was not the only one to be impressed by that paper, which proposes a logic for true concurrency whose formulae describe events in computations and their causal dependencies. The induced logical equivalence is hereditary history preserving bisimilarity. The authors also identify fragments of the logic that capture other truly concurrent behavioural equivalences in the literature: step, pomset and history preserving bisimilarity. After Silvia's talk, I felt that her paper with Paolo should have been written long ago.