A new structural induction theorem for rings of temporal Petri nets

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-1 and k, k⩾5, under which all rings of size k-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