A polynomial time Presburger criterion and synthesis for number decision diagrams

Number decision diagrams (NDD) are the automata-based symbolic representation for manipulating sets of integer vectors encoded as strings of digit vectors (least or most significant digit first). Since 1969 (A. Cobham, 1969, A. Semenov, 1977), we know that any Presburger-definable set (M. Presburger, 1929) (a set of integer vectors satisfying a formula in the first-order additive theory of the integers) can be represented by a NDD, and efficient algorithm for manipulating these sets have been recently developed (P. Wolper et al., 2000, A. Boudet et al., 1996). However, the problem of deciding if a NDD represents such a set, is a well-known hard problem first solved by Muchnik in 1991 with a quadruply-exponential time algorithm. In this paper, we show how to determine in polynomial time whether a NDD represents a Presburger-definable set, and we provide in this positive case a polynomial time algorithm that constructs from the NDD a Presburger-formula that defines the same set.