Thursday, April 30, 2020

An interview with Rob van Glabbeek, CONCUR Test-of-Time Award recipient

This post is devoted to the third interview with the colleagues who were selected for the first edition of the CONCUR Test-of-Time Award. (See here for the interview with Davide Sangiorgi, and here for the interview with Nancy Lynch and Roberto Segala.) I asked Rob van Glabbeek (Data61, CSIRO, Sydney, Australia) a few questions via email and I am happy share his answers with readers of this blog below. Rob's words brought me back to the time when the CONCUR conference started and our field of concurrency theory was roughly a decade old. I hope that his interesting account and opinions will inspire young researchers in concurrency theory of all ages.

Luca: You receive one of the two CONCUR ToT Awards for the period 1990-1993 for your companion papers on "The Linear Time-Branching Time Spectrum", published at CONCUR 1990 and 1993. Could you tell us briefly what spurred you to embark in the encyclopaedic study of process semantics you developed in those two papers and what were your main sources of inspiration?

Rob: My PhD supervisors, Jan Willem Klop and Jan Bergstra, were examining
bisimulation semantics, but also failures semantics, in collaboration
with Ernst-Ruediger Olderog, and at some point, together with Jos Baeten,
wrote a paper on ready-trace semantics to deal with a priority operator.
I had a need to see these activities, and also those of Tony Hoare and
Robin Milner, as revealing different aspects of the same greater whole,
rather than as isolated research efforts. This led naturally to an
abstraction of their work in which the crucial difference was the semantic
equivalence employed. Ordering these semantics in a lattice was never
optional for me, but necessary to see the larger picture.  It may be in
my nature to relate different solutions to similar problems I encounter
by placing them in lattices.

Luca: Did you imagine at the time that the papers on "The Linear Time-Branching Time Spectrum" would have so much impact?

Rob: I didn't think much about impact in those days. I wrote the papers
because I felt the need to do so, and given that, could just as well
publish them. Had I made an estimate, I would have guessed that my
papers would have impact, as I imagined that things that I find
necessary to know would interest some others too. But I would have
underestimated the amount of impact, in part because I had grossly
underestimated the size of the research community eventually working
on related matters.

Luca: In your papers, you present characterizations of process semantics in relational form, via testing scenarios, via modal logics and in terms of (conditional) equational axiomatizations. Of all those characterizations, which ones do you think have been most useful in future work? To your mind, what are the most interesting or unexpected uses in the literature of the notions and techniques you developed in the "The Linear Time-Branching Time Spectrum"? 
Rob: I think that all these characterizations together shed the light on
process semantics that makes them understandable and useful.
Relational characterizations, i.e., of (bi)simulations, are often the
most useful to grasp what kind of relation one has, and this is essential
for any use. But modal characterizations are intimately linked with
model checking, which is one of the more successful verification tools.
Equational characterizations also find practical use in verification,
e.g., in normalization. Yet, they are most useful in illustrating
the essential difference between process semantics, and thus form a guide
in choosing the right one for an application. To me, the testing scenarios
are the most useful in weighing how realistic certain semantic
identifications are in certain application contexts.
Luca: How much of your later work has built on your award-winning papers? What follow-up results of yours are you most proud of and why?
Rob: About one third, I think.
  • My work on action refinement, together with Ursula Goltz, extends theclassification of process semantics in a direction orthogonal to the linear time - branching time spectrum. I am proud of this work mostly because, for a distinct class of applications, action refinement is great criterion to tell which semantics equivalences one ought to prefer over others. These process semantics have also been used in later work on distributability with Ursula and with Jens-Wolfhard Schicke Uffmann. Distributability tells us which distributed systems can be cast as sequential systems cooperating asynchronously, and which fundamentally cannot.
  • I wrote several papers on Structural Operational Semantics, many jointly with Wan Fokkink, aiming to obtain congruence results for semantic equivalences. These works carefully employed the modal characterizations from my spectrum papers. I consider this work important because congruence properties are essential in verification, as we need compositionality to avoid state explosions. 
  • I used a version of failure simulation semantics from my second spectrum paper in work with Yuxin Deng, Matthew Hennessy, Carroll Morgan and Chenyi Zhang, characterizing may- and must testing equivalences for probabilistic nondeterministic processes. Probability and nondeterminism interact in many applications, and I think that may- and must testing are the right tools to single out the essence of their semantics.

