98 citations · 569 across the 35 of their papers we have counts for
38 papers
The Infinite, in Finite Time
Rayhana Amjad, Rob van Glabbeek, Liam O'Connor
Linear-time temporal properties, such as those described by Linear-time Temporal Logic, are typically modelled as sets of infinite traces. Yet, in a run-time verification context,…
Bisimulations and Modal Logics for Higher Dimensional Automata
Safa Zouari, Rob van Glabbeek, Krzysztof Ziemiański
Higher-Dimensional Automata (HDAs) provide a geometric model of true concurrency. While hereditary history-preserving (hhp) bisimilarity is the finest behavioural equivalence in va…
On the Notions of Bounded Bypass, and How to Make any Deadlock-Free MUTEX Protocol Satisfy One of Them
Rob van Glabbeek, Daniele Gorla, Myrthe Spronck
In the literature on mutual exclusion, bounded bypass has been used for a long time as a strengthening of starvation-freedom, but, to the best of our knowledge, it still lacks a sa…
Formally Verified Liveness with Multiparty Session Types in Rocq
Omer Keskin, Nobuko Yoshida, Rob van Glabbeek
Multiparty session types (MPST) offer a framework for the description of communication-based protocols involving multiple participants. In the top-down approach to MPST, the commun…
The Similarity Control Problem with Required Events
Yu Wang, Zhaohui Zhu, Rob van Glabbeek +2
In order to guarantee that a supervised system satisfies safety requirements of the specification, as well as requirements saying that in certain states certain events must be enab…
A Lean-Congruence Format for EP-Bisimilarity
Rob van Glabbeek, Peter Höfner, Weiyou Wang
Enabling preserving bisimilarity is a refinement of strong bisimilarity that preserves safety as well as liveness properties. To define it properly, labelled transition systems nee…
A Cancellation Law for Probabilistic Processes
Rob van Glabbeek, Jan Friso Groote, Erik de Vink
We show a cancellation property for probabilistic choice. If distributions mu + rho and nu + rho are branching probabilistic bisimilar, then distributions mu and nu are also branch…
A Lean-Congruence Format for EP-Bisimilarity
Rob van Glabbeek, Peter Höfner, Weiyou Wang
Enabling preserving bisimilarity is a refinement of strong bisimilarity, which preserves safety as well as liveness properties. To define it properly, labelled transition systems n…
Fair Must Testing for I/O Automata
Rob van Glabbeek
The concept of must testing is naturally parametrised with a chosen completeness criterion or fairness assumption. When taking weak fairness as used in I/O automata, I show that it…
Just Testing
Rob van Glabbeek
The concept of must testing is naturally parametrised with a chosen completeness criterion, defining the complete runs of a system. Here I employ justness as this completeness crit…
Abstract Processes in the Absence of Conflicts in General Place/Transition Systems
Rob van Glabbeek, Ursula Goltz, Jens-Wolfhard Schicke-Uffmann
Goltz and Reisig generalised Petri's concept of processes of one-safe Petri nets to general nets where places carry multiple tokens. BD-processes are equivalence classes of Goltz-R…
Modelling Mutual Exclusion in a Process Algebra with Time-outs
Rob van Glabbeek
I show that in a standard process algebra extended with time-outs one can correctly model mutual exclusion in such a way that starvation-freedom holds without assuming fairness or…
Reactive Bisimulation Semantics for a Process Algebra with Time-Outs
Rob van Glabbeek
This paper introduces the counterpart of strong bisimilarity for labelled transition systems extended with time-out transitions. It supports this concept through a modal characteri…
Failure Trace Semantics for a Process Algebra with Time-outs
Rob van Glabbeek
This paper extends a standard process algebra with a time-out operator, thereby increasing its absolute expressiveness, while remaining within the realm of untimed process algebra,…
Justness: A Completeness Criterion for Capturing Liveness Properties
Rob van Glabbeek
This paper poses that transition systems constitute a good model of distributed systems only in combination with a criterion telling which paths model complete runs of the represen…
Rooted Divergence-Preserving Branching Bisimilarity is a Congruence
Rob van Glabbeek, Bas Luttik, Linda Spaninks
We prove that rooted divergence-preserving branching bisimilarity is a congruence for the process specification language consisting of nil, action prefix, choice, and the recursion…
Lean and Full Congruence Formats for Recursion
Rob van Glabbeek
In this paper I distinguish two (pre)congruence requirements for semantic equivalences and preorders on processes given as closed terms in a system description language with a recu…
MALL proof nets identify proofs modulo rule commutation
Rob van Glabbeek, Dominic Hughes
We show that the proof nets introduced in [Hughes & van Glabbeek 2003, 2005] for MALL (Multiplicative Additive Linear Logic, without units) identify cut-free proofs modulo rule com…
Divide and Congruence II: From Decomposition of Modal Formulas to Preservation of Delay and Weak Bisimilarity
Wan Fokkink, Rob van Glabbeek
Earlier we presented a method to decompose modal formulas for processes with the internal action , and congruence formats for branching and -bisimilarity were derived on the…
Sequence Numbers Do Not Guarantee Loop Freedom; AODV Can Yield Routing Loops
Rob van Glabbeek, Peter Höfner, Wee Lum Tan +1
In the area of mobile ad-hoc networks and wireless mesh networks, sequence numbers are often used in routing protocols to avoid routing loops. It is commonly stated in protocol spe…
Modelling and Verifying the AODV Routing Protocol
Rob van Glabbeek, Peter Höfner, Marius Portmann +1
This paper presents a formal specification of the Ad hoc On-Demand Distance Vector (AODV) routing protocol using AWN (Algebra for Wireless Networks), a recent process algebra which…
Automated Analysis of AODV using UPPAAL
Ansgar Fehnker, Rob van Glabbeek, Peter Höfner +3
This paper describes an automated, formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in wireless mesh networks.…
A Process Algebra for Wireless Mesh Networks
Ansgar Fehnker, Rob van Glabbeek, Peter Höfner +3
We propose a process algebra for wireless mesh networks that combines novel treatments of local broadcast, conditional unicast and data structures. In this framework, we model the…
Modelling and Analysis of AODV in UPPAAL
Ansgar Fehnker, Rob van Glabbeek, Peter Höfner +3
This paper describes work in progress towards an automated formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in…