Keep it Fair: Equivalences
Keep it Fair: Equivalences
复制标题
保持公平：等价
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Stephan Mennicke
中科院分区：
文献类型：
--
作者：
Tobias Prehn;Stephan Mennicke
对于并发和分布式系统的模型，在安全性和/或活性属性方面建立正确性非常重要且具有挑战性。分布式系统理论认为等价是基本的，因为它们（1）保留了理想的正确性特征，（2）通常允许组件替换，使组合推理变得可行。对分布式系统进行建模通常需要利用非确定性进行抽象，这会导致无限执行方面的意外行为，并反复解决一个非确定性选择，每次都会忽略一个替代方案。这些情况被认为是不现实或极不可能的。公平假设通常用于过滤系统行为，从而区分现实和不现实的执行。这允许在分布式系统的正确性证明中提供关键参数，否则这是不可能的。我们的贡献是保留了公平假设的等价谱。所确定的等价性允许对结合公平性假设的正确性进行（组合）推理。
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.