DocumentCode
301467
Title
Decision problems related to structural induction for rings of Petri nets with fairness
Author
Li, Jianan ; Suzuki, Ichiro ; Yamashita, Masafumi
Author_Institution
Dept. of Electr. Eng. & Comput. Sci., Wisconsin Univ., Milwaukee, WI, USA
Volume
2
fYear
1995
fDate
22-25 Oct 1995
Firstpage
1436
Abstract
Structural induction is a technique for proving that a system consisting of many identical components works correctly regardless of the actual number of components it has. Previously the authors have obtained conditions under which structural induction goes through for rings that are modeled as a Petri net satisfying a fairness requirement. The conditions guarantee that for some k, all rings of size k or greater exhibit “similar” behavior. The key concept is the similarity between rings, where rings Rk and Rl of sizes k and l, respectively, are said to be similar if: none of the components in either ring can tell whether it is in Rk or R l, and none of the components (except possibly one) can tell its position within the ring to which it belongs. A ring satisfying this second property is said to be uniform. We prove the undecidability of various basic questions regarding similarity and uniformity. Some of the questions are shown to be undecidable regarding the existence of K such that: 1) Rk and Rk+1 are similar; 2) all rings of size k or greater are mutually similar; 3) Rk is uniform; and 4) Rk, Rk+1, Rk+2,... are all uniform?
Keywords
Petri nets; finite state machines; formal verification; inference mechanisms; temporal logic; Petri net rings; finite state machines; similarity; structural induction; topology; undecidability; Logic; Petri nets; Sufficient conditions; Topology;
fLanguage
English
Publisher
ieee
Conference_Titel
Systems, Man and Cybernetics, 1995. Intelligent Systems for the 21st Century., IEEE International Conference on
Conference_Location
Vancouver, BC
Print_ISBN
0-7803-2559-1
Type
conf
DOI
10.1109/ICSMC.1995.537974
Filename
537974
Link To Document