On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic | SpringerLink
Skip to main content
Springer Nature Link
Log in

On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic

  • Conference paper
Mathematical Foundations of Computer Science 2014 (MFCS 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8635))

Abstract

We study the complexity of decision problems encoded in bit-vector logic. This class of problems includes word-level model checking, i.e., the reachability problem for transition systems encoded by bit-vector formulas. Our main result is a generic theorem which determines the complexity of a bit-vector encoded problem from the complexity of the problem in explicit encoding. In particular, NL-completeness of graph reachability directly implies PSpace-completeness and ExpSpace-completeness for word-level model checking with unary and binary arity encoding, respectively. In general, problems complete for a complexity class C are shown to be complete for an exponentially harder complexity class than C when represented by bit-vector formulas with unary encoded scalars, and further complete for a double exponentially harder complexity class than C with binary encoded scalars. We also show that multi-logarithmic succinct encodings of the scalars result in completeness for multi-exponentially harder complexity classes. Technically, our results are based on concepts from descriptive complexity theory and related techniques for OBDDs and Boolean encodings.

Supported by the NFN grant S11403-N23 (RiSE) of the Austrian Science Fund (FWF) and by the grant ICT10-050 (PROSEED) of the Vienna Science and Technology Fund (WWTF).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Balcázar, J.L., Lozano, A., Torán, J.: The complexity of algorithmic problems on succinct instances. Computer Science, 351–377 (1992)

    Google Scholar 

  2. Borchert, B., Lozano, A.: Succinct circuit representations and leaf language classes are basically the same concept. Inf. Process. Lett. 59(4), 211–215 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  3. Das, B., Scharpfenecker, P., Torán, J.: Succinct encodings of graph isomorphism. In: Dediu, A.-H., Martín-Vide, C., Sierra-Rodríguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol. 8370, pp. 285–296. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  4. Feigenbaum, J., Kannan, S., Vardi, M.Y., Viswanathan, M.: Complexity of problems on graphs represented as OBDDs. Chicago Journal of Theoretical Computer Science 5(5) (1999)

    Google Scholar 

  5. Galperin, H., Wigderson, A.: Succinct representations of graphs. Information and Control 56(3), 183–198 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  6. Gottlob, G., Leone, N., Veith, H.: Succinctness as a source of complexity in logical formalisms. Annals of Pure and Applied Logic 97(1), 231–260 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  7. Lozano, A., Balcázar, J.L.: The complexity of graph problems for succinctly represented graphs. In: Nagl, M. (ed.) WG 1989. LNCS, vol. 411, pp. 277–286. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  8. Papadimitriou, C.H., Yannakakis, M.: A note on succinct representations of graphs. Information and Control 71(3), 181–185 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  9. Veith, H.: Succinct representation, leaf languages, and projection reductions. In: IEEE Conference on Computational Complexity, pp. 118–126 (1996)

    Google Scholar 

  10. Veith, H.: Languages represented by boolean formulas. Inf. Process. Lett. 63(5), 251–256 (1997)

    Article  MathSciNet  Google Scholar 

  11. Veith, H.: Succinct representation, leaf languages, and projection reductions. Information and Computation 142(2), 207–236 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  12. Wagner, K.W.: The complexity of combinatorial problems with succinct input representation. Acta Informatica 23(3), 325–356 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  13. Fröhlich, A., Kovásznai, G., Biere, A.: More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding. In: Bulatov, A.A., Shur, A.M. (eds.) CSR 2013. LNCS, vol. 7913, pp. 378–390. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  14. Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for bit-vector arithmetic. In: Proc. DAC 1998, pp. 522–527 (1998)

    Google Scholar 

  15. Bjørner, N.S., Pichora, M.C.: Deciding fixed and non-fixed size bit-vectors. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 376–392. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  16. Bruttomesso, R., Sharygina, N.: A scalable decision procedure for fixed-width bit-vectors. In: ICCAD, pp. 13–20. IEEE (2009)

    Google Scholar 

  17. Cyrluk, D., Möller, O., Rueß, H.: An efficient decision procedure for a theory of fixed-sized bitvectors with composition and extraction. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 60–71. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  18. Franzén, A.: Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT. PhD thesis, University of Trento (2010)

    Google Scholar 

  19. Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. In: Proc. SMT 2010 (2010)

    Google Scholar 

  20. Brummayer, R., Biere, A., Lonsing, F.: BTOR: bit-precise modelling of word-level problems for model checking. In: Proc. 1st International Workshop on Bit-Precise Reasoning, pp. 33–38. ACM, New York (2008)

    Google Scholar 

  21. Kovásznai, G., Fröhlich, A., Biere, A.: On the complexity of fixed-size bit-vector logics with binary encoded bit-width. In: Proc. SMT 2012, pp. 44–55 (2012)

    Google Scholar 

  22. Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  23. Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 78–92. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  24. Manolios, P., Srinivasan, S.K., Vroon, D.: BAT: The bit-level analysis tool. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 303–306. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  25. Bradley, A.R.: Understanding IC3. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 1–14. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  26. Brummayer, R., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174–177. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  27. de Moura, L., Bjørner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  28. Bjesse, P.: A practical approach to word level model checking of industrial netlists. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 446–458. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  29. Bjorner, N., McMillan, K., Rybalchenko, A.: Program verification as satisfiability modulo theories. In: Proc. SMT 2012, pp. 3–11 (2013)

    Google Scholar 

  30. Veith, H.: How to encode a logical structure by an OBDD. In: Proc. 13th Annual IEEE Conference on Computational Complexity, pp. 122–131. IEEE (1998)

    Google Scholar 

  31. Immerman, N.: Languages that capture complexity classes. SIAM Journal on Computing 16(4), 760–778 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  32. Schwentick, T.: Padding and the expressive power of existential second-order logics. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414, pp. 461–477. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  33. Immerman, N.: Descriptive complexity. Springer (1999)

    Google Scholar 

  34. Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Texts in Theoretical Computer Science. Springer (2008)

    Google Scholar 

  35. Stewart, I.A.: Complete problems involving boolean labelled structures and projection transactions. Journal of Logic and Computation 1(6), 861–882 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  36. Stewart, I.A.: On completeness for NP via projection translations. In: Martini, S., Börger, E., Kleine Büning, H., Jäger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol. 702, pp. 353–366. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  37. Stewart, I.A.: Using the Hamiltonian path operator to capture NP. Journal of Computer and System Sciences 45(1), 127–151 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  38. Stewart, I.A.: On completeness for NP via projection translations. Mathematical Systems Theory 27(2), 125–157 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  39. Stewart, I.A.: Complete problems for monotone NP. Theoretical Computer Science 145(1), 147–157 (1995)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Formal Methods in Systems Engineering Group, Vienna University of Technology, Wien, Austria

    Gergely Kovásznai & Helmut Veith

  2. Institute for Formal Models and Verification, Johannes Kepler University, Linz, Austria

    Andreas Fröhlich & Armin Biere

Authors
  1. Gergely Kovásznai
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Helmut Veith
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Andreas Fröhlich
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Armin Biere
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Informatics, Eötvös Loránd University, Pázmány Péter sétány 1/C, 1117, Budapest, Hungary

    Erzsébet Csuhaj-Varjú

  2. Fakultät für Informatik und Automatisierung, Technische Universität Ilmenau, Helmholtzplatz, 598693, Ilmenau, Germany

    Martin Dietzfelbinger

  3. Institute of Informatics, Szeged University, Tisza Lajos krt. 103, 6720, Szeged, Hungary

    Zoltán Ésik

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kovásznai, G., Veith, H., Fröhlich, A., Biere, A. (2014). On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds) Mathematical Foundations of Computer Science 2014. MFCS 2014. Lecture Notes in Computer Science, vol 8635. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44465-8_41

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-44465-8_41

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-44464-1

  • Online ISBN: 978-3-662-44465-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation