8 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…
Unique Solutions of Guarded Recursive Equations
Rob van Glabbeek
This paper shows that guarded systems of recursive equations have unique solutions up to strong bisimilarity for any process algebra with a structural operation semantics in the re…
Formal Methods for Mobile Ad Hoc Networks: A Survey
Wan Fokkink, Rob van Glabbeek
In a mobile ad hoc network (MANET), communication is wireless and nodes can move independently. Properly analyzing the functional correctness, performance, and security of MANET pr…
Just Verification of Mutual Exclusion Algorithms
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…
More on Maximally Permissive Similarity Control of Discrete Event Systems
Yu Wang, Zhaohui Zhu, Rob van Glabbeek +3
Takai proposed a method for constructing a maximally permissive supervisor for the similarity control problem (IEEE Transactions on Automatic Control, 66(7):3197-3204, 2021). This…