Finite and infinite implementation of transition systems

Wim H. Hesselink; Gerard R. Renardel de Lavalette

doi:10.1016/j.tcs.2012.08.014

Finite and infinite implementation of transition systems

Wim H. Hesselink, Gerard R. Renardel de Lavalette

Fundamental Computing

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

324 Downloads (Pure)

Abstract

A system T is defined as implementing a system S if every infinite execution of T leads to the same observations as some infinite execution of S. System T implements S finitely if every finite execution of T leads to the same observations as some finite execution of S. It is proved that, under certain conditions on the implemented system, finite implementation implies implementation. The proof uses Konig's lemma. It is shown that the conditions are essential. (C) 2012 Elsevier B.V. All rights reserved.

Original language	English
Pages (from-to)	131-135
Number of pages	5
Journal	Theoretical Computer Science
Volume	458
DOIs	https://doi.org/10.1016/j.tcs.2012.08.014
Publication status	Published - 2-Nov-2012

Keywords

Transition system
Implementation
Stuttering
Konig's lemma
Model checking

Access to Document

10.1016/j.tcs.2012.08.014

2012ThCompSciHesselink.pdfFinal publisher's version, 238 KB

Handle.net

Persistent link

Cite this

@article{39ce5f9a5797474aac5de3cc1523ca98,

title = "Finite and infinite implementation of transition systems",

abstract = "A system T is defined as implementing a system S if every infinite execution of T leads to the same observations as some infinite execution of S. System T implements S finitely if every finite execution of T leads to the same observations as some finite execution of S. It is proved that, under certain conditions on the implemented system, finite implementation implies implementation. The proof uses Konig's lemma. It is shown that the conditions are essential. (C) 2012 Elsevier B.V. All rights reserved.",

keywords = "Transition system, Implementation, Stuttering, Konig's lemma, Model checking",

author = "Hesselink, {Wim H.} and {Renardel de Lavalette}, {Gerard R.}",

note = "Relation: http://www.rug.nl/fmns-research/bernoulli/index Rights: University of Groningen, Johann Bernoulli Institute for Mathematics and Computer Science",

year = "2012",

month = nov,

day = "2",

doi = "10.1016/j.tcs.2012.08.014",

language = "English",

volume = "458",

pages = "131--135",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier",

}

TY - JOUR

T1 - Finite and infinite implementation of transition systems

AU - Hesselink, Wim H.

AU - Renardel de Lavalette, Gerard R.

N1 - Relation: http://www.rug.nl/fmns-research/bernoulli/index Rights: University of Groningen, Johann Bernoulli Institute for Mathematics and Computer Science

PY - 2012/11/2

Y1 - 2012/11/2

N2 - A system T is defined as implementing a system S if every infinite execution of T leads to the same observations as some infinite execution of S. System T implements S finitely if every finite execution of T leads to the same observations as some finite execution of S. It is proved that, under certain conditions on the implemented system, finite implementation implies implementation. The proof uses Konig's lemma. It is shown that the conditions are essential. (C) 2012 Elsevier B.V. All rights reserved.

AB - A system T is defined as implementing a system S if every infinite execution of T leads to the same observations as some infinite execution of S. System T implements S finitely if every finite execution of T leads to the same observations as some finite execution of S. It is proved that, under certain conditions on the implemented system, finite implementation implies implementation. The proof uses Konig's lemma. It is shown that the conditions are essential. (C) 2012 Elsevier B.V. All rights reserved.

KW - Transition system

KW - Implementation

KW - Stuttering

KW - Konig's lemma

KW - Model checking

U2 - 10.1016/j.tcs.2012.08.014

DO - 10.1016/j.tcs.2012.08.014

M3 - Article

SN - 0304-3975

VL - 458

SP - 131

EP - 135

JO - Theoretical Computer Science

JF - Theoretical Computer Science

ER -

Finite and infinite implementation of transition systems

Abstract

Keywords

Access to Document

Handle.net

Fingerprint

Cite this