Skip to main content
SpringerLink
Log in

Experiments with Multiple Abstraction Heuristics in Symbolic Verification

  • Conference paper
Abstraction, Reformulation and Approximation (SARA 2005)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 3607))

Abstract

In this work we investigate a symbolic heuristic search algorithm in a model checker. The symbolic search algorithm is built on a system that manipulates binary decision diagrams (BDDs). We study the performance of the search algorithm in terms of the number of BDD operations, size of the BDDs, number of nodes they contain and run-time. We study the heuristic distribution of the state space, we measure effort by computing the mean heuristic value, and we compare single and multiple heuristics. In the case of multiple heuristics, we consider admissible and non-admissible merge strategies. We experiment on problems from a variety of domains. We find that multiple heuristics can perform significantly worse than single heuristics in symbolic search in at least one domain. In general, the effect of the heuristics on the symbolic search in the different domains varies markedly, and we conjecture that the different behaviour is caused by intrinsic differences in the characteristics of the state space.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • 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.

References

  1. Bollig, B., Wegener, I.: Improving the variable ordering of obdds is np-complete. IEEE Trans. Computers 45(9), 993–1002 (1996)

    Article  MATH  Google Scholar 

  2. Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Transaction C-35(8), 677–691 (1986)

    Article  MATH  Google Scholar 

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

    Google Scholar 

  4. Culberson, J.C., Schaeffer, J.: Searching with pattern databases. In: McCalla, G.I. (ed.) Canadian AI 1996. LNCS, vol. 1081, pp. 402–416. Springer, Heidelberg (1996)

    Google Scholar 

  5. Edelkamp, S.: Symbolic pattern databases in heuristic search planning. In: Proc. of the Sixth Int. Conf. on Artificial Intelligence Planning Systems, Toulouse, France, April 23-27, pp. 274–283. AAAI, Menlo Park (2002)

    Google Scholar 

  6. Edelkamp, S., Lluch-Lafuente, A.: Abstraction databases in theory and model checking practice. In: Proc. of Workshop on Connecting Planning Theory with Practice, Int. Conf. on Automated Planning and Scheduling, ICAPS, Whistler, Canada (2004)

    Google Scholar 

  7. Edelkamp, S., Reffel, F.: OBDDs in heuristic search. In: Herzog, O. (ed.) KI 1998. LNCS, vol. 1504, pp. 81–92. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  8. Felner, A., Korf, R.E., Hanan, S.: Additive pattern database heuristics. J. Artif. Intell. Res (JAIR) 22, 279–318 (2004)

    MATH  MathSciNet  Google Scholar 

  9. Hansen, E., Zhou, R., Feng, Z.: Symbolic heuristic search using decision diagrams. In: Koenig, S., Holte, R.C. (eds.) SARA 2002. LNCS (LNAI), vol. 2371, pp. 83–98. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  10. Holte, R., Newton, J., Felner, A., Meshulam, R., Furcy, D.: Multiple pattern databases. In: Proc. of 14th Intl. Conf. on Automated Planning & Scheduling (ICAPS), pp. 122–131. AAAI, Menlo Park (2004)

    Google Scholar 

  11. Holte, R.C., Hernádvölgyi, I.T.: A space-time tradeoff for memory-based heuristics. In: AAAI/IAAI, pp. 704–709 (1999)

    Google Scholar 

  12. Jensen, R.M., Bryant, R.E., Veloso, M.M.: Seta*: An efficient bdd-based heuristic search algorithm. In: Proc. of the Eighteenth National Conf. on Artificial Intelligence and 14th Conf. on Innovative Applications of Artificial Intelligence, Alberta, Canada, pp. 668–673. AAAI Press, Menlo Park (2002)

    Google Scholar 

  13. Korf, R.: Finding optimal solutions to to Rubik’s cube using pattern databases. In: Proc. of the 14th National Conf. on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conf., Providence, Rhode Island, July 27-31, pp. 700–705. AAAI Press/The MIT Press (1997)

    Google Scholar 

  14. Korf, R.E., Felner, A.: Disjoint pattern database heuristics. Artif. Intell. 134(1-2), 9–22 (2002)

    Article  MATH  Google Scholar 

  15. Korf, R.E., Reid, M., Edelkamp, S.: Time complexity of iterative-deepening-a*. Artif. Intell. 129(1-2), 199–218 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  16. McMillan, K.: Symbolic model checking. Kluwer Academic Publishers, Boston (1993)

    MATH  Google Scholar 

  17. Nymeyer, A., Qian, K.: Heuristic search algorithm based on symbolic data structures. In: Gedeon, T(T.) D., Fung, L.C.C. (eds.) AI 2003. LNCS (LNAI), vol. 2903, pp. 966–979. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  18. Qian, K., Nymeyer, A.: Abstraction-based model checking using heuristical refinement. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 165–178. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  19. Qian, K., Nymeyer, A.: Guided invariant model checking based on abstraction and symbolic pattern databases. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 497–511. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  20. Qian, K., Nymeyer, A.: Abstraction-guided model checking using symbolic IDA* and heuristic synthesis. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 275–289. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  21. Ravi, K., Somenzi, F.: High-density reachability analysis. In: ICCAD 1995: Proc. of the 1995 IEEE/ACM international conference on Computer-aided design, pp. 154–158. IEEE Computer Society, Los Alamitos (1995)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science & Engineering, The University of New South Wales, Sydney, Australia

    Kairong Qian, Albert Nymeyer & Steven Susanto

Authors
  1. Kairong Qian
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Albert Nymeyer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Steven Susanto
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. UR 079 GEODES, IRD, 32 avenue Henri Varagnat, 93143, Bondy, France

    Jean-Daniel Zucker

  2. Dip. di Informatica, Università del Piemonte Orientale, Via Bellini 25/G, 15100, Alessandria, Italy

    Lorenza Saitta

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Qian, K., Nymeyer, A., Susanto, S. (2005). Experiments with Multiple Abstraction Heuristics in Symbolic Verification. In: Zucker, JD., Saitta, L. (eds) Abstraction, Reformulation and Approximation. SARA 2005. Lecture Notes in Computer Science(), vol 3607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11527862_22

Download citation

  • DOI: https://doi.org/10.1007/11527862_22

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-27872-6

  • Online ISBN: 978-3-540-31882-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation