In: Gotzhein, R.; Bredereke, J.: Formal Description Techniques IX Theory, application and tools, International Conference, Kaiserslautern, Germany, Oct. 8-11, 1996, pages 380-395. London: Chapman & Hall, 1996.
Abstract: The computation of a reachability graph is one of the most used method to check system properties. Its main drawback is the state explosion. Two different approaches are generally used to tackle this problem: by defining new concise graph representations for which verification methods are adapted; by reducing graphs while preserving observed properties. We propose a new representation of a reachability graph where nodes are particular Petri nets, occurrence nets, characterizing parts of the state space. Checking invariant properties can be done using efficient algorithms for occurrence nets. Moreover, our representation can be used to obtain a stuttering equivalent graph on which nexttime-less linear temporal formulae are verifed.