Title :
Structural induction for rings using temporal Petri nets
Author :
Li, Jianan ; Suzuki, Ichiro ; Yamashita, Masafumi
Author_Institution :
Dept. of Electr. Eng. & Comput. Sci., Wisconsin Univ., Milwaukee, WI, USA
Abstract :
The authors present a novel structural induction theorem for rings consisting of identical components that 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 fewer components.. The use of the theorem is illustrated using the problem of demand-driven token circulation
Keywords :
Petri nets; finite state machines; temporal logic; temporal reasoning; concurrent systems; demand-driven token circulation; finite state machines; rings; structural induction; temporal Petri nets; temporal logic; temporal reasoning; Automata; Computer science; Independent component analysis; Logic; Petri nets; Sufficient conditions;
Conference_Titel :
Systems, Man and Cybernetics, 1992., IEEE International Conference on
Conference_Location :
Chicago, IL
Print_ISBN :
0-7803-0720-8
DOI :
10.1109/ICSMC.1992.271546
