Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Nineteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 2004)

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

Winner of the Kleene Award in 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 Symposium on Logic in Computer Science (LICS 2004)},
    year =	 {2004},
    month =	 {July}, 
    pages =      {110--119},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2017-04-0512:37
Andrzej Murawski