Luca: If I remember correctly, your master thesis was in pure mathematics. Why did you decide to move to a PhD in computer science? What was it like to work as a PhD student at CWI in the late 1980s? How did you start your collaborations with Jos Baeten and fellow PhD student Frits Vaandrager, amongst others? 
Rob: I was interested in mathematical logic already since high school,
after winning a book on the foundations of logic set theory in a
mathematics Olympiad.  I found the material in my logic course,
thought at the University of Leiden by Jan Bergstra, fascinating, and
when doing a related exam at CWI, where Jan had moved to at that
time, and he asked me to do a PhD on related subjects, I say no reason
not to. But he had to convince me first that my work would not involve
any computer science, as my student advisor at The University of
Leiden, Professor Claas, had told us that this was not a real
science. Fortunately, Jan had no problem passing that hurdle.

I was the third member of the team of Jan Bergstra and Jan Willem
Klop, after Jos Baeten had been recruited a few months earlier, but in
a more senior position. Frits arrived a month later than me. As we
were exploring similar subjects, and shared an office, it was natural
to collaborate. As these collaborations worked out very well, they
became quite strong.

CWI was a marvelous environment in the late 1980s. Our group gradually
grew beyond a dozen members, but there remained a much greater
cohesion then I have seen anywhere else. We had weekly process
algebra meetings, where each of us shared our recent ideas with others
in the group. At those meetings, if one member presented a proof, the
entire audience followed it step by step, contributing meaningfully
where needed, and not a single error went unnoticed.

Luca: Already as PhD student, you took up leadership roles within the community. For instance, I remember attending a workshop on "Combining Compositionality and Concurrency" in March 1988, which you co-organized with Ursula Goltz and Ernst-Ruediger Olderog. Would you recommend to a PhD student that he/she become involved in that kind of activities early on in their career? Do you think that doing so had a positive effect on your future career?  
Rob: Generally I recommend this. Although I co-organized this workshop
because the circumstances were right for it, and the need great; not
because I felt it necessary to organize things.  My advice to PhD
students would not be specifically to add a leadership component to
their CV regardless of the circumstances, but instead do take such an
opportunity when the time is right, and not be shy because of lack of
This workshop definitively had a positive effect on my future career.
When finishing my PhD I inquired at Stanford and MIT for a possible
post-doc position, and the good impressions I had left at this
workshop were a factor in getting offers from both institutes.
In fact, Vaughan Pratt, who was deeply impressed with work I had
presented at this workshop, convinced me to apply straight away for an
assistant professorship, and this led to my job at Stanford.   

Luca: I still have vivid memories of your talk at the first CONCUR conference in 1990 in Amsterdam, where you introduced notions of black-box experiments on processes using an actual box and beer-glass mats. You have attended and contributed to many of the editions of the conference since then. To your mind, how has the focus of CONCUR changed since its first edition in 1990? 
Rob: I think the focus on foundations has shifted somewhat to more applied
topics, and the scope of "concurrency theory" has broadened significantly.
Still, many topics from the earlier CONCURs are still celebrated today.

Luca: The last forty years have seen a huge amount of work on process algebra and process calculi. However, the emphasis on that field of research within concurrency theory seems to have diminished over the last few years, even in Europe. What advice would you give to a young researcher interested in working on process calculi today? 
Rob: Until 10 years ago, many people I met in industry voiced the opinion
that formals methods in general, and process algebra in particular,
has been tried in the previous century, and had been found to not to
scale to tackle practical problems. But more recently this opinion is
on the way out, in part because it became clear that the kind of
problems solved by formal methods are much more pressing then originally
believed, and in part because many of the applications that were
deemed to hard in the past, are now being addressed quite adequately.
For these reasons, I think work on process calculi is still a good bet
for a PhD study, although a real-world application motivating the
theory studied is perhaps harder needed than in the past, and toy
examples just to illustrate the theory are not always enough.

