The
International Conference on Concurrency Theory (CONCUR) and the I
FIP 1.8 Working Group on Concurrency Theory are happy to announce the first edition of the CONCUR
Test-of-Time Award. The purpose of the award is to recognize important
achievements in Concurrency Theory that were published at the CONCUR
conference and have stood the test of time. All papers published in
CONCUR between 1990 and 1995 were eligible.
The award winners for the CONCUR ToT Awards 2020 may be found
here, together with the citations for the awars. They were selected by a jury composed of Jos Baeten, Patricia
Bouyer-Decitre, Holger Hermanns, Alexandra Silva and myself.
This post is the first of a series in which I interview the recipients of the CONCUR ToT Awards 2020. I asked
Davide Sangiorgi (University of Bologna, Italy) a small number of questions via email and I report his answers below in a slightly edited form. Let me thank Davide for his willingness to take part in an interview and for his inspiring answers, which I hope will be of interest to readers of this blog and will inspire young researchers to take up work on Concurrency Theory.
In what follows, LA stands for Luca Aceto and DS for Davide Sangiorgi.
LA: You receive one of the two CONCUR ToT Awards for the period 1992-1995 for your paper "
A Theory of Bisimulation for the pi-Calculus", presented at CONCUR 1993. Could you tell us briefly what spurred you to develop open bisimilarity and how the ideas underlying that notion came about?
DS: I developed the paper on open bisimulation during 1992 and 1993. I was in Robin Milner's group, in Edinburgh. We were studying and questioning basic aspects of the theory of the
pi-calculus. One such aspect was the definition of equality on processes; thus a very fundamental aspect, underlying the whole theory. The equality had to be a form of bisimulation, in the same way as it was for CCS. The two forms of bisimilarity that were around for the pi-calculus, late and early bisimilarity, are not congruence relations. In both cases, the input clause of bisimilarity uses a universal quantification on the possible instantiations of the bound name. As a consequence, neither bisimilarity is preserved by the input prefix (forbidding substitutions in the input clause would make things worse, as congruence would fail for parallel composition). Therefore, one has to introduce separately the induced congruence, by universally quantifying the bisimilarities over all name substitutions. In other words, the two bisimilarities are not fully substitutive ('equal' terms cannot be replaced, one for the other, in an arbitrary context). On the other hand, the congruences induced by the bisimilarities are not themselves bisimilarities. Hence in this case 'equal' terms, after some actions, need not be 'equal' anymore. Thus, for instance, such relations do not support dynamic modifications of the context surrounding related terms.
This situation was not fully satisfactory. The same could be said for the algebraic theory: there were proof systems for the two bisimilarities (of course, on finitary processes) but, because of the above congruence issue, there were no axiomatisations. (In those years I was also working with Joachim Parrow on axiomatisations of these relations.)
The universal quantification on substitutions in the input clause of the bisimilarites and in the definitions of the induced congruences was also unsatisfactory because it could make checking equalities cumbersome.
All these were motivations for looking at possible variations of the definition of bisimulation. The specific hints towards open bisimulation came from thinking at two key facets of the pi-calculus model that were somehow neglected in the definitions of early and late bisimilarities. The first facet has to do with the pi-calculus rejection of the separation between channels and variables (`channel' here meaning a 'constant identifier'). In the pi-calculus ,there is only one syntactic category, that of
names, with no formal distinction between channels and variables. This contributes to the elegance of the model and its theory. However, both in early and in late bisimilarity, the free names of processes are treated as channels, whereas the bound names of inputs are treated as variables because of their immediate instantiation in the bisimilarity clause. There was somehow a discrepancy between the syntax and the semantics.
The second facet of the pi-calculus that contributed to the definition of open bisimilarity is the lack of the mismatch operator: the pi-calculus, at least in its original proposal, has a match operator to test equality between names, but not the dual mismatch, to test for inequality. Mismatching had been excluded for the preservation of a monotonicity property on transitions, intuitively asserting that substitutions may only increase the action capabilities of a process. (Both facets above represented major differences between the pi-calculus and its closest ancestor----Engberg and Nielsen's Extended CCS.) Thus I started playing with the idea of avoiding the name instantiation in the input clause and, instead, allowing, at any moment, for arbitrary instantiations (i.e., substitutions) of the names of the processes---the latter justified by the above monotonicity property of transitions. By adding the requirement of being a congruence, the definition of open bisimilarity came about.
Still, I was not sure that such a bisimulation could be interesting and robust. Two further developments helped here. One was the axiomatisation (over recursion-free terms). It was a pure axiomatisation, it was simple, and with a completeness proof that leads to the construction of canonical and minimal (in some syntactic sense) representatives for the equivalence classes of the bisimilarity. For other bisimilarities, or related congruences, obtaining canonical representatives seems hard; at best such representatives are parametrised upon a set of free names and even in these cases minimality is not guaranteed.
The other development has to do with a symbolic or "efficient" characterisation of the bisimilarity. The initial definition of open bisimulation makes heavy use of substitutions. In the symbolic characterisation, substitutions are performed only when needed (for instance, the unification of two names
a and
b is required if there is an input at
a and an output at
b that can interact), somehow echoing the call-by-need style of functional languages. Such a characterisation seemed promising for automated or semi-automated verification.
LA: How much of your later work has built on your CONCUR 1993 paper? What results of yours are you most proud of and why?
DS: The most basic idea in open bisimulation is to avoid the instantiation of the bound name of an input, possibly making such a bound name a free name of the derivative term. The use of substitutions, elsewhere in the definition, is necessary to obtain a congruence relation for the pi-calculus. I was surprised to discover, in the following years, that such substitutions are not necessary in two relevant subsets of the pi-calculus. I called the variant of open bisimulation without substitutions
ground bisimulation (I think the name came from Robin). One subset is Honda and
Boudol's Asynchronous pi-calculus, whose main constraint is to make outputs floating particles that do not trigger the activation of a continuation (other limitations concern sum and matching). The other subset is the Internal (or Private) pi-calculus, in which only private (i.e., restricted) names may be transmitted. I designed the Internal pi-calculus with ground bisimilarity in mind. People seem to have found this calculus useful in many ways, partly because of its expressiveness combined with its simple theory (in many aspects similar to that of CCS), partly because it allows one to limit or control aliasing between names, which can be useful for carrying out proofs about behavioural properties of processes, or for designing and reasoning about type systems, or for representing the calculus in logical systems.
Sometimes, the possibility of using ground bisimulation can considerably simplify proofs of equalities of terms. For instance, in my works on comparisons between pi-calculus and lambda-calculus, when I had to translate the latter into the former I have always used one of the above subcalculi (sometimes even combining them, e.g., the Asynchronous Internal pi-calculus), precisely for being able to use ground bisimilarity.
I consider both ground bisimilarity and the Internal pi-calculus spin-offs of the work on open bisimilarity.
While working on open bisimilarity for the pi-calculus, in a different paper, I applied the idea of open bisimilarity to the lambda-calculus. I kept the name 'open' but the bisimulation is really 'ground', as there are no substitutions involved. I remember Robin encouraging me to keep the name 'open' because it conveyed well the idea of setting a bisimulation on open terms, rather than on closed terms as usually done. In open bisimulation for the lambda-calculus, a lambda-abstraction
lambda x. M yields an action with label
lambda x that should be matched (modulo alpha-conversion) by the same action by a bisimilar term. (Of course additional bisimulation clauses are needed when a free variable is found in evaluation position.) In contrast, in the ordinary bisimulation for the lambda-calculus, Abramsky's applicative bisimilarity, the bound variable of an abstraction has to be instantiated with all closed terms, which is heavy. In general, open bisimilarity is finer than applicative bisimilarity and contextual equivalence (the reference equivalence in the lambda-calculus) but they often coincide in examples of concrete interest. Moreover, open bisimilarity does coincide with contextual equivalence in appropriate extensions of the lambda-calculus. In short, open bisimilarity offers us a technique for reasoning on higher-order languages using 'first-order' tools, somehow similarly to what game semantics does.
This line of work about open bisimilarity in higher-order languages has been very fruitful, and is still studied a lot, for various forms of higher-order languages, sometimes under the name of 'normal-form' bisimulation.
LA: In your opinion, what is the most interesting or unexpected use in the literature of the notions and techniques you developed in your award-winning paper?
DS: I mentioned the hope, when working on open bisimilarity, that its symbolic "efficient" characterisation could be useful for automated or semi-automated tools for reasoning about behavioural properties. Shortly after introducing open bisimulation, Björn Victor and Faron Moller, both in Edinburgh at the time, exploited it to design the Mobility Workbench. I also worked on an algorithm and a prototype tool for on-the-fly checking, with Marco Pistore.
However the most surprising applications in this direction have arrived later, when the 'lazy' instantiation of bound names of open bisimilarity has been applied to languages richer than pi-calculus. For instance, Chaki, Rajamani, Rehof have used open similarity in their methods and tools for model checking distributed message-passing software. Others have applied open bisimilarity to languages for security and cryptography, like the spi-calculus and applied pi-calculus. These include S. Brias, U. Nestmann and colleagues at EPFL and Berlin. R. Horne, A. Tiu and colleagues in Singapore and Luxembourg have pushed significantly in this direction, with verification techniques and tools. For instance very recently they have discovered a privacy vulnerability for e-passports.
Similarly, Yuxin Deng and colleagues have applied the idea of open bisimulation to quantum processes, with analogous motivations --- avoiding the universal quantification in the instantiation of variables, algorithmically unfeasible in the quantum setting as quantum states constitute a continuum.
Another line of work that I found interesting and surprising concerns abstract frameworks for concurrency, including logical frameworks. Here forms of open bisimulation are often the 'natural' bisimulation that come up. These frameworks may be based, for instance on coalgebras and category theory (e.g., works by M. Fiore and S. Staton, N. Ghani, K. Yemane, and B. Victor), category theory for reactive systems (e.g., works by F. Bonchi, B. König and U. Montanari), nominal SOS rule formats (e.g., works by M. Cimini, M. R. Mousavi, and M. A. Reniers), higher-order logic languages (e.g., works by A. Tiu, G. Nadathur, and D. Miller).
There have been works that have pushed the idea of open bisimulation of avoiding the instantiation of bound names in interactions with an external observer one step further: such bound names are not instantiated even in interactions
internal to the processes. The substitutions produced by the interactions are added to the calculus, producing particles sometimes called fusions. This mechanism resembles the explicit substitutions of the lambda-calculus, but it goes beyond that; for instance the addition of fusions leads to modifications of input and output prefixes that produce pleasant syntactic and semantic symmetry properties. Various people have worked on this, including B. Victor, J. Parrow, Y. Fu, C. Laneve, P. Gardner and L. Wischik.
I should also mention the recent work by K. Y. Ahn, R. Horne, and A. Tiu on logical interpretations of open bisimilarity. Remarkably, they explain the difference between the original (late and early) formulations of bisimilarity in the pi-calculus and open bisimilarity as the difference between intuitionistic and classical versions of modal logics.
Apologies for not mentioning everybody!
LA: To your mind, how has the focus of CONCUR changed since its first edition in 1990?
DS: I remember that in the early years of CONCUR there was a tremendous excitement about the conference. A forum for grouping the (fast-growing) community had been long-awaited. In Edinburgh, every year after the conference, the people with an interest in concurrency would meet (multiple times!) and discuss the contents of the proceedings. Several of us every year would attend the conference. Attending the conference was very useful and interesting: one was sure to meet a lot of people, hear about excellent papers, have lively discussions. We would try to go, even without a paper in the proceedings. I vividly remember the 1993 edition, where I presented the paper on open bisimulation. It had been organised by Eike Best in Hildesheim, Germany. It was an enjoyable and exciting week, I met and knew a number of people of our community, and learned a lot. (How sad and unwise that the Computer Science department in Hildesheim, so strong in concurrency at the time, was shut down a few years later.) Over the years, the CONCUR community has kept increasing its size. The conference has substantially broadened its scope, rightly including new emerging topics. Perhaps it is more difficult than in the past to (more or less) understand most of the presented papers, both because of the diversity of the topics and of their technical specialisation. On the other hand, there are now satellite events, covering a number of areas. Hence there are always plenty of interesting presentations and talks to attend (this definitely occurred to me in the last edition, in Amsterdam!). I should also mention here the activity on the IFIP WG 1.8 on Concurrency Theory, currently chaired by Ilaria Castellani, that in many ways supports and promotes CONCUR.
The quality of the papers at CONCUR is still very high. This is very important. As a community we should strive to maintain, and possibly even increase, the excellence and prestige of the conference, first of all, by submitting our best papers to the conference. CONCUR must be a reference conference in Computer Science, which is essential for injecting new people and energy into the community.
Acknowledgements: Many thanks to
Ilaria Castellani, who pointed out a number of typos in the original version of this text.
