Issue No. 02 - February (1994 vol. 20)

ISSN: 0098-5589

pp: 115-126

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.265633

ABSTRACT

<p>Presents a new structural induction theorem for rings consisting of identical components that are modeled using a Petri net and a temporal logic formula. The theorem gives a condition in terms of the behavior of the rings of sizes k/spl minus/1 and k, k/spl ges/5, under which all rings of size k/spl minus/1 or greater exhibit "similar" behavior. Using the example of demand-driven token circulation, we show how the theorem can be applied to formally infer the correctness of a ring of any large size from that of a ring having fewer components.</p>

INDEX TERMS

Petri nets; temporal logic; temporal reasoning; formal verification; structural induction theorem; rings; temporal Petri nets; identical components; temporal logic formula; similar behavior; demand-driven token circulation; correctness; formal verification

CITATION

Jianan Li, M. Yamashita, I. Suzuki, "A New Structural Induction Theorem for Rings of Temporal Petri Nets",

*IEEE Transactions on Software Engineering*, vol. 20, no. , pp. 115-126, February 1994, doi:10.1109/32.265633