4 papers
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…
Just Verification of Mutual Exclusion Algorithms with (Non-)Blocking and (Non-)Atomic Registers
Rob van Glabbeek, Bas Luttik, Myrthe Spronck
We verify the correctness of a variety of mutual exclusion algorithms through model checking. We look at algorithms where communication is via shared read/write registers, where th…
Stronger Validity Criteria for Encoding Synchrony
Rob van Glabbeek, Ursula Goltz, Christopher Lippert +1
We analyse two translations from the synchronous into the asynchronous -calculus, both without choice, that are often quoted as standard examples of valid encodings, showing th…
A Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with Probabilistic Choice
Rob van Glabbeek, Jan Friso Groote, Erik de Vink
This paper proposes a notion of branching bisimilarity for non-deterministic probabilistic processes. In order to characterize the corresponding notion of rooted branching probabil…