Title :
A concurrency characteristic in Petri net unfolding
Author :
Hwang, Chang-Hee ; Lee, Dong-Ik
Author_Institution :
DACOM R&D Center, Taejon, South Korea
Abstract :
Unfolding, originally introduced by McMillan (1995), is gaining ground as a partial-order based method for the verification of concurrent systems without state-space explosion. However, it can be exposed to redundancy, which may increase its size exponentially. So far, there have been trials to reduce such redundancy resulting from conflicts by improving McMillan´s cut-off criterion. In this paper, we show that concurrency is also another cause of redundancy in unfolding, and we present an algorithm to reduce such redundancy in live, bounded and reversible Petri nets, which is independent of any cut-off algorithm
Keywords :
Petri nets; algorithm theory; distributed algorithms; formal verification; redundancy; search problems; state-space methods; Petri net unfolding; bounded Petri nets; concurrency characteristic; concurrent systems verification; cut-off criterion; live Petri nets; partial-order based method; redundancy reduction; reversible Petri nets; state-space explosion; Asynchronous circuits; Concurrent computing; Explosions; Interleaved codes; Petri nets; Research and development; State-space methods;
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.637370