M. Blockelet and S. Schmitz, Model checking coverability graphs of vector addition systems, Proceedings of MFCS 2011, vol.6907, pp.108-119, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00600077

M. Blondin, A. Finkel, C. Haase, and S. Haddad, Approaching the coverability problem continuously, Proceedings of TACAS 2016, vol.9636, pp.480-496, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01242916

M. Blondin, A. Finkel, and P. Mckenzie, Well behaved transition systems, Logical Methods in Computer Science, vol.13, issue.3, pp.1-19, 2017.

S. Demri, On selective unboundedness of VASS, J. Comput. Syst. Sci, vol.79, issue.5, pp.689-713, 2013.

A. Finkel, Reduction and covering of infinite reachability trees, Information and Computation, vol.89, issue.2, pp.144-179, 1990.

A. Finkel, The minimal coverability graph for Petri nets, Advances in Petri Nets, vol.674, pp.210-243, 1993.

A. Finkel and J. Goubault-larrecq, Forward analysis for WSTS, part II: Complete WSTS, Logical Methods in Computer Science, vol.8, issue.4, pp.1-35, 2012.

A. Finkel, G. Geeraerts, J. F. Raskin, and L. Van-begin, A counter-example to the minimal coverability tree algorithm, Belgium, 2005.

G. Geeraerts, J. F. Raskin, and L. Van-begin, On the efficient computation of the minimal coverability set of Petri nets, International Journal of Fundamental Computer Science, vol.21, issue.2, pp.135-165, 2010.

R. M. Karp and R. E. Miller, Parallel program schemata, J. Comput. Syst. Sci, vol.3, issue.2, pp.147-195, 1969.

J. Leroux, Distance Between Mutually Reachable Petri Net Configurations, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02156549

A. Piipponen and A. Valmari, Constructing minimal coverability sets, Fundamenta Informaticae, vol.143, issue.3-4, pp.393-414, 2016.

P. A. Reynier and F. Servais, Minimal coverability set for Petri nets: Karp and Miller algorithm with pruning, Fundamenta Informaticae, vol.122, issue.1-2, pp.1-30, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00554919

P. A. Reynier and F. Servais, On the computation of the minimal coverability set of petri nets, Proceedings of Reachability Problems 2019, vol.11674, pp.164-177, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02442611

A. Valmari and H. Hansen, Old and new algorithms for minimal coverability sets, Fundamenta Informaticae, vol.131, issue.1, pp.1-25, 2014.

, Assume the assertions of the lemma are satisfied. Denote by CT = (V , E , ? , ? ) and Front , the value of variables CT and Front after performing Delete(u) on CT

F. V-=-v-\-{u} and . {u}, We split the proof in two cases: ? There exists w ? V \ Front with ?(w) ? m * -If w = u then w ? V \ Front . Since ? (w) = ?(w), m * is still quasi-covered. -If w = u then there exists v such that ? (v) = ?(v) ? ?(u). Therefore, if v / ? Front then m * is still quasi-covered. Otherwise since ?(V \ Front) is an antichain, for all v / ? Front ?(v ) ? ?(u) implying ?(v ) ? ?(v). Therefore, the sequence ?(v) ? ?? ?(v) ? m * , is an exploring sequence. ? i ? Acc * . -Assume w = u. Since (1) for all 0 ? i ? k, there does not exist v ? V \ Front such that ?(w) + C(? 0 t 1 ? 1 . . . t i ? i ) ? ?(v ), (2) V \ Front ? V \ Front, and (3) ? (w) = ?(w), m ? ?? m is still an exploring sequence. -Assume w = u. Since ?(v) ? ?(u) = ?(u) + C(? 0 ) then v ? Front: otherwise it would contradict the definition of an exploring sequence, Let m * ? Cov(N , m 0 ). Thus m * is quasi-covered. By definition

, Front and Acc be the values of corresponding variables at some execution point of MinCov

, All m ? Cover(N , m 0 ) are quasi-covered

, \ Front) is an antichain

, Then all m ? Cover(N , m 0 ) are quasi-covered after performing Prune(u) and then adding u to Front

. Proof, . Let-u-?-v-.-denote, =. Ct-=-(v-,-e-,-?-,-?-)-;-v-\-front, and . V-\, and Front the value CT after performing Prune(u) on CT and adding u to Front. Assume that the assertions of the Lemma hold. If u ? Front then CT = CT and we are done. So let us assume that u / ? Front. Due to the definition of Prune

, Moreover, for all v ? V , ? (v) = ?(v)

, Thus m * is quasi-covered. We split the proof in two cases, Let m * ? Cov(N , m 0 )

, All m ? Cover(N , m 0 ) are quasi-covered

, \ Front) is an antichain

, For all v ? V \ {r}, ?(prd(v))

. ?-??????-?-?,

. Delete,

, All m ? Cover(N , m 0 ) are quasi-covered

, \ Front) is an antichain

, The second and third assertions of the conclusion are still satisfied since we do no add vertices and edges. So let us establish that all m ? Cover(N , m 0 ) are still quasi-covered

, ? There exists w ? V \ Front with ?(w) ? m * . -Assume that w is not a descendant of u . Since w is not a descendant of u , w is still in V \ Front

, All m ? Cover(N , m 0 ) are quasi-covered

, \ Front) ? {?(u)} is an antichain

, Then after removing u from Front and for all t ? T fireable from ?(u), adding a child v t to u in Front with marking of v t defined by ? u (v t ) = ?(u) + C(t)

, ? , ? ) and Front the value of variables CT and Front after removing u from Front and for all

+. ,

. Let-m-*-?-cov, Due to the assertions of the lemma, m * is quasi-covered. By definition, V \ Front = (V \ Front) ? {u}. We split the proof in two cases: ? There exists w ? V \ Front with ?(w) ? m * . Since only u has been added to V \ Front and ?(u) is incomparable to any ?(w), m is still quasi-covered. ? i ? Acc * . -Either there does not exist i ? k such that ?(w) + C(? 0 t 1 ? 1 · · · t i ? i ) ? ?(u)