Keep it Fair: Equivalences

Tobias Prehn
(TU Berlin, Germany)
Stephan Mennicke
(TU Braunschweig, Germany)

For models of concurrent and distributed systems, it is important and also challenging to establish correctness in terms of safety and/or liveness properties. Theories of distributed systems consider equivalences fundamental, since they (1) preserve desirable correctness characteristics and (2) often allow for component substitution making compositional reasoning feasible. Modeling distributed systems often requires abstraction utilizing nondeterminism which induces unintended behaviors in terms of infinite executions with one nondeterministic choice being recurrently resolved, each time neglecting a single alternative. These situations are considered unrealistic or highly improbable. Fairness assumptions are commonly used to filter system behaviors, thereby distinguishing between realistic and unrealistic executions. This allows for key arguments in correctness proofs of distributed systems, which would not be possible otherwise. Our contribution is an equivalence spectrum in which fairness assumptions are preserved. The identified equivalences allow for (compositional) reasoning about correctness incorporating fairness assumptions.

In Massimo Bartoletti, Laura Bocchi, Ludovic Henrio and Sophia Knight: Proceedings 10th Interaction and Concurrency Experience (ICE 2017), Neuchâtel, Switzerland, 21-22nd June 2017, Electronic Proceedings in Theoretical Computer Science 261, pp. 5–16.
Published: 29th November 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: