Abstract / Description of output
Groote and Vaandrager introduced the tyft/tyxt format for Transition System Specifications (TSSs), and established that for each TSS in this format that iswell-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 oftree rulesonly. As a corollary we can give an affirmative answer to an open question, namely whether 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.
Original language | English |
---|---|
Article number | 30 |
Number of pages | 10 |
Journal | Information and Computation |
Volume | 126 |
Issue number | 1 |
DOIs | |
Publication status | Published - 10 Apr 1996 |