Quantifier elimination for counting extensions of Presburger arithmetic

We give a new quantifier elimination procedure for Presburger arithmetic extended with a unary counting quantifier there exists=x(y) Phi that binds to the variable x the number of different y satisfying Phi. While our procedure runs in non-elementary time in general, we show that it yields nearly optimal elementary complexity results for expressive counting extensions of Presburger arithmetic, such as the threshold counting quantifier there exists(>= c)y Phi that requires that the number of different y satisfying Phi be at least c is an element of N, where c can succinctly be defined by a Presburger formula. Our results are cast in terms of what we call the monadically-guarded fragment of Presburger arithmetic with unary counting quantifiers, for which we develop a 2ExPSPAcE decision procedure.