A technique for generating the reduced reachability graph of petri net models

The reachability graph technology is the basic and important method of analysis and verification of a system but it suffers from state explosion problem. To cope with this problem, this paper introduces transition vectors which can detect all the enabled transitions at given state of system and identify them as dependent or independent. Transition vectors have been found useful and functional for simultaneous execution of concurrently enabled transitions. An efficient algorithm based on transition vectors has been presented to generate the reduced reachability graph and compared with the reduced reachability graph constructed by stubborn set method.