On Presburger arithmetic extended with modulo counting quantifiers?

Abstract. We consider Presburger arithmetic (PA) extended with mod-ulo counting quantifiers. We show that its complexity is essentially the same as that of PA, i.e., we give a doubly exponential space bound. This is done by giving and analysing a quantifier elimination procedure sim-ilar to Reddy and Loveland’s procedure for PA. We also show that the complexity of the automata-based decision procedure for PA with mod-ulo counting quantifiers has the same triple-exponential time complexity as the one for PA when using least significant bit first encoding.