Pith. sign in

REVIEW 2 cited by

Progress, Fairness and Justness in Process Algebra

Not yet reviewed by Pith; the record is open.

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1501.03268 v1 pith:LJ4V7GLA submitted 2015-01-14 cs.LO

classification cs.LO
keywords fairnessjustnessprogressformalismnecessaryprocesspropertiesadded
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
read the original 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.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Justness: A Completeness Criterion for Capturing Liveness Properties

    cs.LO 2019-08 accept novelty 6.0 of 10

    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.

  2. Ensuring Liveness Properties of Distributed Systems: Open Problems

    cs.LO 2019-08 accept novelty 4.0 of 10

    A research agenda for a theory of concurrency that proves liveness properties using justness instead of fairness, because fairness assumptions can yield conclusions that do not hold in reality.

Pith tools