Abstract J.C.M. Baeten and E.P. de Vink
Axiomatizing GSOS with Termination
Technical Report CSR 01-06, Technische Universiteit Eindhoven, 2001


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 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.