AI帮你理解科学

AI 生成解读视频

AI抽取解析论文重点内容自动生成视频


pub
生成解读视频

AI 溯源

AI解析本论文相关学术脉络


Master Reading Tree
生成 溯源树

AI 精读

AI抽取本论文的概要总结


微博一下
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)

被引用40|浏览130
EI
下载 PDF 全文
引用
微博一下

摘要

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...更多

代码

数据

简介
  • 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 [25], which is an improvement of Cooper’s quantifier elimination method [10]
  • 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 [14], which are used to describe Turing machines in PA, and using lower bounds on the BDD size for Ñ-bit multiplication [8], 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.
    Google ScholarLocate open access versionFindings
  • L. Berman. The complexity of logical theories. Theor. Comput. Sci., 11:71–77, 1980.
    Google ScholarLocate open access versionFindings
  • A. Blumensath and E. Gradel. Automatic structures. In LICS’00, pp. 51–62, 2000.
    Google ScholarLocate open access versionFindings
  • B. Boigelot. Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Facultedes Sciences Appliquees de l’Universitede Liege, Liege, Belgium, 1999.
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • A. Boudet and H. Comon. Diophantine equations, Presburger arithmetic and finite automata. In CAAP’96, LNCS 1059, pp. 30–43, 1996.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • J. Buchi. Weak second-order arithmetic and finite automata. Z. Math. Logik Grundlagen Math., 6:66–92, 1960.
    Google ScholarLocate open access versionFindings
  • D. Cooper. Theorem proving in arithmetic without multiplication. Machine Intelligence, 7:91–99, 1972.
    Google ScholarLocate open access versionFindings
  • J. Dixmier. Proof of a conjecture by Erdos and Graham concerning the problem of Frobenius. J. Number Theory, 34(2):198–209, 1990.
    Google ScholarLocate open access versionFindings
  • H. Enderton. A Mathematical Introduction to Mathematical Logic. Academic Press, 1972.
    Google ScholarFindings
  • J. Ferrante and C. Rackoff. The Computational Complexity of Logical Theories. LNM 718. 1979.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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 [14].
    Google ScholarFindings
  • C. Frougny. Representations of numbers and finite automata. Math. Syst. Theory, 25(1):37–60, 1992.
    Google ScholarLocate open access versionFindings
  • C. Frougny. Numeration systems. In M. Lothaire, editor, Algebraic Combinatorics on Words, ch. 7. 2002.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • E. Gradel. Subclasses of Presburger arithmetic and the polynomial-time hierarchy. Theor. Comput. Sci., 56:289– 301, 1988.
    Google ScholarLocate open access versionFindings
  • M. Hollander. Greedy numeration systems and regularity. Theory Comput. Syst., 31(2):111–133, 1998.
    Google ScholarLocate open access versionFindings
  • B. Khoussainov and A. Nerode. Automatic presentations of structures. In LCC’94, LNCS 960, pp. 367–392, 1995.
    Google ScholarLocate open access versionFindings
  • D. Oppen. A 3⁄43⁄43⁄4ÔÒupper bound on the complexity of Presburger arithmetic. J. Comput. Syst. Sci., 16:323–332, 1978.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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 [23] by D. Jacquette.
    Google ScholarLocate open access versionFindings
  • C. Reddy and D. Loveland. Presburger arithmetic with bounded quantifier alternation. In STOC’78, pp. 320–325, 1978.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • T. Rybina and A. Voronkov. A decision procedure for term algebras with queues. ACM Trans. Comput. Log., 2(2):155– 181, 2001.
    Google ScholarLocate open access versionFindings
  • T. Rybina and A. Voronkov. Upper bounds for a theory of queues. In ICALP’03, LNCS 2719, pp. 714–724, 2003.
    Google ScholarLocate open access versionFindings
  • U. Schoning. Complexity of Presburger arithmetic with fixed quantifier dimension. Theory Comput. Syst., 30(4):423–428, 1997.
    Google ScholarLocate open access versionFindings
  • J. Shallit. Numeration systems, linear recurrences, and regular sets. Inf. Comput., 113(2):331–347, 1994.
    Google ScholarLocate open access versionFindings
  • T. Shiple, J. Kukula, and R. Ranjan. A comparison of Presburger engines for EFSM reachability. In CAV’98, LNCS 1427, pp. 280–292, 1998.
    Google ScholarLocate open access versionFindings
  • 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 [32].
    Google ScholarLocate open access versionFindings
  • [34] 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.
    Google ScholarFindings
  • [35] L. Stockmeyer. The complexity of decision problems in automata theory and logic. PhD thesis, Department of Electrical Engineering, MIT, Boston, MA, USA, 1974.
    Google ScholarFindings
  • [36] V. Weispfenning. Mixed real-integer linear quantifier elimination. In ISSAC’99, pp. 129–136, 1999.
    Google ScholarLocate open access versionFindings
  • [37] P. Wolper and B. Boigelot. On the construction of automata from linear arithmetic constraints. In TACAS’00, LNCS 1785, pp. 1–19, 2000.
    Google ScholarLocate open access versionFindings
您的评分 :
0

 

标签
评论
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科