Affiliations: Université P. & M. Curie LIP6 - CNRS UMR
7606, 4 Place Jussieu, 75252 Paris cedex 05, France. E-mail:
{Alexandre.Hamez,Yann.Thierry-Mieg,Fabrice.Kordon}@lip6.fr
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 symbolic 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 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.
Keywords: Hierarchical Decision Diagrams, Model Checking, Saturation
