Abstract
Groote and Vaandrager [5] introduced the tyft/tyxt format for transition system specifications (TSSs), and established that for each TSS in this format that is well-founded, the strong bisimulation it induces is a congruence. In this paper, we construct for each TSS in tyft/tyxt format an equivalent TSS that consists of tree rules only. As a corollary we can give an affirmative answer to an open question, namely whether the well-foundedness condition in the Congruence Theorem of [5] can be dropped. These results extend to tyft/tyxt with negative premises and predicates.
Preview
Unable to display preview. Download preview PDF.
References
B. Bloom, S. Istrail, and A.R. Meyer. Bisimulation can't be traced: preliminary report. In Proceedings 15th ACM Symposium on Principles of Programming Languages, San Diego, California, pages 229–239, 1988.
J.C.M. Baeten and C. Verhoef. A congruence theorem for structured operational semantics with predicates. In E. Best, editor, Proceedings CONCUR 93, Hildesheim, LNCS 715, pages 477–492. Springer-Verlag, 1993.
R.J. van Glabbeek. Full abstraction in structural operational semantics. In M. Nivat, C. Rattray, T. Rus, and G. Scollo, editors, Proceedings 3rd AMAST Conference, Twente, The Netherlands, June 1993, Workshops in Computing, pages 77–84. Springer-Verlag, 1993.
J.F. Groote. Transition system specifications with negative premises. In J.C.M. Baeten and J.W. Klop, editors, Proceedings CONCUR 90, Amsterdam, LNCS 458, pages 332–341. Springer-Verlag, 1990.
J.F. Groote and F.W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100(2):202–260, 1992.
D.M.R. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, 5th GI Conference, LNCS 104, pages 167–183. Springer-Verlag, 1981.
G.D. Plotkin. A structural approach to operational semantics. Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.
R. de Simone. Higher-level synchronising devices in MEIJE-SCCS. Theoretical Computer Science, 37:245–267, 1985.
C. Verhoef. A congruence theorem for structured operational semantics with predicates and negative premises. Report CSN-93/18, Eindhoven University of Technology, Eindhoven, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fokkink, W.J. (1994). The tyft/tyxt format reduces to tree rules. In: Hagiya, M., Mitchell, J.C. (eds) Theoretical Aspects of Computer Software. TACS 1994. Lecture Notes in Computer Science, vol 789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57887-0_109
Download citation
DOI: https://doi.org/10.1007/3-540-57887-0_109
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57887-1
Online ISBN: 978-3-540-48383-0
eBook Packages: Springer Book Archive