On the use of non-deterministic automata for Presburger arithmetic

Abstract

A well-known decision procedure for Presburger arithmetic uses deterministic finite-state automata. While the complexity of the decision procedure for Presburger arithmetic based on quantifier elimination is known (roughly, there is a double-exponential non-deterministic time lower bound and a triple exponential deterministic time upper bound), the exact complexity of the automata-based procedure was unknown. We show in this paper that it is triple-exponential as well by analysing the structure of the non-deterministic automata obtained during the construction. Furthermore, we analyse the sizes of deterministic and non-deterministic automata built for several subclasses of Presburger arithmetic such as disjunctions and conjunctions of atomic formulas. To retain a canonical representation which is one of the strengths of the use of automata we use residual finite-state automata, a subclass of non-deterministic automata. © 2010 Springer-Verlag.