On the Construction of Automata from Linear Arithmetic Constraints Wolper and Boigelot (2000)

When encoded in a base r ≥ 2, a natural number is a word over the alphabet {0, . . . r−1}. A language or set of words thus represents a set of natural numbers. An obvious question to ask then is which sets of natural numbers correspond to the regular languages under this representation. Motivated by the need to represent sets of integer vectors in the context of the verification of infinite-state systems [BW94], an automata-based approach is being developed for linear integer (Presburger) arithmetic [WB95,Boi98]. The idea that Presburger arithmetic formulas can be represented by automata goes back at least to Bu ̈chi [Bu ̈c60], and has lead to nice characterization results for the finite-state representable sets of integer vectors [Cob69,Sem77,BHMV94]. The attractiveness of the approach is not so much for single-shot arithmetic decision problems for which more traditional decision procedures perform well [Pug92], but for situations in which represented sets are repeatedly manipulated and compared, as is necessary in verification. Indeed, minimized deterministic finite automata are a convenient normal form for arithmetic formulas, in a way similar to BDDs [Bry92] being a normal form for Boolean formulas.