@inproceedings{862db5e1bb0c4abb88edbf55566238b4,
title = "Axiomatizing GSOS with termination",
abstract = "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 GSOSto 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 signifi- cant improvement over the mechanical axiomatization techniques known so far.",
author = "J.C.M. Baeten and \{Vink, de\}, E.P.",
year = "2002",
doi = "10.1007/3-540-45841-7\_48",
language = "English",
isbn = "3-540-43283-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "583--595",
editor = "H. Alt and A. Ferreira",
booktitle = "Proceedings 19th Annual Symposium on Theoretical Aspects of Computer Science (STACS 2002, Antibes - Juan-les-Pins, France, March 14-16, 2002)",
address = "Germany",
}