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.