How to manage coverability graphs construction: an overview

To analyze the behavior of Petri nets, the reachability graph permits us to verify qualitative properties. However, even for small nets, the reachability graph can become infinite if the studied Petri net is unbounded. So, to deal with the state space explosion problem, the coverability graph must be used. The paper aims to expose the main ways of construction of coverability graphs and specifies how some qualitative properties can be checked in these different approaches.