Building Efficient Model checkers using Hierarchical Set Decision Diagrams and automatic Saturation

Authors

Alexandre Hamez, Yann Thierry-Mieg, Fabrice Kordon

Journal

Fundamenta Informaticae

Type

article

Date

2009-01-01

Abstract

Shared decision diagram representations of a state-space provide efficient solutions for model-checking of large systems. However, decision diagram manipulation is trickyas 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 effectand allows verification of much larger systems. Howeverapplying this algorithm currently requires deep knowledge of the decision diagram data-structures. 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, flexibility to a user defining a transition relation. We show in this paper howwith very limited user input, the SDD library is able to optimize evaluation of a transition relation to produce a saturation effect at runtime. We build as an example an SDD model-checker for a compositional formalism: Instantiable Petri Nets (IPN). IPN define a type as an abstract contract. Labeled P/T nets are used as an elementary type. A composite type is defined to hierarchically contain instances (of elementary or composite type). To compose behaviors, IPN use classic label synchronization semantics from process calculi. With a particular recursive folding SDD are able to offer solutions for symmetric systems in logarithmic complexity with respect to other DD. Even in less regular cases, the use of hierarchy in the specification is shown to be well supported by SDD. Experimentations and performances are reported on some well known examples.

Bibtex (lrde.bib)

@Article{	  hamez.09.fi,
  abstract	= {Shared decision diagram representations of a state-space
		  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. 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, flexibility to a user
		  defining a transition relation. We show in this paper how,
		  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 build as an example an SDD
		  model-checker for a compositional formalism: Instantiable
		  Petri Nets (IPN). IPN define a \emph{type} as an abstract
		  contract. Labeled P/T nets are used as an elementary type.
		  A composite type is defined to hierarchically contain
		  instances (of elementary or composite type). To compose
		  behaviors, IPN use classic label synchronization semantics
		  from process calculi. With a particular recursive folding
		  SDD are able to offer solutions for symmetric systems in
		  logarithmic complexity with respect to other DD. Even in
		  less regular cases, the use of hierarchy in the
		  specification is shown to be well supported by SDD.
		  Experimentations and performances are reported on some well
		  known examples. },
  author	= {Alexandre Hamez and Yann Thierry-Mieg and Fabrice Kordon},
  date-added	= {2009-05-06 16:39:07 +0200},
  date-modified	= {2009-05-06 16:48:10 +0200},
  journal	= {Fundamenta Informaticae},
  title		= {Building Efficient Model checkers using Hierarchical Set
		  Decision Diagrams and automatic Saturation},
  year		= 2009
}