Ntyft/ntyxt Rules Reduce to Ntree Rules

Wan Fokkink*, Rob Van Glabbeek

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review


Groote and Vaandrager introduced the tyft/tyxt format for Transition System Specifications (TSSs), and established that for each TSS in this format that is well-founded, the bisimulation equivalence 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-founded ness condition in the congruence theorem for tyft/tyxt can be dropped. These results extend to tyft/tyxt with negative premises and predicates.

Original languageEnglish
Pages (from-to)1-10
Number of pages10
JournalInformation and Computation
Issue number1
Publication statusPublished - 10 Apr 1996


Dive into the research topics of 'Ntyft/ntyxt Rules Reduce to Ntree Rules'. Together they form a unique fingerprint.

Cite this