Sciweavers

Share
CONCUR
2010
Springer

On the Use of Non-deterministic Automata for Presburger Arithmetic

8 years 9 months ago
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 nondeterministic 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.
Antoine Durand-Gasselin, Peter Habermehl
Added 24 Jan 2011
Updated 24 Jan 2011
Type Journal
Year 2010
Where CONCUR
Authors Antoine Durand-Gasselin, Peter Habermehl
Comments (0)
books