Computing the transitive closure of a union of affine integer tuple relations

Overview & Synopsis

This paper proposes a method to compute the transitive clo- sure of a union of a±ne relations on integer tuples. Within Presburger arithmetics, complete algorithms to compute the transitive closure exist for convex polyhedra only. In presence of non-convex relations, there ex- ist little but special cases and incomplete heuristics. We introduce a novel su±cient and necessary condition de¯ning a class of relations for which an exact computation is possible. Our method is immediately applica- ble to a wide area of symbolic computation problems. It is illustrated on representative examples and compared with state-of-the-art approaches.