33 . Ntyft/ntyxt Rules Reduce to Ntree Rules

W.J. Fokkink (CWI) & R.J. van Glabbeek (Stanford)

February 1995

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-foundedness condition in the congruence theorem for tyft/tyxt can be dropped. These results extend to tyft/tyxt with negative premises and predicates.

KEYWORDS: Concurrency, labelled transition systems, structural operational semantics, bisimulation.

Report STAN-CS-TN-95-17 and CWI report CS-R9508.
Available at ftp://Boole.stanford.edu/pub/DVI/tree.dvi.gz, ftp://Boole.stanford.edu/pub/PS/tree.ps.gz and ftp://Boole.stanford.edu/pub/TEX/tree.tex.gz.
To appear in Information and Computation.