Blog icon

Prof Rob van Glabbeek

Chief Research Scientist

Contact details:



Rob van Glabbeek has a strong international reputation in the study of the theory of concurrent computation, having made particular contributions to the conciliation of the interleaving and the true concurrency communities by codeveloping the current view of branching time and causality as orthogonal but interacting dimensions of concurrency. He condensed many divergent views on semantic equivalences into the linear time- branching time spectrum. The resulting publications are required reading in the graduate programs of several universities. Together with Peter Weijland he invented the notion of branching bisimulation, that since has become the prototypical example of a branching time equivalence, and the semantic equivalence used in most verification tools based on equivalence checking. With Ursula Goltz he proposed the notion of action refinement as a useful tool for evaluating semantic equivalences and implementation relations. This gave rise to a wave of publications, including a dozen Ph.D. theses. With Peter Rittgen he initiated the application of process algebraic methods in the formal description and analysis of economic production processes. As consultant for Ricoh innovations he contributed to the practical application of concurrency-theoretic ideas in workflow management. With Dominic Hughes he made a crucial contribution to the proof theory of linear logic by proposing a notion of proof net that had been sought after in vain by linear logicians since the inception of linear logic. Together with Vaughan Pratt he initiated the now widespread use of higher dimensional automata and other geometric models of concurrency. With Gordon Plotkin he integrated various causality respecting models of concurrency, including Petri nets, event structures and propositional theories. By bridging the areas of structural operational semantics and logic programming, he developed a proof method and semantics that applies simultaneously to transition system specifications and logic programs. With Wan Fokkink he used results from unification theory and from modal logic to obtain compositionality results in structural operational semantics. This research gave rise to many congruence formats for semantic equivalences and preorders, which allow one to infer compositionality from purely syntactic properties of language specifications. In 2017 he even contributed a congruence format for recursion. In 2007, in cooperation with Yuxin Deng, Matthew Hennessy, Carroll Morgan and Chenyi Zhang, he characterised the may- and must-testing preorders for processes with probabilistic and nondeterministic choice, thereby solving a problem that was posed in 1992 and had remained open ever since. Together with Bas Ploeger, he showed that the leading algorithm for determining whether a program (abstractly represented as a transition system) correctly simulates another such program, is based on a fixed point theory that is irreparably flawed; and repaired the algorithm in a way that bypasses this fixed point theory. In 2011, together with NICTA colleagues Peter Höfner, Annabelle MvIver, Ansgar Fehnker, Marius Portman and Wee Lum Tan, he developed a new process algebra for wireless mesh networks and used it to obtain the first rigorous formalisation of the specification of the popular Ad-hoc On-demand Distance Vector (AODV) routing protocol. This revealed that under a plausible interpretation of the original specification of AODV, the protocol does admit routing loops; this is in direct contradiction with popular belief, the promises of the AODV specification, and the main paper on AODV (with 13000 citations). The NICTA team also proved loop-freedom of AODV under a subtly different interpretation of the original specification. In cooperation with Tim Bourke, this work was mechanically formalised with the theorem prover Isabelle/HOL. In 2012, together with Ursula Goltz and Jens Schicke-Uffmann, he gave a precise characterisation of the class of concurrent systems, modelled as plain Petri nets, that, without making concessions on branching time behaviour, concurrency or divergence, cannot be implemented in a distributed way using only asynchronous communication. In 2015, jointly with Peter Höfner, he established that fair schedulers, as frequently occur in network routers and operating systems, as well as correct mutual exclusion protocols, cannot be rendered in standard process algebras like CCS, at least not without resorting to fairness assumptions. For this type of application, mild extensions of CCS are called for. Also together with Peter Höfner, he wrote a definitive survey of fairness assumptions for concurrent systems, and introduced justness, an assumption in between progress and weak fairness, that is crucial for proving liveness properties of distributed system. In 2019 he published a research agenda for proving liveness properties that is based on this notion; it calls for a radical adaptation of established theories, including strong bisimilarity. He added reward testing as a new and more powerful mode of testing concurrent systems, besides the classical modes of may, must and should testing. In 2020 he proposed reactive temporal logic, a form of temporal logic better adapted to the study of reactive systems. Amongst others, it allows unambiguous formal specifications of what does and doesn't count as a correct mutual exclusion protocol.

In addition, he has organised workshops on combining compositionality and concurrency, on logic, language and information, on the Unified Modelling Language, on workflow management, web services and business process modelling, on automatic and semi-automatic system verification, on structural operational semantics, on formal methods for embedded systems, and on models for formal analysis of real systems .

He is editor-in-chief of Electronic Proceedings in Theoretical Computer Science, a member of the editorial boards of Information and Computation and Theoretical Computer Science, and has been on several dozen program committees.

Related Pages

Achievements and Awards

  • 2015-my death

    Foreign member
    The Royal Holland Society of Sciences and Humanities

  • 1990-2020

    Test-of-time award

Current Roles

  • Editor in Chief
    of Electronic Proceedings in Theoretical Computer Science

  • Member editorial board
    of Information and Computation

  • Member editorial board
    of Theoretical Computer Science

Academic Qualifications

  • 1984

    Master of Science
    University of Leiden, The Netherlands

  • 1990

    Free University, Amsterdam, The Netherlands

Professional Experiences

  • September 1981-November 1984

    Teaching Assistant
    University of Leiden, The Netherlands

  • December 1984-November 1989

    Research Scientist
    Centre for Mathematics and Computer Science (CWI), Amsterdam, The Netherlands

  • February 1990-August 1990

    Research Scientist
    Technical University of Munich, Germany

  • September 1990-August 1991

    Acting Assistant Professor
    Stanford University, USA

  • September 1991-August 2002

    Research Associate
    Stanford University, USA

  • September 2002-Present

    Research Affiliate (not a paid position)
    Concurrency Group, Stanford University, USA

  • August 2000-January 2003

    Ricoh Innovations, Menlo Park, California, USA

  • November 2002-December 2002

    Research Scientist
    Centre for Mathematics and Computer Science (CWI), Amsterdam, The Netherlands

  • February, 2003-May, 2003

    Associate Professor
    NICTA/UNSW, Sydney, Australia

  • June 2003-August 2003

    Visiting Fellow
    INRIA, France

  • September 2003-March 2004

    Visiting Research Fellow
    University of Edinburgh, UK

  • April 2004-May 2004

    Visiting Research Fellow
    University of Cambridge

  • June 2004-June 2016

    Principal Researcher
    NICTA, Sydney, Australia

  • June 2004-December 2007

    Conjoint Associate Professor (not a paid position)
    University of New South Wales, Sydney, Australia

  • January 2008-Present

    Conjoint Professor (not a paid position)
    University of New South Wales, Sydney, Australia

  • July 2016-Present

    Chief Research Scientist
    Data61, CSIRO, Sydney, Australia