Bounds on the Automata Size for Presburger Arithmetic

Details Bounds on the Automata Size for Presburger Arithmetic Bounds on the Automata Size for Presburger Arithmetic

2005-06-02

arxiv.org/abs/cs/0506008v1

Computer Science

Logic in Computer Science

Scientific paper

Automata provide a decision procedure for Presburger arithmetic. However, until now only crude lower and upper bounds were known on the sizes of the automata produced by this approach. In this paper, we prove an upper bound on the the number of states of the minimal deterministic automaton for a Presburger arithmetic formula. This bound depends on the length of the formula and the quantifiers occurring in the formula. The 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 our bound is tight, even for nondeterministic automata. Moreover, we provide optimal automata constructions for linear equations and inequations.

Affiliated with

Also associated with

No associations

Rating

Bounds on the Automata Size for Presburger Arithmetic does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Bounds on the Automata Size for Presburger Arithmetic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Bounds on the Automata Size for Presburger Arithmetic will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-434759