DocumentCode
1620436
Title
Temporal Petri nets and structural induction for rings of processes
Author
Li, Jianan ; Suzuki, Ichiro ; Yamashita, Masafumi
Author_Institution
Dept. of Electr. Eng. & Comput. Sci., Wisconsin Univ., Milwaukee, WI, USA
fYear
1992
Firstpage
377
Abstract
A structural induction theorem for rings consisting of an arbitrary number of identical components is presented. The components of a ring are modeled using a Petri net and a temporal logic formula. The theorem can be used to formally infer the correctness of a ring of any large size from the correctness of a ring having only a few components. The usefulness of the theorem is demonstrated using the example of token-passing mutual exclusion
Keywords
Petri nets; concurrency control; multiprocessing systems; protocols; temporal logic; concurrent processing systems; rings of processes; structural induction; temporal Petri nets; temporal logic formula; token-passing mutual exclusion; Automata; Automatic testing; Computer science; Independent component analysis; Logic; Petri nets; Sufficient conditions; Timing;
fLanguage
English
Publisher
ieee
Conference_Titel
Circuits and Systems, 1992., Proceedings of the 35th Midwest Symposium on
Conference_Location
Washington, DC
Print_ISBN
0-7803-0510-8
Type
conf
DOI
10.1109/MWSCAS.1992.271282
Filename
271282
Link To Document