Hierarchical Set Decision Diagrams and Automatic Saturation

Authors

Alexandre Hamez, Yann Thierry-Mieg, Fabrice Kordon

Where

Petri Nets and Other Models of Concurrency –ICATPN 2008

Type

inproceedings

Projects

Verification"Verification" is not in the list (Vaucanson, Spot, URBI, Olena, APMC, Tiger, Climb, Speaker ID, Transformers, Bison, ...) of allowed values for the "Related project" property.

Date

2008-03-01

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.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  hamez.08.atpn,
  author	= {Alexandre Hamez and Yann Thierry-Mieg and Fabrice Kordon},
  title		= {Hierarchical Set Decision Diagrams and Automatic
		  Saturation},
  booktitle	= {Petri Nets and Other Models of Concurrency --ICATPN 2008},
  year		= 2008,
  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.}
}