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
Approaching the coverability problem continuously, Proceedings of TACAS 2016, vol.9636, pp.480-496, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01242916
Well behaved transition systems, Logical Methods in Computer Science, vol.13, issue.3, pp.1-19, 2017. ,
On selective unboundedness of VASS, J. Comput. Syst. Sci, vol.79, issue.5, pp.689-713, 2013. ,
Reduction and covering of infinite reachability trees, Information and Computation, vol.89, issue.2, pp.144-179, 1990. ,
The minimal coverability graph for Petri nets, Advances in Petri Nets, vol.674, pp.210-243, 1993. ,
Forward analysis for WSTS, part II: Complete WSTS, Logical Methods in Computer Science, vol.8, issue.4, pp.1-35, 2012. ,
A counter-example to the minimal coverability tree algorithm, Belgium, 2005. ,
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. ,
Parallel program schemata, J. Comput. Syst. Sci, vol.3, issue.2, pp.147-195, 1969. ,
Distance Between Mutually Reachable Petri Net Configurations, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02156549
Constructing minimal coverability sets, Fundamenta Informaticae, vol.143, issue.3-4, pp.393-414, 2016. ,
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
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
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
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
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))
,
,
, 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
,
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) ,