Paper: Turning SOS rules into equations (at LICS 1992)
Authors: Aceto, L. Bloom, B. Vaandrager, F.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 = {Aceto, L. and Bloom, B. and Vaandrager, F.},
title = {Turning SOS rules into equations},
booktitle = {Proceedings of the Seventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1992},
year = 1992,
editor = {Andre Scedrov},
month = {June},
pages = {113--124},
location = {Santa Cruz, CA, USA},
publisher = {IEEE Computer Society Press}
}