In: Rozenberg, G.: Lecture Notes in Computer Science, Vol. 674; Advances in Petri Nets 1993, pages 210-243. Springer-Verlag, 1993.
Abstract: We present the unique minimal coverability graph for Petri nets. When the reachability graph of a Petri net is infinite, the minimal coverability graph allows us to decide the same problems as the well-known Karp-Miller graph: the Finite Reachability Tree Problem, the Finite Reachability Set Problem, the Boundedness Problem, the Quasi-Liveness Problem and the Regularity Problem. The algorithm given for computing the minimal coverability graph is based on a new optimization of the Karp and Miller procedure.
Keywords: Petri nets; decidability; Karp-Miller graph; minimal coverability graph; effective computation of the minimal coverability graph; verification of protocols.