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
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;
Conference_Titel :
Circuits and Systems, 1992., Proceedings of the 35th Midwest Symposium on
Conference_Location :
Washington, DC
Print_ISBN :
0-7803-0510-8
DOI :
10.1109/MWSCAS.1992.271282
