Logic in Computer Science (LICS 2004)

Paper: On the Automata Size for Presburger Arithmetic (at LICS 2004)

Authors: Felix Klaedtke

Abstract

Automata provide an effective mechanization of decision procedures for Presburger arithmetic. However, only crude lower and upper bounds are known on the sizes of the automata produced by this approach. In this paper, we prove that the number of states of the minimal deterministic automaton for a Presburger arithmetic formula is triple exponentially bounded in the length of the formula. This 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 this triple exponential bound is tight (even for nondeterministic automata). Moreover, we provide optimal automata constructions for linear equations and inequations.

BibTeX

  @InProceedings{Klaedtke-OntheAutomataSizefo,
    author = 	 {Felix Klaedtke},
    title = 	 {On the Automata Size for Presburger Arithmetic},
    booktitle =  {Proceedings of the Nineteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2004},
    year =	 2004,
    editor =	 {Harald Ganzinger},
    month =	 {July}, 
    pages =      {110--119},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }