Advertisement

Hierarchical Set Decision Diagrams and Automatic Saturation

  • Alexandre Hamez
  • Yann Thierry-Mieg
  • Fabrice Kordon
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5062)

Abstract

Shared decision diagram representations of a state-space have been shown to provide efficient solutions for model-checking of large systems. However, decision diagram manipulation is tricky, as the construction procedure is liable to produce intractable intermediate structures (a.k.a peak effect). The definition of the so-called saturation method has empirically been shown to mostly avoid this peak effect, and allows verification of much larger systems. However, applying this algorithm currently requires deep knowledge of the decision diagram data-structures, of the model or formalism manipulated, and a level of interaction that is not offered by the API of public DD packages.

Hierarchical Set Decision Diagrams (SDD) are decision diagrams in which arcs of the structure are labeled with sets, themselves stored as SDD. This data structure offers an elegant and very efficient way of encoding structured specifications using decision diagram technology. It also offers, through the concept of inductive homomorphisms, unprecedented freedom to the user when defining the transition relation. Finally, with very limited user input, the SDD library is able to optimize evaluation of a transition relation to produce a saturation effect at runtime. We further show that using recursive folding, SDD are able to offer solutions in logarithmic complexity with respect to other DD. We conclude with some performances on well known examples.

Keywords

Hierarchical Decision Diagrams Model Checking Saturation 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)zbMATHCrossRefGoogle Scholar
  2. 2.
    Burch, J., Clarke, E., McMillan, K.: Symbolic model checking: 1020 states and beyond (Special issue for best papers from LICS90). Information and Computation 98(2), 153–181 (1992)CrossRefMathSciNetGoogle Scholar
  3. 3.
    Bollig, B., Wegener, I.: Improving the Variable Ordering of OBDDs Is NP-Complete. IEEE Trans. Comput. 45(9), 993–1002 (1996)zbMATHCrossRefGoogle Scholar
  4. 4.
    Roig, O., Cortadella, J., Pastor, E.: Verification of asynchronous circuits by BDD-based model checking of Petri nets. In: DeMichelis, G., Díaz, M. (eds.) ICATPN 1995. LNCS, vol. 935, pp. 374–391. Springer, Heidelberg (1995)Google Scholar
  5. 5.
    Ciardo, G., Marmorstein, R., Siminiceanu, R.: Saturation unbound. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 379–393. Springer, Heidelberg (2003)Google Scholar
  6. 6.
    Holzmann, G., Smith, M.: A practical method for verifying event-driven software. In: ICSE 1999: Proceedings of the 21st international conference on Software engineering, Los Alamitos, CA, USA, pp. 597–607. IEEE Computer Society Press, Los Alamitos (1999)Google Scholar
  7. 7.
    LIP6/Move: the libDDD environment (2007), http://www.lip6.fr/libddd
  8. 8.
    Couvreur, J.M., Encrenaz, E., Paviot-Adet, E., Poitrenaud, D., Wacrenier, P.A.: Data Decision Diagrams for Petri Net Analysis. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 1–101. Springer, Heidelberg (2002)Google Scholar
  9. 9.
    Couvreur, J.M., Thierry-Mieg, Y.: Hierarchical Decision Diagrams to Exploit Model Structure. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 443–457. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  10. 10.
    Wang, F.: Formal verification of timed systems: A survey and perspective. IEEE 92(8) (2004)Google Scholar
  11. 11.
    Ciardo, G., Siminiceanu, R.: Using edge-valued decision diagrams for symbolic generation of shortest paths. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 256–273. Springer, Heidelberg (2002)Google Scholar
  12. 12.
    Somenzi, F.: CUDD: CU Decision Diagram Package (release 2.4.1) (2005), http://vlsi.colorado.edu/fabio/CUDD/cuddIntro.html
  13. 13.
    Lind-Nielsen, J., Mishchenko, A., Behrmann, G., Hulgaard, H., Andersen, H.R., Lichtenberg, J., Larsen, K., Soranzo, N., Bjorner, N., Duret-Lutz, A., Cohen, H.a.: buddy - library for binary decision diagrams (release 2.4) (2004), http://buddy.wiki.sourceforge.net/
  14. 14.
    Ciardo, G.: Reachability Set Generation for Petri Nets: Can Brute Force Be Smart? Applications and Theory of Petri Nets 2004, pp. 17–34 (2004)Google Scholar
  15. 15.
    Cabac, L., Duvigneau, M., Moldt, D., Rölke, H.: Modeling Dynamic Architectures Using Nets-within-Nets. In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol. 3536, pp. 148–167. Springer, Heidelberg (2005)Google Scholar
  16. 16.
    Biberstein, O., Buchs, D., Guelfi, N.: Object-oriented nets with algebraic specifications: The CO-OPN/2 formalism (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Alexandre Hamez
    • 1
    • 2
  • Yann Thierry-Mieg
    • 1
  • Fabrice Kordon
    • 1
  1. 1.Université P. & M. Curie, LIP6 - CNRS UMR 7606Paris cedex 05France
  2. 2.EPITA, Research and Development LaboratoryLe Kremlin-Bicetre cedexFrance

Personalised recommendations