Axiomatizing GSOS with termination

Aceto, Bloom and Vaandrager showed for the GSOS-format how to generate sound and complete axiomatizations. We add to the GSOS-format a notion of termination and adapt the axiomatization technique for this setting. The result is twofold: successful termination and deadlock are treated separately; the resulting axiom systems are in several cases more appealing.  

hosted by