Fair Petri nets and structural induction for rings of processes

Jianan Li, Ichiro Suzuki, Masafumi Yamashita

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

We present a structural induction theorem for rings consisting of an arbitrary number of identical components. The components of a ring are modeled using a "fair Petri net," in which the firing of a prespecified set of transitions is assumed to occur fairly, i.e., any of these transitions that becomes firable infinitely often must fire infinitely often. Specifically, we introduce the concept of similarity between rings of different sizes, and give a condition under which the similarity between the rings of sizes two and three guarantees the similarity among the rings of all sizes. So if the given condition is satisfied, then the correctness of a ring of any large size can be inferred from the correctness of a ring having only a few components. The usefulness of the theorem is demonstrated using the examples of token-passing mutual exclusion and a simple producer-consumer system.

Original languageEnglish
Pages (from-to)377-404
Number of pages28
JournalTheoretical Computer Science
Volume135
Issue number2
DOIs
Publication statusPublished - Dec 12 1994

Fingerprint

Petri nets
Petri Nets
Proof by induction
Fires
Ring
Correctness
Mutual Exclusion
Theorem
Arbitrary
Similarity

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Fair Petri nets and structural induction for rings of processes. / Li, Jianan; Suzuki, Ichiro; Yamashita, Masafumi.

In: Theoretical Computer Science, Vol. 135, No. 2, 12.12.1994, p. 377-404.

Research output: Contribution to journalArticle

Li, Jianan ; Suzuki, Ichiro ; Yamashita, Masafumi. / Fair Petri nets and structural induction for rings of processes. In: Theoretical Computer Science. 1994 ; Vol. 135, No. 2. pp. 377-404.
@article{704c29c355814f3495a23ac89bc8c5be,
title = "Fair Petri nets and structural induction for rings of processes",
abstract = "We present a structural induction theorem for rings consisting of an arbitrary number of identical components. The components of a ring are modeled using a {"}fair Petri net,{"} in which the firing of a prespecified set of transitions is assumed to occur fairly, i.e., any of these transitions that becomes firable infinitely often must fire infinitely often. Specifically, we introduce the concept of similarity between rings of different sizes, and give a condition under which the similarity between the rings of sizes two and three guarantees the similarity among the rings of all sizes. So if the given condition is satisfied, then the correctness of a ring of any large size can be inferred from the correctness of a ring having only a few components. The usefulness of the theorem is demonstrated using the examples of token-passing mutual exclusion and a simple producer-consumer system.",
author = "Jianan Li and Ichiro Suzuki and Masafumi Yamashita",
year = "1994",
month = "12",
day = "12",
doi = "10.1016/0304-3975(94)90113-9",
language = "English",
volume = "135",
pages = "377--404",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "2",

}

TY - JOUR

T1 - Fair Petri nets and structural induction for rings of processes

AU - Li, Jianan

AU - Suzuki, Ichiro

AU - Yamashita, Masafumi

PY - 1994/12/12

Y1 - 1994/12/12

N2 - We present a structural induction theorem for rings consisting of an arbitrary number of identical components. The components of a ring are modeled using a "fair Petri net," in which the firing of a prespecified set of transitions is assumed to occur fairly, i.e., any of these transitions that becomes firable infinitely often must fire infinitely often. Specifically, we introduce the concept of similarity between rings of different sizes, and give a condition under which the similarity between the rings of sizes two and three guarantees the similarity among the rings of all sizes. So if the given condition is satisfied, then the correctness of a ring of any large size can be inferred from the correctness of a ring having only a few components. The usefulness of the theorem is demonstrated using the examples of token-passing mutual exclusion and a simple producer-consumer system.

AB - We present a structural induction theorem for rings consisting of an arbitrary number of identical components. The components of a ring are modeled using a "fair Petri net," in which the firing of a prespecified set of transitions is assumed to occur fairly, i.e., any of these transitions that becomes firable infinitely often must fire infinitely often. Specifically, we introduce the concept of similarity between rings of different sizes, and give a condition under which the similarity between the rings of sizes two and three guarantees the similarity among the rings of all sizes. So if the given condition is satisfied, then the correctness of a ring of any large size can be inferred from the correctness of a ring having only a few components. The usefulness of the theorem is demonstrated using the examples of token-passing mutual exclusion and a simple producer-consumer system.

UR - http://www.scopus.com/inward/record.url?scp=0028730440&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0028730440&partnerID=8YFLogxK

U2 - 10.1016/0304-3975(94)90113-9

DO - 10.1016/0304-3975(94)90113-9

M3 - Article

AN - SCOPUS:0028730440

VL - 135

SP - 377

EP - 404

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 2

ER -