DocumentCode
1029221
Title
A new structural induction theorem for rings of temporal Petri nets
Author
Li, Jianan ; Suzuki, Ichiro ; Yamashita, Masafumi
Author_Institution
Dept. of Electr. Eng. & Comput. Sci., Wisconsin Univ., Milwaukee, WI, USA
Volume
20
Issue
2
fYear
1994
fDate
2/1/1994 12:00:00 AM
Firstpage
115
Lastpage
126
Abstract
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
Keywords
Petri nets; formal verification; temporal logic; temporal reasoning; correctness; demand-driven token circulation; formal verification; identical components; rings; similar behavior; structural induction theorem; temporal Petri nets; temporal logic formula; Automata; Cybernetics; Formal verification; Logic; Petri nets; Sufficient conditions;
fLanguage
English
Journal_Title
Software Engineering, IEEE Transactions on
Publisher
ieee
ISSN
0098-5589
Type
jour
DOI
10.1109/32.265633
Filename
265633
Link To Document