Luca: What are the research topics that currently excite you the most?
Rob: I am very excited about showing liveness properties, in Lamport's
sense, telling that a modeled system eventually achieves a desirable outcome.
And even more in creating process algebraic verification frameworks
that are in principle able to do this. I have come to believe that
traditional approaches popular in process algebra and temporal logic
can only deal with liveness properties when making fairness
assumptions that are too strong and lead to unwarranted conclusions.
Together with Peter Hoefner I have been advocating a weaker concept of
fairness, that we call justness, that is much more suitable as a basis
for formulating liveness properties. Embedding this concept into the
conceptual foundations of process algebra and concurrency theory, in
such a way that it can be effectively used in verification, is for a me
a challenging task, involving many exciting open questions.

A vaguely related subject that excites me since the end of last year,
is the extension of standard process algebra with a time-out operator,
while still abstaining from quantifying time. I believe that such an
extension reaches exactly the right level of expressiveness necessary
for many applications.

Both topics also relate with the impossibility of correctly expressing
expressing mutual exclusion in standard process algebras, a discovery
that called forth many philosophical questions, such as under which
assumptions on our hardware is mutual exclusion, when following the
formal definitions of Dijkstra and others, even theoretically implementable.

Friday, April 03, 2020

An interview with Nancy Lynch and Roberto Segala, CONCUR Test-of-Time Award recipients

This post is devoted to the second interview with the colleagues who were selected for the first edition of the CONCUR Test-of-Time Award. (See here for the interview with Davide Sangiorgi.) I asked Nancy Lynch (MIT, USA) and Roberto Segala (University of Verona, Italy) a few questions via email and I copy their answers below. Let  me thank Nancy and Roberto for their answers. I trust that readers of this blog will find them interesting and inspiring.

Luca: You receive one of the two CONCUR ToT Awards for the period 1992-1995 for your paper "Probabilistic simulations for probabilistic processes", presented at CONCUR 1994. Could you tell us briefly what spurred you to develop the “simple” probabilistic automaton model introduced in that paper and how the ideas underlying that notion came about?

Roberto: We were studying randomized distributed algorithms and we noted that several algorithms suffered from subtle errors. We were looking for a formal, rigorous way to study the correctness of those algorithms and in particular we were trying to extend the hierarchical approach used for I/O automata. We knew that there was already an extensive literature within concurrency theory, but we were not able to use the theory to express even the simple idea that you may choose internally between flipping a fair or a biased coin; the existing approaches were extending labeled transition systems by adding probabilities to the arcs, losing the ability to distinguish between probabilistic and nondeterministic choice. The fact that the axioms for nondeterministic choice were not valid in most probabilistic calculi was further evidence of the problem. Starting from the observation that in the non-probabilistic world a step of a distributed algorithm corresponds to a transition of an I/O automaton, we tried to extend the notion of transition so that the process of flipping a coin could be represented by the "new" entity. This led to the idea of "replacing points with measures" within ordinary automata and/or ordinary labeled transition systems. The idea worked very well for our analysis of randomized distributed algorithms, but we also wanted to validate it by checking whether it would simplify the concurrency-theoretical approach to probability. We decided to use simulation relations for our test, and indeed it worked and led to the CONCUR 1994 paper.

Nancy: For background for this paper, we should recall that, at the time,  there was a divergence in styles of modeling for distributed systems, between different concurrency theory research communities.   The style I had been using since the late 70s for modeling distributed algorithms involved interactive state machines, such as I/O automata, which are based on a set-theoretic foundation.  Such models are good for describing distributed algorithms, and for analyzing them for both correctness and costs.  On the other hand, the predominant style in the European concurrency community was more syntactic, based on logical languages like PCTL or various process algebras.  These were good for formal verification, and for studying expressive power of different formalisms, but not great for analyzing complicated distributed algorithms.  Our models were in the general spirit of the Labeled Transition System (LTS) models previously studied in Europe. When Roberto came to MIT, he and I set about to extend prior modeling work for distributed systems to the probabilistic setting.  To do this, we considered both the set-theoretic and logical approaches.  We  needed to bridge the gap between them, which led us to the ideas in this paper.

Luca: How much of your later work has built on your CONCUR 1994 paper? What follow-up results of yours are you most proud of and why?

