Technical Report No. 239 - Abstract

Jochen Eisinger
Upper Bounds on the Automata Size for Integer and Mixed Real and Integer Linear Arithmetic

Automata-based decision procedures have proved to be a particularly useful tool for infinite-state model checking, where automata are used to represent sets of real and integer values. However, not all theoretical aspects of these decision procedures are completely understood. We establish triple exponential upper bounds on the automata size for FO(ℤ,+,<) and FO(ℝ,Z,+,<). While a similar bound for Presburger Arithmetic, i.e., FO(ℤ,+,<) was obtained earlier using a quantifier elimination based approach, the bound for FO(ℝ,Z,+,<) is novel. We define two graded back-and-forth systems, and use them to derive bounds on the automata size by establishing a connection between those systems and languages that can be described by formulas in the respective logics. With these upper bounds that match the known lower bounds, the theoretical background for automata-based decision procedures for linear arithmetics becomes more complete.