Title :
Persistency and weak persistency in partial order based analysis
Author :
Hiraishi, Kunihiko
Author_Institution :
Sch. of Inf. Sci., Japan Adv. Inst. of Sci. & Technol., Ishikawa, Japan
Abstract :
The purpose of the paper is to show how the results of Petri net theory can be applied to analysis of concurrent systems. State space explosion is known as one of the serious problems in the verification of concurrent systems. We focus on the partial order method, which was proposed to overcome this problem. In this method, a partial order defined on the set of transitions is used to obtain a reduced state space that preserves various properties to be verified. We give an interpretation of the partial order method by means of the theory of persistency and weak persistency of Petri nets
Keywords :
Petri nets; parallel algorithms; program verification; Petri net theory; concurrent systems analysis; concurrent systems verification; partial order based analysis; partial order method; reduced state space; state space explosion; weak persistency; Bipartite graph; Explosions; Logic; Petri nets; State-space methods; System recovery;
Conference_Titel :
Systems, Man, and Cybernetics, 1997. Computational Cybernetics and Simulation., 1997 IEEE International Conference on
Conference_Location :
Orlando, FL
Print_ISBN :
0-7803-4053-1
DOI :
10.1109/ICSMC.1997.637373
