From automata to formulas: convex integer polyhedra

Automata-based representations have recently been investigated as a tool for representing and manipulating sets of integer vectors. In this paper, we study some structural properties of automata accepting the encodings (most significant digit first) of the natural solutions of systems of linear Diophantine inequations, i.e., convex polyhedra in Nⁿ. Based on those structural properties, we develop an algorithm that takes as input an automaton and generates a quantifier-free formula that represents exactly the set of integer vectors accepted by the automaton. In addition, our algorithm generates the minimal Hilbert basis of the linear system. In experiments made with a prototype implementation, we have been able to synthesize in seconds formulas and Hilbert bases from automata with more than 10,000 states.