Bounds on the automata size for Presburger arithmetic

ABSTRACT

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 the automata-based approach for Presburger arithmetic. In this article, we give an upper bound on 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 it. We establish the upper bound by comparing the automata for Presburger arithmetic formulas with the formulas produced by a quantifier-elimination method. We show that our bound is tight, also for nondeterministic automata. Moreover, we provide automata constructions for atomic formulas and establish lower bounds for the automata for linear equations and inequations.

REFERENCES

• 1: Bardin, S., Finkel, A., Leroux, J., and Petrucci, L. 2003. FAST: Fast accelereation of symbolic transition systems. In Proceedings of the 15th International Conference on Computer-Aided Verification (CAV'03). Lecture Notes in Computer Science, vol. 2725. Springer-Verlag, New York, 118--121.
• 2: Bartzis, C. and Bultan, T. 2003. Efficient symbolic representations for arithmetic constraints in verification. Int. J. Found. Comput. Sci. 14, 4, 605--624.
• 3: Berman, L. 1980. The complexity of logical theories. Theor. Comput. Sci. 11, 71--77.
• 4: Achim Blumensath , Erich Grädel, Automatic Structures, Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, p.51, June 26-29, 2000
• 5: Boigelot, B. 1999. Symbolic methods for exploring infinite state spaces. Ph.D. dissertation, Faculté des Sciences Appliquées de l'Université de Liège, Liège, Belgium.
• 6: Bernard Boigelot , Sébastien Jodogne , Pierre Wolper, An effective decision procedure for linear arithmetic over the integers and reals, ACM Transactions on Computational Logic (TOCL), v.6 n.3, p.614-633, July 2005 [doi>10.1145/1071596.1071601]
• 7: Bernard Boigelot , Stéphane Rassart , Pierre Wolper, On the Expressiveness of Real and Integer Arithmetic Automata (Extended Abstract), Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.152-163, July 13-17, 1998
• 8: Bernard Boigelot , Pierre Wolper, Representing Arithmetic Constraints with Finite Automata: An Overview, Proceedings of the 18th International Conference on Logic Programming, p.1-19, July 29-August 01, 2002
• 9: Alexandre Boudet , Hubert Comon, Diophantine Equations, Presburger Arithmetic and Finite Automata, Proceedings of the 21st International Colloquium on Trees in Algebra and Programming, p.30-43, April 22-24, 1996
• 10: Bruyère, V., Hansel, G., Michaux, C., and Villemaire, R. 1994. Logic and p-recognizable sets of integers. Bull. Belg. Math. Soc. 1, 2, 191--238.
• 11: Brzozowski, J. A. and Leiss, E. L. 1980. On equations for regular languages, finite automata, and sequential networks. Theoret. Compu. Sci. 10, 1, 19--35.
• 12: Büchi, J. 1960. Weak second-order arithmetic and finite automata. Z. Math. Logik Grundlagen Math. 6, 66--92.
• 13: Ashok K. Chandra , Dexter C. Kozen , Larry J. Stockmeyer, Alternation, Journal of the ACM (JACM), v.28 n.1, p.114-133, Jan. 1981 [doi>10.1145/322234.322243]
• 14: Cobham, A. 1969. On the base-dependence of sets of numbers recognizable by finite automata. Math. Syst. Theory 3, 186--192.
• 15: Cooper, D. 1972. Theorem proving in arithmetic without multiplication. Mach. Intell. 7, 91--99.
• 16: Dixmier, J. 1990. Proof of a conjecture by Erdös and Graham concerning the problem of Frobenius. J. Numb. Theory 34, 2, 198--209.
• 17: Ferrante, J. and Rackoff, C. W. 1975. A decision procedure for the first order theory of real addition with order. SIAM J. Compu. 4, 1, 69--76.
• 18: Ferrante, J. and Rackoff, C. W. 1979. The Computational Complexity of Logical Theories. Lecture Notes in Mathematics, vol. 718. Springer-Verlag, New York.
• 19: Fischer, M. and Rabin, M. 1974. Super-exponential complexity of Presburger arithmetic. In Symposium on Applied Mathematics. SIAM-AMS Proceedings, vol. VII. 27--41.
• 20: Fischer, M. and Rabin, M. 1998. Super-exponential complexity of Presburger arithmetic. In Quantifier Elimination and Cylindrical Algebraic Decomposition, B. Caviness and J. Johnson, Eds. Texts and Monographs in Symbolic Computation. Springer-Verlag, New York, 122--135. (Reprint of the article {Fischer and Rabin 1974}).
• 21: Vijay Ganesh , Sergey Berezin , David L. Dill, Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.171-186, November 06-08, 2002
• 22: Erich Grädel, Subclasses of Presburger arithmetic and the polynomial-time hierarchy, Theoretical Computer Science, v.56 n.3, p.289-301, March, 1988 [doi>10.1016/0304-3975(88)90136-3 ]
• 23: Hopcroft, J. E. 1971. An n log n algorithm for minimizing the states in a finite automaton. In Proceedings of the International Symposium in Theory of Machines and Computations, (Technion, Israel Institute of Technology, Haifa, Israel), Z. Kohavi and A. Paz, Eds. Academic Press, Orlando, FL, 189--196.
• 24: Hopcroft, J. E. and Ullman, J. D. 1979. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading, MA.
• 25: Bakhadyr Khoussainov , Anil Nerode, Automatic Presentations of Structures, Selected Papers from the International Workshop on Logical and Computational Complexity, p.367-392, October 13-16, 1994
• 26: LASH. The Liège Automata-based Symbolic Handler. See the web-page http://www.montefiore.ulg.ac.be/~boigelot/research/lash/.
• 27: Oppen, D. 1978. A 2^22pn upper bound on the complexity of Presburger arithmetic. J. Comp. Syst. Sci. 16, 323--332.
• 28: Presburger, M. 1930. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Sprawozdanie z I Kongresu metematyków slowiańskich, Warszawa 1929. 92--101 and 395.
• 29: C. R. Reddy , D. W. Loveland, Presburger arithmetic with bounded quantifier alternation, Proceedings of the tenth annual ACM symposium on Theory of computing, p.320-325, May 01-03, 1978, San Diego, California, United States [doi>10.1145/800133.804361]
• 30: Klaus Reinhardt, The complexity of translating logic to finite automata, Automata logics, and infinite games: a guide to current research, Springer-Verlag New York, Inc., New York, NY, 2002
• 31: Rubin, S. 2004. Automatic structures. Ph.D. dissertation, University of Auckland, Auckland, New Zealand.
• 32: A decision procedure for term algebras with queues, ACM Transactions on Computational Logic (TOCL), v.2 n.2, p.155-181, April 2001 [doi>10.1145/371316.371494]
• 33: Rybina, T. and Voronkov, A. 2003. Upper bounds for a theory of queues. In Proceedings of the 30th International Colloquium on Automata, Languages and Programming (ICALP'03). Lecture Notes in Computer Science, vol. 2719. Springer-Verlag, New York, 714--724.
• 34: Schöning, U. 1997. Complexity of Presburger arithmetic with fixed quantifier dimension. Theory Comp. Syst. 30, 4, 423--428.
• 35: Semenov, A. 1977. Presburgerness of predicates regular in two number systems. Sib. Math. J. 18, 289--300.
• 36: Thomas R. Shiple , James H. Kukula , Rajeev K. Ranjan, A Comparison of Presburger Engines for EFSM Reachability, Proceedings of the 10th International Conference on Computer Aided Verification, p.280-292, June 28-July 02, 1998
• 37: Skolem, T. 1931. Über einige Satzfunktionen in der Arithmetik. In Skrifter utgitt av Det Norske Videnskaps-Akademi i Oslo, I. Matematisk naturvidenskapelig klasse. Vol. 7. Oslo, 1--28.
• 38: Skolem, T. 1970. Über einige Satzfunktionen in der Arithmetik. In Selected Works in Logic, J. Fenstad, Ed. Universitetsforlaget, Oslo, 281--306. (Reprint of the article {Skolem 1931}.)
• 39: Ryan Stansifer, Presburger''s Article on Integer Arithmetic: Remarks and Translation, Cornell University, Ithaca, NY, 1984
• 40: Stockmeyer, L. 1974. The complexity of decision problems in automata theory and logic. Ph.D. dissertation, Department of Electrical Engineering, MIT, Boston, MA.
• 41: Volker Weispfenning, Mixed real-integer linear quantifier elimination, Proceedings of the 1999 international symposium on Symbolic and algebraic computation, p.129-136, July 28-31, 1999, Vancouver, British Columbia, Canada [doi>10.1145/309831.309888]
• 42: Pierre Wolper , Bernard Boigelot, An Automata-Theoretic Approach to Presburger Arithmetic Constraints (Extended Abstract), Proceedings of the Second International Symposium on Static Analysis, p.21-32, September 25-27, 1995
• 43: Pierre Wolper , Bernard Boigelot, On the Construction of Automata from Linear Arithmetic Constraints, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.1-19, March 25-April 02, 2000
• 44: Yavuz-Kahveci, T., Bartzis, C., and Bultan, T. 2005. Action language verifier, extended. In Proceedings of the 17th International Conference on Computer Aided Verification (CAV'05). Lecture Notes in Computer Science, vol. 3576. Springer-Verlag, New York, 413--417.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computational logic

General Terms:
Algorithms, Theory

Keywords:
Automata-based decision procedures, Presburger arithmetic, complexity, quantifier elimination