Bounds on the Automata Size for Presburger Arithmetic

TL;DR

This paper establishes tight bounds on the size of automata for Presburger arithmetic formulas, linking automata complexity to formula length and quantifiers, and provides optimal automata constructions for linear equations.

Contribution

It introduces a precise upper bound on automata size for Presburger formulas and demonstrates its tightness, advancing understanding of automata-based decision procedures.

Findings

Derived an upper bound on automata states based on formula length and quantifiers.

Proved the bound is tight for nondeterministic automata.

Constructed optimal automata for linear equations and inequalities.

Abstract

Automata provide a decision procedure for Presburger arithmetic. However, until now only crude lower and upper bounds were known on the sizes of the automata produced by this approach. In this paper, we prove an upper bound on the the number of states of the minimal deterministic automaton for a Presburger arithmetic formula. This bound depends on the length of the formula and the quantifiers occurring in the formula. The upper bound is established by comparing the automata for Presburger arithmetic formulas with the formulas produced by a quantifier elimination method. We also show that our bound is tight, even for nondeterministic automata. Moreover, we provide optimal automata constructions for linear equations and inequations.