Transitive Closures of Affine Integer Tuple Relations and their Overapproximations
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.
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.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...