NTYFT NTYXT RULES REDUCE TO NTREE RULES

Groote and Vaandrager introduced the tyft/tyxt format for Transition S ystem 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 corol lary we can give an affirmative answer to an open question, namely whe ther the well-foundedness condition in the congruence theorem for tyft /tyxt can be dropped. These results extend to tyft/tyxt with negative premises and predicates. (C) 1996 Academic Press, Inc.