Robert Jan van Glabbeek - Selected Publications#

(with W.P. Weijland) Branching time and abstraction in bisimulation semantics, Journal of the ACM 43(3), 1996, pp. 555-600.
1166 citations.

This paper contributed 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. Impressive verifications of industrially relevant software, based on this notion, have been carried out by the mCRL2 group at the university of Eindhoven (\href{https://mcrl2.org}{https://mcrl2.org}) and the CADP group in Grenoble (\href{http://cadp.inria.fr}{http://cadp.inria.fr/}).

The linear time - branching time spectrum I; the semantics of concrete, sequential processes, in: Handbook of Process Algebra (J.A. Bergstra, A. Ponse & S.A. Smolka, eds.), Chapter 1, Elsevier, 2001, pp. 3-99.
1453 citations. There is also a follow-up paper with 721 citations.

This paper helped unify a multitude of different approaches to concurrency theory by classifying the (sometimes implicit) underlying semantic equivalences used therein.

(with U. Goltz) Refinement of Actions and Equivalence Notions for Concurrent Systems, Acta Informatica 37(4/5), 2001, pp. 229-327.
368+298 citations.

This work was crucial in the conciliation of the interleaving and the true concurrency communities by co-developing the current view of branching time and causality as orthogonal, but interacting, dimensions of concurrency.

(with S.A. Smolka & B. Steffen) Reactive, Generative and Stratified Models of Probabilistic Processes, Information and Computation 121(1), 1995, pp. 59-80.
679 citations.

This paper was a milestone in the work of understanding probabilistic processes.

(with F.W. Vaandrager) Petri net models for algebraic theories of concurrency (extended abstract), in: Proceedings PARLE conference, Eindhoven, The Netherlands 1987, Vol. II (Parallel Languages) (J.W. de Bakker, A.J. Nijman & P.C. Treleaven, eds.), LNCS 259, Springer-Verlag, 1987, pp. 224-242.
415 citations.

This was one of the key papers that helped bridge the gap between process algebra and Petri net approached to concurrency.

(with D.J.D. Hughes) Proof Nets for Unit-free Multiplicative-Additive Linear Logic, ACM Transactions on Computational Logic 6(4), 2005, pp. 784-842.
94+64 citations.

This paper 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.

(with Y. Deng, M. Hennessy & C.C. Morgan) Characterising Testing Preorders for Finite Probabilistic Processes, July 2008. Archived at http://arxiv.org/abs/0810.3708. Logical Methods in Computer Science 4(4:4), 2008, pp. 1-33.
127 citations

This work lays foundations of the verification of systems with both probabilistic and nondeterministic choice. It 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.

(with P. Höfner) Progress, Justness and Fairness. Archived at http://arxiv.org/abs/1810.07414. ACM Computing Surveys 52(4):69, 2019, doi:10.1145/3329125.
28 citations

This papers presents an authoritative survey on fairness in distributed systems.
It also proposes the notion of justness, an assumption in between progress and fairness, that is crucial for proving liveness properties of distributed system when abstracting from real-time.

(with P. Höfner, M. Portmann & W.L. Tan) Modelling and Verifying the AODV Routing Protocol. Archived at http://arxiv.org/abs/1512.08867. Distributed Computing 29(4), 2016, pp. 279-315, doi:10.1007/s00446-015-0262-7.
63 citations (+90+63)

This work 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 26000 citations). The paper also proved loop-freedom of AODV under a subtly different interpretation of the original specification.

(with U. Goltz & J.-W. Schicke-Uffmann) On Characterising Distributability. Archived at http://arxiv.org/abs/1309.3883. Logical Methods in Computer Science 9(3:17), 2013, pp. 1-58.
58 citations.

This paper gave a precise characterisation of the class of concurrent systems, that, without making concessions on branching time behaviour, concurrency or divergence, cannot be implemented in a distributed way using only asynchronous communication.

(with G.D. Plotkin) Configuration Structures, Event Structures and Petri Nets. Archived at http://arxiv.org/abs/0912.4023. Theoretical Computer Science 410(41) (2009), pp. 4111-4159.
163+123 citations.

This paper bridged a lot of work in domain theory and concurrency theory.