Transitive Closures of Affine Integer Tuple Relations and their Overapproximations

Sven Verdoolaege 1 Albert Cohen 1 Anna Beletska 1
1 ALCHEMY - Architectures, Languages and Compilers to Harness the End of Moore Years
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, CNRS - Centre National de la Recherche Scientifique : UMR8623, Inria Saclay - Ile de France
Résumé : L'ensemble des chemins dans un graphe joue un rôle important pour de nombreuses applications dans le domaine de l'analyse des systèmes. Dans le cas des relations entre tuples d'entiers, lesquelles permettent de représenter des graphes potentiellement infinis, cet ensemble correspond à la clôture transitive de la relation. Lorsque ces relations sont décrites uniquement à l'aide de contraintes affines et de projections, elles ont la puissance d'expression de l'arithmétique de Presburger, et elles donnent lieu à des algorithmes relativement efficaces en pratique. Malheureusement, la clôture transitive d'une telle relation quasi-affine n'est pas forcément quasi-affine, impliquant le recours à des approximations. En particulier, la plupart des applications à l'analyse des systèmes requiert des sur-approximations. Les résultats antérieurs se concentrent soit sur des sous-approximations soit sur des cas particuliers de relations affines. Nous proposons un nouvel algorithme pour le calcul de sur-approximations de clôtures transitives, dans le cas général des relations quasi-affines (convexes ou non). Nos résultats expérimentaux portent sur des relations non-triviales issues d'applications réelles, et démontrent que notre algorithme est plus précis et plus rapide en moyenne que les meilleures alternatives connues.
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00578052
Contributeur : Sven Verdoolaege <>
Soumis le : vendredi 18 mars 2011 - 11:16:32
Dernière modification le : jeudi 5 avril 2018 - 12:30:12
Document(s) archivé(s) le : jeudi 8 novembre 2012 - 12:10:16

Fichier

RR-7560.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00578052, version 1

Collections

Citation

Sven Verdoolaege, Albert Cohen, Anna Beletska. Transitive Closures of Affine Integer Tuple Relations and their Overapproximations. [Research Report] RR-7560, INRIA. 2011. 〈inria-00578052〉

Partager

Métriques

Consultations de la notice

403

Téléchargements de fichiers

226