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

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 allows besides active
and negative premises as in GSOS, also for, what is called 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 system
specifications.  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. The examples provided indicate a
significant improvement over the mechanical axiomatization techniques
known so far.