Trustworthy Systems

Asynchronous Communication in Distributed Systems

Activities

  • Synchronous versus asynchronous communication: We propose and inventory various definitions of what it means for processes to communicate with each other using only asynchronous communication, and subsequently investigate which processes can be implemented conform these definitions. In deciding whether a given process can be implemented using only asynchronous communication, one needs to choose a semantic equivalence that specifies which aspects of the specified behaviour need to be preserved under implementation. Depending on this choice, either a class of systems can be implemented distributedly—and we aim at giving a structural characterisation of this class—or all systems can be implemented distributedly—and we aim to investigate the strongest behavioural equivalence that makes this possible.
  • Causal semantics of Petri nets: A well-known problem in Petri net theory, open since the mid eighties, is to formalise an appropriate causality-based concept of process or run. The so-called "individual token interpretation", where tokens are distinguished according to their causal history, giving rise to the processes of Goltz and Reisig (1983), makes distinctions between runs that are commonly understood to be the same. This project studies a class of Petri nets, the structural conflict nets, that strictly contains the well-known 1-safe nets and is closed under asynchronous parallel composition. On this class we propose an abstract concept of process, and aim to show that it constitutes a simple and fully satisfying solution.
  • Expressiveness of process calculi: We propose and elaborate a definition of what it means for one system description language to encode another one, thereby enabling an ordering of system description languages with respect to expressive power. Our definition requires a system to be behaviourally equivalent with its encoding, and thus is parametrised with the choice of a suitable semantic equivalence on the represented processes. By means of a series of case studies we hope to ascertain which semantic equivalences are most suitable for certain applications. Finally, we hope to apply the framework to compare the expressiveness of existing process calculi, in particular focussing on calculi with synchronous and with asynchronous communication primitives.

People

Past

  • Rob van Glabbeek

Publications

To appear

Abstract PDF Rob van Glabbeek, Ursula Goltz and Jens-Wolfhard Schicke-Uffmann
Abstract processes and conflicts in place/transition systems
Information and Computation

2020

Abstract PDF Rob van Glabbeek, Vincent Gramoli and Pierre Tholoniat
Feasibility of cross-chain payment with success guarantees
32nd ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2020, pp. 579-581, Virtual event, July, 2020

2019

Abstract PDF Rob van Glabbeek, Vincent Gramoli and Pierre Tholoniat
Cross-chain payment protocols with success guarantees
Technical Report, Data61, CSIRO, December, 2019
Abstract PDF Rob van Glabbeek, Ursula Goltz, Christopher Lippert and Mennicke Stephan
Stronger validity criteria for encoding synchrony
The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy — Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday, pp. 182-205, Paris, November, 2019
Abstract PDF Rob van Glabbeek
Ensuring liveness properties of distributed systems: Open problems
Journal of Logical and Algebraic Methods in Programming, Volume 109, pp. 1-19, August, 2019
Abstract PDF Rob van Glabbeek and Peter Hoefner
Progress, justness and fairness
ACM Computing Surveys, Volume 52, Issue 4, pp. 69:1–69:38, August, 2019
Abstract PDF Rob van Glabbeek
Justness: A completeness criterion for capturing liveness properties
International Conference on Foundations of Software Science and Computational Structures, pp. 505-522, Prague, Czech Republic, April, 2019

2018

Abstract PDF Rob van Glabbeek and Peter Hoefner
Progress, justness and fairness
Technical Report, Data61, CSIRO, October, 2018
Abstract PDF Rob van Glabbeek
On the validity of encodings of the synchronous in the asynchronous π-calculus
Information Processing Letters, Volume 137, pp. 17-25, September, 2018
Abstract PDF Rob van Glabbeek
Is speed-independent mutual exclusion implementable?
International Conference on Concurrency Theory (CONCUR), Beijing, China, September, 2018
Abstract PDF Rob van Glabbeek
A theory of encodings and expressiveness
International Conference on Foundations of Software Science and Computational Structures, pp. 183-202, Thessaloniki, Greece, April, 2018

2017

Abstract PDF Victor Dyseryn, Rob van Glabbeek and Peter Hoefner
Analysing mutual exclusion using process algebra with signals
Combined International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics (EXPRESS/SOS), Berlin, August, 2017

2015

Abstract PDF Kirstin Peters and Rob van Glabbeek
Analysing and comparing encodability criteria
Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics, pp. 46–60, Madrid, Spain, August, 2015