98 citations · 569 across the 35 of their papers we have counts for
31 papers · 1 filter
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…
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…
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…
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…
Mechanizing a Process Algebra for Network Protocols
Timothy Bourke, Robert J. van Glabbeek, Peter Höfner
This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invar…
Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP
Rob van Glabbeek
In 1987 Ernst-Rüdiger Olderog provided an operational Petri net semantics for a subset of CCSP, the union of Milner's CCS and Hoare's CSP. It assigns to each process term in the su…
Analysing and Comparing Encodability Criteria
Kirstin Peters, Rob van Glabbeek
Encodings or the proof of their absence are the main way to compare process calculi. To analyse the quality of encodings and to rule out trivial or meaningless encodings, they are…
On the Axiomatizability of Impossible Futures
Taolue Chen, Wan Fokkink, Rob van Glabbeek
A general method is established to derive a ground-complete axiomatization for a weak semantics from such an axiomatization for its concrete counterpart, in the context of the proc…
Progress, Fairness and Justness in Process Algebra
Rob van Glabbeek, Peter Höfner
To prove liveness properties of concurrent systems, it is often necessary to postulate progress, fairness and justness properties. This paper investigates how the necessary progres…
Showing invariance compositionally for a process algebra for network protocols
Timothy Bourke, Robert J. van Glabbeek, Peter Höfner
This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invar…