inria-00578052, version 1
Transitive Closures of Affine Integer Tuple Relations and their Overapproximations
Sven Verdoolaege 1Albert Cohen
1Anna Beletska 1
N° RR-7560 (2011)
Résumé : The set of paths in a graph is an important concept with many applications in system analysis. In the context of integer tuple relations, which can be used to represent possibly infinite graphs, this set corresponds to the transitive closure of the relation. Relations described using only affine constraints and projection are fairly efficient to use in practice and capture Presburger arithmetic. Unfortunately, the transitive closure of such a quasi-affine relation may not be quasi-affine and so there is a need for approximations. In particular, most applications in system analysis require overapproximations. Previous work has mostly focused either on underapproximations or special cases of affine relations. We present a novel algorithm for computing overapproximations of transitive closures for the general case of quasi-affine relations (convex or not). Experiments on non-trivial relations from real-world applications show our algorithm to be on average more accurate and faster than the best known alternatives.
- 1 : ALCHEMY (INRIA Saclay - Ile de France)
- INRIA – CNRS : UMR8623 – Université Paris XI - Paris Sud
- Domaine : Informatique/Calcul formel
Informatique/Algorithme et structure de données
Informatique/Calcul parallèle, distribué et partagé
Informatique/Théorie et langage formel
- Mots-clés : affine integer tuple relation – dependence graph – Floyd-Warshall – maximal reaching path length – polyhedral model – strongly connected components – transitive closure
- Référence interne : RR-7560
- inria-00578052, version 1
- http://hal.inria.fr/inria-00578052
- oai:hal.inria.fr:inria-00578052
- Contributeur : Sven Verdoolaege
- Soumis le : Vendredi 18 Mars 2011, 11:16:32
- Dernière modification le : Vendredi 18 Mars 2011, 11:19:42