Quantifier elimination for counting extensions of Presburger arithmetic

We give a new quantifier elimination procedure for Presburger arithmetic extended with a unary counting quantifier ∃=xyΦ that binds to the variable x the number of different y satisfying Φ. 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 ∃≥cyΦ that requires that the number of different y satisfying Φ be at least c∈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