The Community for Technology Leaders
Green Image
<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
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
88 ms
(Ver 3.3 (11022016))