Trustworthy Systems

The coarsest precongruences respecting safety and liveness properties

Authors

Rob van Glabbeek

NICTA

UNSW

Abstract

This paper characterises the coarsest refinement preorders on labelled transition systems that are precongruences for renaming and partially synchronous interleaving operators, and respect all safety, liveness, and conditional liveness properties, respectively.

BibTeX Entry

  @inproceedings{vanGlabbeek_10,
    address          = {Brisbane},
    author           = {van Glabbeek, Robert},
    booktitle        = {Theoretical Computer Science 2010},
    editor           = {{C.S. Calude \& V. Sassone}},
    issn             = {1868-4238},
    keywords         = {safety properties, liveness properties, conditional liveness properties, refinement preorders,
                        labelled transition systems, full abstraction, process algebra, partially synchronous interleaving
                        operator, abstraction, state operator, deadlock, divergence},
    month            = sep,
    pages            = {32--52},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/3971.pdf},
    publisher        = {Springer},
    title            = {The Coarsest Precongruences Respecting Safety and Liveness Properties},
    year             = {2010}
  }

Download