Model checking based on occurrence net graph

摘要

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 algorithm for occurrence nets. Moreover, our representation can be used to obtain a stuttering equivalent graph on which nexttime-less linear temporal formulae are verified.