In: Journal of Research Practices and Information Technology, Vol. 32, No. 2, pages 131-143. 2000.
Abstract: Reachability graph analysis is one of the most widely used techniques to verify the behavior of asynchronous and concurrent systems modeled in Petri nets. Unfortunately, the state explosion problem is often an issue when applying Petri net modeling and analysis to large and complex industrial systems. The paper proposes an approach in which Petri net slices are computed based on structural concurrency inherent in the Pr/T net and compositional reachability graph analysis is performed. Petri net slices are proven to provide behavioral equivalence to P/T nets. This approach may enable verification of properties such as boundedness and liveness which may fail on unsliced P/T nets due to a state explosion problem. Effectiveness and scalability of the proposed approach is demonstrated using both dining philosophers and feature interaction problem found in telecommunication software.
Keywords: Petri nets, compositional reachability analysis, industrial applications, slicing-based approach.
Back to the Petri Nets Bibliography