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.
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.
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.
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
experience.
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
experience.
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.
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.
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.
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.
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.
No comments:
Post a Comment