Ntyft/ntyxt Rules Reduce to Ntree Rules

Wan Fokkink; Rob Van Glabbeek

doi:10.1006/inco.1996.0030

Ntyft/ntyxt Rules Reduce to Ntree Rules

Wan Fokkink^*
, Rob Van Glabbeek

^*Corresponding author for this work

Research output: Contribution to Journal › Article › Academic › peer-review

Abstract

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 language	English
Pages (from-to)	1-10
Number of pages	10
Journal	Information and Computation
Volume	126
Issue number	1
DOIs	https://doi.org/10.1006/inco.1996.0030
Publication status	Published - 10 Apr 1996

Funding

* Current affiliation: Department of Philosophy, Utrecht University, Utrecht, The Netherlands. -This work was supported by ONR under Grant N00014-92-J-1974.

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 16 Peace, Justice and Strong Institutions

Access to Document

10.1006/inco.1996.0030

Persistent URL (handle)

Persistent link

Cite this

@article{8df7ab665da142aeb1776e65f5f81e14,

title = "Ntyft/ntyxt Rules Reduce to Ntree Rules",

abstract = "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.",

author = "Wan Fokkink and \{Van Glabbeek\}, Rob",

year = "1996",

month = apr,

day = "10",

doi = "10.1006/inco.1996.0030",

language = "English",

volume = "126",

pages = "1--10",

journal = "Information and Computation",

issn = "0890-5401",

publisher = "Elsevier Inc.",

number = "1",

}

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 - https://www.scopus.com/pages/publications/0002095573

UR - https://www.scopus.com/pages/publications/0002095573#tab=citedBy

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 -

Ntyft/ntyxt Rules Reduce to Ntree Rules

Abstract

Funding

UN SDGs

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this