Skip to main content

Justness: A completeness criterion for capturing liveness properties

Authors

Rob van Glabbeek

DATA61

UNSW Sydney

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.

BibTeX Entry

  @inproceedings{vanGlabbeek_19,
    publisher        = {Springer},
    doi              = {https://doi.org/10.1007/978-3-030-17127-8\_29},
    series           = {LNCS 11425},
    booktitle        = {22st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS
                        2019)},
    author           = {van Glabbeek, Rob},
    month            = apr,
    volume           = {LNCS 11425},
    editor           = {{BojaƄczyk, Mikolaj and Simpson, Alex}},
    keywords         = {Justness; progress, fairness; completeness criteria; liveness; distributed systems; process algebra;
                        labelled transition systems with concurrency; {CCS}; broadcast communication; signals.},
    year             = {2019},
    date             = {2019-4-5},
    title            = {Justness: {A} Completeness Criterion for Capturing Liveness Properties},
    pages            = {505-522},
    address          = {Prague, Czech Republic}
  }

Download