Justness: A Completeness Criterion for Capturing Liveness Properties
arXiv:1909.00286
Abstract
This paper poses that transition systems constitute a good model of distributed systems only in combination with a criterion telling which paths model complete runs of the represented systems. Among such criteria, progress is too weak to capture relevant liveness properties, and fairness is often too strong; for typical applications we advocate the intermediate criterion of justness. Previously, we proposed a definition of justness in terms of an asymmetric concurrency relation between transitions. Here we define such a concurrency relation for the transition systems associated to the process algebra CCS as well as its extensions with broadcast communication and signals, thereby making these process algebras suitable for capturing liveness properties requiring justness.
This second version incorporates many small improvements based on feedback from Weiyou Wang. An extended abstract of this paper appears in Proc. FoSSaCS'19
References in corpus (6)
- A Process Algebra for Wireless Mesh Networks
- Progress, Justness and Fairness
- CCS: It's not Fair! Fair Schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions
- Analysing Mutual Exclusion using Process Algebra with Signals
- Progress, Fairness and Justness in Process Algebra
- Ensuring Liveness Properties of Distributed Systems (A Research Agenda)