Paper: Turning SOS rules into equations (at LICS 1992)

Authors: Luca Aceto Bard Bloom Fritz W. Vaandrager

Abstract

A procedure is given for extracting from a GSOS specification of an arbitrary process algebra a complete axiom system for bisimulation equivalence (equational, except for possibly one conditional equation). The methods apply to almost all SOSs for process algebras that have appeared in the literature, and the axiomatizations compare reasonably well with most axioms that have been presented. In particular, they discover the L characterization of parallel composition. It is noted that completeness results for equational axiomatizations are tedious and have become rather standard in many cases. A generalization of extant completeness results shows that in principle this burden can be completely removed if one gives a GSOS description of a process algebra

BibTeX

  @InProceedings{AcetoBloomVaandrage-TurningSOSrulesinto,
    author = 	 {Luca Aceto and Bard Bloom and Fritz W. Vaandrager},
    title = 	 {Turning SOS rules into equations},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS 1992)},
    year =	 {1992},
    month =	 {June}, 
    pages =      {113--124},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }