Abstract: Reachability graph (RG) generation suffers from the
problem of exponential space and time complexity. To alleviate the
more critical problem of time complexity, this paper presents the new
approach for RG generation for the Petri net (PN) models of parallel
processes. Independent RGs for each parallel process in the PN
structure are generated in parallel and cross-product of these RGs
turns into the exhaustive state space from which the RG of given
parallel system is determined. The complexity analysis of the
presented algorithm illuminates significant decrease in the time
complexity cost of RG generation. The proposed technique is
applicable to parallel programs having multiple threads with the
synchronization problem.