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.
|