The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.02 - February (1994 vol.20)
pp: 115-126
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, I. Suzuki, M. Yamashita, "A New Structural Induction Theorem for Rings of Temporal Petri Nets", IEEE Transactions on Software Engineering, vol.20, no. 2, pp. 115-126, February 1994, doi:10.1109/32.265633
19 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool