LAUSR

State space techniques are one of the main approaches deployed for the analysis of concurrent systems. However, state space construction is stalled by a common phenomenon called the state explosion problem which makes it a tough task or even impossible when the state space computation demands prohibitive cost (time and memory). We limit general resource allocation systems (RASs) to a certain class whose state space can be hierarchically constructed, yet it comprises various enough types of real-world discrete event systems, such as automated manufacturing systems. This paper focuses on a class of RASs modeled with Petri nets (PNs), where, through pure algebraic operations, a novel method to compute the state spaces is proposed, which is motivated by the superposition property. Given a PN model of a system and a target resource configuration, we first propose a special initial marking called the initial basis marking and compute the corresponding reachability graph. Then, we increase the capacity of the resource places in an incremental way and generate the reachability graphs by taking advantage of the PN structure and the previously computed reachability graph until the capacity function of resources reaches the target resource configuration. A complete enumeration of reachable states can be obtained by a recursive scheme. Experimental studies also demonstrate the efficiency of the proposed approach in terms of computational cost and its high-potential to cope with the state-explosion problem.