Issue No. 02 - February (1994 vol. 20)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.265633
<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>
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
J. Li, M. Yamashita and I. Suzuki, "A New Structural Induction Theorem for Rings of Temporal Petri Nets," in IEEE Transactions on Software Engineering, vol. 20, no. , pp. 115-126, 1994.