Turning SOS Rules into Equations

Many process algebras are defined by structural operational semantics (SOS). Indeed, most such definitions are nicely structured and fit the GSOS format of Bloom et al. (J. Assoc. Comput. Mach. , to appear). We give a procedure for converting any GSOS language definition to a finite complete equational axiom system (possibly with one infinitary induction principle) which precisely characterizes strong bisimulation of processes.

Authors

• L. Aceto
• B. Bloom
• F. Vaandrager

Keywords

No keywords are indexed for this paper.