A concurrency characteristic in Petri net unfolding

Author

Hwang, Chang-Hee ; Lee, Dong-Ik

Author_Institution

DACOM R&D Center, Taejon, South Korea

Volume

5

fYear

1997

fDate

12-15 Oct 1997

Firstpage

4266

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Systems, Man, and Cybernetics, 1997. Computational Cybernetics and Simulation., 1997 IEEE International Conference on

Conference_Location

Orlando, FL

ISSN

1062-922X

Print_ISBN

0-7803-4053-1

Type

conf

DOI

10.1109/ICSMC.1997.637370

Filename

637370