Logic in Computer Science (LICS 2004)

Paper: From Automata to Formulas: Convex Integer Polyhedra (at LICS 2004)

Authors: Louis Latour

Abstract

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{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.

BibTeX

  @InProceedings{Latour-FromAutomatatoFormu,
    author = 	 {Louis Latour},
    title = 	 {From Automata to Formulas: Convex Integer Polyhedra},
    booktitle =  {Proceedings of the Nineteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2004},
    year =	 2004,
    editor =	 {Harald Ganzinger},
    month =	 {July}, 
    pages =      {120--129},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }