TY - JOUR
T1 - Ntyft/ntyxt Rules Reduce to Ntree Rules
AU - Fokkink, Wan
AU - Van Glabbeek, Rob
PY - 1996/4/10
Y1 - 1996/4/10
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=0002095573&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0002095573&partnerID=8YFLogxK
U2 - 10.1006/inco.1996.0030
DO - 10.1006/inco.1996.0030
M3 - Article
AN - SCOPUS:0002095573
SN - 0890-5401
VL - 126
SP - 1
EP - 10
JO - Information and Computation
JF - Information and Computation
IS - 1
ER -