Abstract
We present a new way of using Binary Decision Diagrams in automata based algorithms for solving the satisfiability problem of quantifier-free Presburger arithmetic. Unlike in previous approaches [5,2,19], we translate the satisfiability problem into a model checking problem and use the existing BDD-based model checker SMV [13] as our primary engine.
We also compare the performance of various Presburger tools, based on both automata and ILP approaches, on a large suite of parameterized randomly generated test cases. The strengths and weaknesses of each approach as a function of these parameters are reported, and the reasons for the same are discussed. The results show that no single tool performs better than the others for all the parameters.
On the theoretical side, we provide tighter bounds on the number of states of the automata.
This research was supported by GSRC contract SA2206-23106PG-2 and in part by National Science Foundation CCR-9806889-002. The content of this paper does not necessarily reflect the position or the policy of GSRC, NSF, or the Government, and no official endorsement should be inferred.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Tod Amon, Gaetano Borriello, Taokuan Hu, and Jiwen Liu. Symbolic timing verification of timing diagrams using Presburger formulas. In Design Automation Conference, pages 226–231, 1997.
Alexandre Boudet and Hubert Comon. Diophantine equations, Presburger arithmetic and finite automata. In H. Kirchner, editor, Colloquium on Trees in Algebra and Programming (CAAP’96), volume 1059 of Lecture Notes in Computer Science, pages 30–43. Springer Verlag, 1996.
R. Brinkmann and R. Drechsler. RTL-datapath verification using integer linear programming. InIEEEVLSIDesign’01 & Asia and South Pacific Design Automation Conference, Bangalore, pages 741–746, 2002.
R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677–691, 1986.
J. R. Büchi. Weak second-order arithmetic and finite automata. Zeitschrift für mathematische Logik und Grundladen der Mathematik, 6:66–92, 1960.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98:142–170, 1992.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.
D. C. Cooper. Theorem proving in arithmetic without multiplication. In Machine Intelligence, volume 7, pages 91–99, New York, 1972. American Elsevier.
George B. Dantzig and B. Curtis Eaves. Fourier-Motzkin elimination and its dual. Journal of Combinatorial Theory (A), 14:288–297, 1973.
Jacob Elgaard, Nils Klarlund, and Anders Møller. Mona 1.x: new techniques for ws1s and ws2s. In Computer Aided Verification, CAV’ 98, Proceedings, volume 1427 of LNCS. Springer Verlag, 1998.
P. Johannsen and R. Drechsler. Formal verification on the RT level computing one-to-one design abstractions by signal width reduction. In IFIP International Conference on Very Large Scale Integration (VLSI’01), Montpellier, 2001, pages 127–132, 2001.
G. Kreisel and J. Krivine. Elements of mathematical logic, 1967.
K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.
Derek C. Oppen. A 222pn upper bound on the complexity of Presburger arithmetic. Journal of Computer and System Sciences, 16(3):323–332, June 1978.
M. Presburger. Uber de vollständigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen, die addition als einzige operation hervortritt. In Comptes Rendus du Premier Congrès des Mathématicienes des Pays Slaves, pages 92–101, 395, Warsaw, 1927.
William Pugh. The omega test: a fast and practical integer programming algorithm for dependence analysis. In Supercomputing, pages 4–13, 1991.
T. R. Shiple, J. H. Kukula, and R. K. Ranjan. A comparison of Presburger engines for EFSM reachability. In A. J. Hu and M. Y. Vardi, editors, Proceedings of the 10th International Conference on Computer Aided Verification, volume 1427, pages 280–292. Springer-Verlag, 1998.
H. P. Williams. Fourier-Motzkin elimination extension to integer programming problems. Journal of Combinatorial Theory (A), 21:118–123, 1976.
Pierre Wolper and Bernard Boigelot. On the construction of automata from linear arithmetic constraints. In Proc. 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 1785 of Lecture Notes in Computer Science, pages 1–19, Berlin, March 2000. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ganesh, V., Berezin, S., Dill, D.L. (2002). Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods. In: Aagaard, M.D., O’Leary, J.W. (eds) Formal Methods in Computer-Aided Design. FMCAD 2002. Lecture Notes in Computer Science, vol 2517. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36126-X_11
Download citation
DOI: https://doi.org/10.1007/3-540-36126-X_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00116-4
Online ISBN: 978-3-540-36126-8
eBook Packages: Springer Book Archive