Abstract
In this paper, I show that methods from computational algebraic geometry can be used to carry out symbolic model checking using an encoding of Boolean sets as the common zeros of sets of polynomials. This approach could serve as a useful supplement to symbolic model checking methods based on Ordered Binary Decision Diagrams and may provide important theoretical insights by bringing the powerful mathematical machinery of algebraic geometry to bear on the model checking problem.
Chapter PDF
Similar content being viewed by others
References
W. W. Adams and P. Loustaunau. An Introduction to Gröbner Bases, Volume 3 of Graduate Studies in Mathematics. American Mathematical Society, Providence, RI, 1994.
D. Bayer and M. Stillman. Macaulay: A System for Computation in Algebraic Geometry and Commutative Algebra. Source and object code available for Unix and Macintosh computers. Contact the authors, or download from math. harvard. edu via anonymous ftp., 1982–1994.
D. Bayer and M. Stillman. A criterion for detecting m-regularity. Invent. Math., 87:1–11, 1987.
T. Becker and V. Weispfenning. Gröbner Bases, Volume 141 of Graduate Texts in Mathematics. Springer-Verlag, New York, 1993.
R. E. Bryant. On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Trans. Comput., 40(2):205–213, Feb. 1991.
B. Buchberger. Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. PhD thesis, University of Innsbruck, 1965.
B. Buchberger. Gröbner bases: An algorithmic method in polynomial ideal theory. In N. K. Bose, editor, Multidimensional Systems Theory, pages 184–232. D. Reidel, 1985.
J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 428–439, 1990.
D. Cox, J. Little, and D. O'Shea. Ideals, Varieties, and Algorithms. Undergraduate Texts in Mathematics. Springer-Verlag, New York, 1992.
P. Gritzmann and B. Sturmfels. Minkowski addition of polytopes: Computational complexity and applications to Gröbner bases. SIAM Journal on Discrete Mathematics, 6(2): 246–269, 1993.
R. Hartshorne. Algebraic Geometry, Volume 52 of Graduate Texts in Mathematics. Springer-Verlag, New York, 1977.
E. Mayr and A. Meyer. The complexity of the word problem for commutative semigroups and polynomial ideals. Adv. in Math., 1982.
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Avrunin, G.S. (1996). Symbolic model checking using algebraic geometry. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_55
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_55
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive