The tyft/tyxt format reduces to tree rules

Willem Jan Fokkink*

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review


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.

Original languageEnglish
Title of host publicationTheoretical Aspects of Computer Software - International Symposium TACS 1994, Proceedings
EditorsJohn C. Mitchell, Masami Hagiya
PublisherSpringer - Verlag
Number of pages14
ISBN (Print)9783540578871
Publication statusPublished - 1 Jan 1994
Event2nd International Symposium on Theoretical Aspects of Computer Software, TACS 1994 - Sendai, Japan
Duration: 19 Apr 199422 Apr 1994

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume789 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference2nd International Symposium on Theoretical Aspects of Computer Software, TACS 1994


Dive into the research topics of 'The tyft/tyxt format reduces to tree rules'. Together they form a unique fingerprint.

Cite this