Trustworthy Systems

On infinite guarded recursive specifications in process algebra

Authors

Rob van Glabbeek and Kees Middelburg

DATA61

University of Amsterdam

UNSW Sydney

Abstract

In most presentations of ACP with guarded recursion, recursive specifications are finite or infinite sets of recursion equations of which the right-hand sides are guarded terms. The completeness with respect to bisimulation equivalence of the axioms of ACP with guarded recursion has only been proved for the special case where recursive specifications are finite sets of recursion equations of which the right-hand sides are guarded terms of a restricted form known as linear terms. In this note, we widen this completeness result to the general case.

BibTeX Entry

  @techreport{vanGlabbeek_Middelburg_20:tr,
    author           = {van Glabbeek, Robert and Middelburg, Kees},
    date             = {2020-5-2},
    institution      = {Data61, CSIRO},
    keywords         = {process algebra; guarded recursion; completeness; infinitary conditional logic},
    month            = may,
    numpages         = {9},
    paperurl         = {https://trustworthy.systems/publications/full_text/vanGlabbeek_Middelburg_20%3Atr.pdf},
    publisher        = {arXiv},
    series           = {arXiv:2005.00746},
    title            = {On Infinite Guarded Recursive Specifications in Process Algebra},
    year             = {2020}
  }

Download