The main technique to prove the triple exponential upper bound on the automata size was to relate deterministic word automata with the formulas constructed by a qe method
On the Automata Size for Presburger Arithmetic
LICS, pp.110-119, (2004)
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 ex...更多
下载 PDF 全文
- Presburger arithmetic (PA) is the first-order theory with addition and the ordering relation over the integers.
- These results are not needed for the upper bound on the minimal DWA for a PA formula.
- From Lemma 7, it follows that the minimal DWA representing Ø ℄ has at least Ø · Ø · states.
- Presburger arithmetic (PA) is the first-order theory with addition and the ordering relation over the integers
- PA contrasts with the upper bound on the automata size for the monadic second-order logic WS1S, or even WS1S with the ordering relation “ ” as a primitive but without quantification over monadic second-order variables
- In order to establish the upper bound on the automata size for PA, we give a detailed analysis of the deterministic word automaton (WA) for formulas by comparing the constructed WAs with the quantifier-free formulas produced by the quantifier elimination method in , which is an improvement of Cooper’s quantifier elimination method 
- We analyzed the automata-theoretic approach for deciding Presburger arithmetic and established a tight upper bound on the automata size
- The triple exponential upper bound on the automata size carries over when using the Ô’s complement representation
- The main technique to prove the triple exponential upper bound on the automata size was to relate deterministic word automata (DWA) with the formulas constructed by a qe method
- The authors give an upper bound of the size of the minimal DWA for a formula Ø · , where 3⁄4, ØÜ1⁄2
- The authors give an upper bound on the size of the minimal DWA for a quantifier-free formula.
- This upper bound depends on the maximal absolute value of the constants occurring in theequations of the formula, the homogeneous terms, and the divisibility relations.
- The size of the resultant DWA using the product construction is in the worst case the product of the number of states of the two DWAs. Note that the authors allow the con-
- The authors give an upper bound on the size of the minimal DWA for an arbitrary formula.
- The authors use Reddy and Loveland’s qe method since the produced formulas are “small” with respect to the following parameters on which the upper bound of the minimal DWA in Theorem 10 depends.
- Using the qe method naively to eliminate all quantifiers in a formula is insufficient to prove the upper bounds in Theorem 14.
- The authors prove the main result of the paper: The size of the minimal DWA for a formula is at most triple exponential in the length of the formula.
- Note that Ò ¿ and that the numbers of quantifiers, atomic formulas, and the maximal absolute integer in 3 are at most Ò.
- The size of a DWA representing a PA definable set can be exponentially smaller by interpreting the first letter as the least significant bit.
- Using the formulas defined in , which are used to describe Turing machines in PA, and using lower bounds on the BDD size for Ñ-bit multiplication , it is straightforward to show a similar lower bound for the least significant bit encoding as in Theorem 17.
- The main technique to prove the triple exponential upper bound on the automata size was to relate DWAs with the formulas constructed by a qe method.
- This technique can be used to prove upper bounds on the sizes of minimal automata for other logics that admit qe, and where the structures are automata representable [3, 21], i.
- The effect on the automata size of switching from a Ô’s complement representation to a Õ’s complement representation is open
- This work has been partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS)
- C. Bartzis and T. Bultan. Efficient symbolic representations for arithmetic constraints in verification. Int. J. Found. Comput. Sci., 14(4):605–624, 2003.
- L. Berman. The complexity of logical theories. Theor. Comput. Sci., 11:71–77, 1980.
- A. Blumensath and E. Gradel. Automatic structures. In LICS’00, pp. 51–62, 2000.
- B. Boigelot. Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Facultedes Sciences Appliquees de l’Universitede Liege, Liege, Belgium, 1999.
- B. Boigelot, S. Jodogne, and P. Wolper. On the use of weak automata for deciding linear arithmetic with integer and real veriables. In IJCAR’01, LNCS 2083, pp. 611–625, 2001.
- B. Boigelot, S. Rassart, and P. Wolper. On the expressiveness of real and integer arithmetic automata (extended abstract). In ICALP’98, LNCS 1443, pp. 152–163, 1998.
- A. Boudet and H. Comon. Diophantine equations, Presburger arithmetic and finite automata. In CAAP’96, LNCS 1059, pp. 30–43, 1996.
- R. Bryant. On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Trans. on Comp., 40:205– 213, 1991.
- J. Buchi. Weak second-order arithmetic and finite automata. Z. Math. Logik Grundlagen Math., 6:66–92, 1960.
- D. Cooper. Theorem proving in arithmetic without multiplication. Machine Intelligence, 7:91–99, 1972.
- J. Dixmier. Proof of a conjecture by Erdos and Graham concerning the problem of Frobenius. J. Number Theory, 34(2):198–209, 1990.
- H. Enderton. A Mathematical Introduction to Mathematical Logic. Academic Press, 1972.
- J. Ferrante and C. Rackoff. The Computational Complexity of Logical Theories. LNM 718. 1979.
- M. Fischer and M. Rabin. Super-exponential complexity of Presburger arithmetic. In Symp. appl. Math., volume VII of SIAM-AMS Proc., pp. 27–41, 1974.
- M. Fischer and M. Rabin. Super-exponential complexity of Presburger arithmetic. In B. Caviness and J. Johnson, editors, Quantifier elimination and cylindrical algebraic decomposition, Texts and Monographs in Symbolic Computation, pp. 122–135. 1998. Reprint of the article .
- C. Frougny. Representations of numbers and finite automata. Math. Syst. Theory, 25(1):37–60, 1992.
- C. Frougny. Numeration systems. In M. Lothaire, editor, Algebraic Combinatorics on Words, ch. 7. 2002.
- V. Ganesh, S. Berezin, and D. Dill. Deciding Presburger arithmetic by model checking and comparisons with other methods. In FMCAD’02, LNCS 2517, pp. 171–186, 2002.
- E. Gradel. Subclasses of Presburger arithmetic and the polynomial-time hierarchy. Theor. Comput. Sci., 56:289– 301, 1988.
- M. Hollander. Greedy numeration systems and regularity. Theory Comput. Syst., 31(2):111–133, 1998.
- B. Khoussainov and A. Nerode. Automatic presentations of structures. In LCC’94, LNCS 960, pp. 367–392, 1995.
- D. Oppen. A 3⁄43⁄43⁄4ÔÒupper bound on the complexity of Presburger arithmetic. J. Comput. Syst. Sci., 16:323–332, 1978.
- M. Presburger. Uber die Vollstandigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Sprawozdanie z I Kongresu metematykow slowianskich, Warszawa 1929, pp. 92– 101, 395, 1930.
- M. Presburger. On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation. History and Philosophy of Logic, 12(2):225– 233, 1991. English translation of the article  by D. Jacquette.
- C. Reddy and D. Loveland. Presburger arithmetic with bounded quantifier alternation. In STOC’78, pp. 320–325, 1978.
- K. Reinhardt. The complexity of translating logic to finite automata. In E. Gradel, W. Thomas, and T. Wilke, editors, Automata, Logics, and Infinite Games, LNCS 2500, ch. 13, pp. 231–238. 2002.
- T. Rybina and A. Voronkov. A decision procedure for term algebras with queues. ACM Trans. Comput. Log., 2(2):155– 181, 2001.
- T. Rybina and A. Voronkov. Upper bounds for a theory of queues. In ICALP’03, LNCS 2719, pp. 714–724, 2003.
- U. Schoning. Complexity of Presburger arithmetic with fixed quantifier dimension. Theory Comput. Syst., 30(4):423–428, 1997.
- J. Shallit. Numeration systems, linear recurrences, and regular sets. Inf. Comput., 113(2):331–347, 1994.
- T. Shiple, J. Kukula, and R. Ranjan. A comparison of Presburger engines for EFSM reachability. In CAV’98, LNCS 1427, pp. 280–292, 1998.
- T. Skolem. Uber einige Satzfunktionen in der Arithmetik. In Skrifter utgitt av Det Norske Videnskaps-Akademi i Oslo, I. Matematisk naturvidenskapelig klasse, volume 7, pp. 1–28, Oslo, 1931. Universitetsforlaget, Oslo, 1970. Reprint of the article .
-  R. Stansifer. Presburger’s article on integer arithmetic: Remarks and transl ation. Technical Report TR84-639, Department of Computer Science, Cornell University, Ithaca, NY, USA, 1984.
-  L. Stockmeyer. The complexity of decision problems in automata theory and logic. PhD thesis, Department of Electrical Engineering, MIT, Boston, MA, USA, 1974.
-  V. Weispfenning. Mixed real-integer linear quantifier elimination. In ISSAC’99, pp. 129–136, 1999.
-  P. Wolper and B. Boigelot. On the construction of automata from linear arithmetic constraints. In TACAS’00, LNCS 1785, pp. 1–19, 2000.