Roberto: Besides using the results of the paper for the analysis of several randomized distributed algorithms, we worked jointly as well as independently on the study of the theory and on the analysis of security protocols. In collaboration with Frits Vaandrager, we were able to discover different ways to analyze security in a hierarchical and compositional way. Furthermore, since in simple probabilistic automata probability and nondeterminism are well separated, it was easy to include computational complexity into the analysis of security protocols. This is work I did in collaboration with Andrea Turrini. The clear separation between probability and nondeterminism turned out to extend our approach to real-time models, leading to notions like Probabilistic Timed Automata and to several of the elements behind the first sketches of the probabilistic model checker PRISM in collaboration with the group of Marta Kwiatkowska.

Nancy: Roberto and I continued working on probabilistic models, in the set-theoretic style, for several years.  As Roberto notes, Frits Vaandrager also became  a major collaborator.  Some of our more recent papers following this direction are:
This last  paper provides a kind of compositional foundation for combining  security protocols.  The key idea was to weaken the power of the adversary, making it more "oblivious". In other related work, my students and I have worked extensively on  probabilistic distributed algorithms since then.  The models are similar to those developed in this early paper.  Examples include  wireless network algorithms, and more recently, biologically-inspired  algorithms, such as insect colony algorithms and neural network  algorithms.  I can't pinpoint a specific result that relies heavily on  the 1994 paper, but that paper certainly provided inspiration and foundation for the  later work.

Luca: Did you imagine at the time that the CONCUR 1994 paper and its journal version would have so much impact? 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?

Roberto: We knew that the change of view proposed in the paper would have simplified the study and extension of several other concepts within concurrency theory, but we did not have any specific expectations. The collaboration on the PRISM project and on Probabilistic Timed Automata made more evident that there was a connection with Markov Decision Processes, which lead to a fruitful cross-fertilization between artificial intelligence, model checking, and concurrency theory. It was a long exchange of ideas between a world interested in existential quantification, that is, find an optimal policy to achieve a goal, and universal quantification, that is to make sure that under any scheduler, policy, adversary, a system behaves correctly. The consequences of such exchange were many and unexpected.

Nancy: No, I did not anticipate that it would have broad impact, though of course I thought the ideas were important. But in general, I am  bad at predicting what will appeal to others and inspire them to further work.

Luca: The journal version of your paper appears in the Nordic Journal on Computing, which is not a prime venue. Did you ever regret not publishing that work somewhere else? What is your take on the trend of using the perceived quality of a publication venue to evaluate research quality?

Roberto: Within semantics I know of a few technical reports that are much more influential than most journal papers; I do not think that the venue of a paper should be given much importance. On the other hand, venue as an evaluation tool is more objective, allows an evaluator to consider many papers without reading them, and protects the evaluator from any type of claim against decisions, which sometimes may have even legal consequences. Needless to say that I do not agree with any of the ideas above. I do not agree as well with the other emerging trend of counting papers to evaluate quality. One good paper is much better than ten mediocre papers. What worries me the most is that young researchers may have a hard time to concentrate on quality if they have to focus on venue and quantity. I feel I was lucky not to have to worry about these issues when we submitted our paper for the special issue of the Nordic Journal of Computing.

Nancy: I certainly never regretted the venue for this paper. In general, I haven't paid too much attention to choice of publication venue.  The main thing is to reach the audience you want to reach, which can be done through prestigious journals, less prestigious journals, conferences, or even ArXiv technical reports and some publicity. It’s good to get feedback from referees, though. For evaluations, say for hiring or promotion, I think it’s fair to take many factors into account in evaluating research quality. Venues, number of citations, special factors about different fields,… all can be discussed by hiring and promotion committees. But I hope that those committees also take the time to actually read and consider the work itself.

Luca: The last thirty years have seen a huge amount of work on probabilistic models of computation and on the development of proof techniques and tools based on them. What advice would you give to a young researcher interested in working on probabilistic models in concurrency today?

Roberto: My first advice would be to keep things simple and to focus on key ideas, possibly under the guidance of multiple application scenarios. When we study probabilistic concurrency, especially in contexts where the external world is governed by non-discrete laws, the interplay between different features of the model may become overwhelmingly complex. Of course it is a nice exercise to dive into all the details and see what it leads to, or to extend known results to the new scenarios, but how about checking whether some simple changes to one of the building blocks could make life easier? Unfortunately, working on building blocks is risky. So, my second advice is to dive into details and write papers, but take some breaks and think whether there may be nicer ways to solve the same problems.

