This paper defines a synchron-based concurrency relation for CCS, ABC, and CCSS, making the justness criterion formally available and proving it agrees with previous coinductive definitions.
Progress, Fairness and Justness in Process Algebra
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
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.
citation-role summary
background 1
citation-polarity summary
fields
cs.LO 1years
2019 1verdicts
ACCEPT 1roles
background 1polarities
background 1representative citing papers
citing papers explorer
-
Justness: A Completeness Criterion for Capturing Liveness Properties
This paper defines a synchron-based concurrency relation for CCS, ABC, and CCSS, making the justness criterion formally available and proving it agrees with previous coinductive definitions.