NUSMV has been and is still used as the kernel of MBP, a planner based on model checking able to synthesize reactive controllers for achieving goals in nondeterministic domains [20,21].18 MBP has been obtained by substituting or eliminating some of the NUSMV modules. In particular, the NUSMV parser module has been redone (the two input languages are different); the NUSMV instantiation module has been eliminated (at the moment, in MBP there is no concept of hierarchy); the NUSMV semantic check module has been redone; the NUSMV FSM compiler has been redone to reflect the way in which the MBP input language is compiled into BDDs [17]. All the other modules have been left unchanged, and are shared between the two systems. Finally, a new module, containing all the special purpose, planning algorithms, has been added. This module provides routines based on the image and pre-image computation.
>