Nancy: Pick some particular application domain, and make sure that the models  and techniques you develop work well for that application.  Don't work  on the theory in a vacuum.  The models will turn out much better! Perhaps simpler, as Roberto says.

Luca: What are the research topics that currently excite you the most?

Roberto: Difficult question. There are many things I like to look at, but at the moment I am very curious about how quantum computing can fit in a nice and elementary way into a concurrency framework.

Nancy: Probabilistic algorithms, especially those that are flexible (work in  different environments), robust to failures and noise, and adaptive to  changes.  This includes such topics as wireless network algorithms,  robot swarms, and biologically-inspired algorithms.

Acknowledgements: Many thanks to Ilaria Castellani, who pointed out some typos in the original version of this text.  

Thursday, April 02, 2020

An interview with Davide Sangiorgi, CONCUR Test-of-Time Award recipient

The International Conference on Concurrency Theory (CONCUR) and the IFIP 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. 

Wednesday, April 01, 2020

Magnus M. Halldorsson: EATCS Fellow 2020

As announced here, the EATCS Fellows vintage 2020 are
  • Pierpaolo Degano, Universita di Pisa, Italy: for his contributions in concurrency theory and applications in security and for biological systems. 
  • Mohammad Taghi Hajiaghayi, University of Maryland, USA: for his contributions to the theory of algorithms, in particular algorithmic graph theory, game theory, and distributed computing. 
  • Magnus Mar Halldorsson, Reyjavik University, Iceland: for his contributions to the theory of approximation and graph algorithms as well as to the study of wireless algorithmics. 
Congratulations to all of them! However, I trust that Mohammad and Pierpaolo will forgive me if I devote this post to celebrate Magnus, his work and his contributions to the TCS community.

So, why was Magnus chosen as one of the EATCS Fellows 2020? Here are some reasons why.

Magnús has offered seminal contributions to the theory of approximation and graph algorithms as well as to the study of wireless algorithmics. His research career and contributions so far can be roughly divided into two phases. The first phase spans the time from the beginning of his career until roughly ten years ago. During that time, Magnús made significant contributions to approximation algorithms for maximum independent set and graph colouring, amongst many other problems. In the second phase, which started a bit more than ten years ago, he has worked on the algorithmics of realistic models for wireless computation. I think that it is fair to say that Magnús is currently the expert on wireless algorithmics based on the SINR model.

These two phases are not at all disjoint. Indeed, the typical problems studied in the SINR model, such as determining the capacity of wireless networks or how to schedule messages in such networks, can be seen as independent set and colouring problems, respectively, and his experience with those problems in graph algorithmics certainly helped Magnús in obtaining breakthrough results in wireless algorithmics. Throughout his career, Magnús has also given significant contributions to the computation of independent sets and colourings in restricted computational models, such as the online model of computation and the data streaming model. His sustained research productivity, both in quality and in quantity, is all the more remarkable since it has largely been achieved working in the difficult research environment in Iceland, where he was largely isolated until the establishment of the Icelandic Centre of Excellent in Theoretical Computer Science (ICE-TCS) in 2005. (Magnus has been the scientific director of the centre for 15 years.)

In addition to his seminal research achievements, Magnús has served the theoretical computer science community by sitting on prestigious award committees, organizing conferences and workshops in Iceland and elsewhere, serving on steering committees and by acting as an inspiring mentor for young researchers in computer science who have come to Iceland explicitly to work with him. By way of example, Magnús is a member of the steering committees for SIROCCO (chair), ALGOSENSORS and SWAT, Scandinavian Symposium and Workshops on Algorithm Theory (chair). He was a member of the Council of the EATCS and has organized the best attended ICALP conference to date (ICALP 2008). Amongst many other such duties, he was PC chair for Track C of ICALP 2015 and of ESA 2011.

Magnús was also one of the initiators and first editors of “A compendium of NP optimization problems”, which is catalog of approximability results for NP optimization problems and has been a useful resource for researchers in that field for a long time.

Summing up, Magnús is a true stalwart of the algorithmics research community, and a great example for many of us. In my, admittedly biased, opinion, he richly deserves the recognition of being named an EATCS Fellow. I have no doubt that he will continue to lead by example in the coming years.