  Since 1969 \cite{C-MST69,S-SMJ77}, we know that any Presburger-definable set
\cite{P-PCM29} (a set of integer vectors satisfying a formula in the
first-order additive theory of the integers) can be represented by a
state-based symmbolic representation, called in this paper Finite Digit Vector
Automata (FDVA). Efficient algorithms for manipulating these sets have been
recently developed. However, the problem of deciding if a FDVA 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 FDVA represents a Presburger-definable set, and we
provide in this positive case a polynomial time algorithm that constructs a
Presburger-formula that defines the same set.
