Progress, Fairness and Justness in Process Algebra

Abstract

To prove liveness properties of concurrent systems, it is often necessary to postulate progress, fairness and justness properties. This paper investigates how the necessary progress, fairness and justness assumptions can be added to or incorporated in a standard process-algebraic specification formalism. We propose a formalisation that can be applied to a wide range of process algebras. The presented formalism is used to reason about route discovery and packet delivery in the setting of wireless networks.

Cited by in corpus (9)

• 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
• Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP
• Analysing Mutual Exclusion using Process Algebra with Signals
• Ensuring Liveness Properties of Distributed Systems: Open Problems
• Justness: A Completeness Criterion for Capturing Liveness Properties
• Reward Testing Equivalences for Processes
• A Lean-Congruence Format for EP-Bisimilarity
• Modelling Mutual Exclusion in a Process Algebra with Time-outs