The Ideal View on Rackoff's Coverability Technique

Abstract : Well-structured transition systems form a large class of infinite-state systems, for which safety verification is decidable thanks to a generic backward coverability algorithm. However, for several classes of systems, the generic upper bounds one can extract from the algorithm are far from optimal. In particular, in the case of vector addition systems (VAS) and several of their extensions, the known tight upper bounds were rather derived thanks to ad-hoc arguments based on Rackoff’s small witness property. We show how to derive the same bounds directly on the computations of the VAS instantiation of the generic backward coverability algorithm. This relies on a dual view of the algorithm using ideal decompositions of downwards-closed sets, which exhibits a key structural invariant in the VAS case. This reasoning offers a uniform setting for all well-structured transition systems, including branching ones, and we further apply it to several VAS extensions: we derive optimal upper bounds for coverability in branching and alternating VAS, matching the previously known results from the literature.
Type de document :
Communication dans un congrès
Mikołaj Bojańczyk; Sławomir Lasota; Igor Potapov. RP 2015 - 9th International Workshop on Reachability Problems, Sep 2015, Warsaw, Poland. Springer, 9328, pp.1--13, Lecture Notes in Computer Science. 〈10.1007/978-3-319-24537-9_8〉
Liste complète des métadonnées

Littérature citée [44 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01176755
Contributeur : Sylvain Schmitz <>
Soumis le : mercredi 21 juin 2017 - 20:41:15
Dernière modification le : samedi 24 juin 2017 - 01:09:20

Fichier

article.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Copyright (Tous droits réservés)

Identifiants

Citation

Ranko Lazić, Sylvain Schmitz. The Ideal View on Rackoff's Coverability Technique. Mikołaj Bojańczyk; Sławomir Lasota; Igor Potapov. RP 2015 - 9th International Workshop on Reachability Problems, Sep 2015, Warsaw, Poland. Springer, 9328, pp.1--13, Lecture Notes in Computer Science. 〈10.1007/978-3-319-24537-9_8〉. 〈hal-01176755v3〉

Partager

Métriques

Consultations de la notice

56

Téléchargements de fichiers

19