Deadlock detection-oriented unfolding of unbounded Petri nets

摘要

The state-space explosion obstructs Petri nets for large-scale system analysis. Net unfolding techniques have drawn considerable attention to solve this problem. However, existing techniques are not suitable for deadlock detection of unbounded Petri nets. To address this issue, this paper presents a deadlock detection-oriented unfolding ((DU)-U-2) technique toward unbounded nets. (DU)-U-2 has the following advantages over traditional methods of solving deadlock detection problems: (1) Each configuration-corresponding cyclic or acyclic transition sequence in (DU)-U-2 is firable from the initial marking: (2) (DU)-U-2 can completely decide the existence of deadlocks when some conditions are met: and (3) (DU)-U-2 contains no spurious markings, unlike traditional unfolding techniques of unbounded Petri nets. The construction method and applications of (DU)-U-2 to deadlock detection of unbounded nets are presented. (C) 2019 Elsevier Inc. All rights reserved.