In: Proc. IEEE Int. Conf. on Systems, Man, and Cybernetics (SMC'98), 11-14 October 1998, San Diego, CA, pages 541-546. 1998.
Abstract: To analyze the behavior of Petri nets, the reachability graph permits to verify qualitative properties. However, even for small nets, the reachability graph can become infinite if the analyzed Petri net is unbounded. So, to deal with the state space explosion problem, the coverability graph must be used. This paper aims to expose the main ways of constructing coverability graphs and specifies how some qualitative properties can be checked using these different approaches.
Keywords: Petri nets, coverability graphs, reachability analysis.