•These ideas have been
implemented in a system, MVSIS
•The SS behavior has been
used throughout.
–it is the easiest to use
computationally
–global behavior can be
expressed locally at each node as a BDD of the PI
•In the future we will
experiment with using NSC behavior