Axiomatizing GSOS with Termination
J.C.M. Baeten and E.P. de Vink

We discuss a combination of GSOS-type structural operational semantics with
explicit termination, that we call the tagh-format (tagh being short for
termination and GSOS hybrid). The tagh-format distinguishes between transition
and termination rules, but, besides active and negative premises as in GSOS,
also allows for what we call terminating and passive arguments. We extend the
result of Aceto, Bloom and Vaandrager on the automatic generation of sound and
complete axiomatizations for GSOS to the setting of tagh-transition systems.
The construction of the equational theory is based upon the notion of a smooth
and distinctive operation, which have been generalized from GSOS to tagh. We
prove the soundness of the synthesized laws and show their completeness modulo
bisimulation.  The examples provided indicate a significant, though yet not
ideal, improvement over the axiomatization techniques known so~far.