Emil,
>>>>> "E" == Emil <Emil.Dumitrescu@imag.fr> writes:
>> However, VIS does not use ZDDs instead of BDDs for the more
>> traditional tasks of model checking. Experiments we ran several years
>> ago were not encouraging.
E> Does this mean that zdd manipulations are not at all fit for
E> symbolic FSM traversal ?
I think that would be going a bit too far. One can cetainly use
ZDDs. The question is whether you can improve over BDDs that way.
E> Is there a particular zdd operation which introduces a significant
E> computation/memory overhead ?
It mostly boils down to the size of the ZDDs representing the sets of
states. The reduction rules for ZDDs and BDDs are, as you know,
different. For model checking the reduction rule for BDDs was more
efficient. For example, in reachability analysis, after the first few
steps, the sets of states are not so sparse, and BDDs did better. I
can't recall much of the experiments we ran, because it was probably
seven or eight years ago, but I do remember we gave up on the idea
because of the disappointing results. I cannot rule out that for
certain classes of models, ZDDs may indead outperform BDDs in model
checking.
Another factor to take into account is that there are more functions
in CUDD that manipulate BDDs than functions that manipulate ZDDs. For
instance, there is no "constrain" or "restrict" for ZDDs.
Fabio
This archive was generated by hypermail 2b30 : Wed Mar 20 2002 - 07:55:13 MST