This module provides all the {RT}CTL model checking functionalities, such as reachability and model checking routines, routines that perform computation of quantitative characteristics, and check invariants on the fly. All these routines are based on the image and pre-image computation primitives, and are independent of the particular method used to represent the FSM.
>