LTL is important because it allows us to express properties, such as
fairness,^{11} which are not expressible in CTL. Furthermore,
LTL can be useful to perform selective analysis, namely to specify the paths
of interest.

NUSMV supports LTL model checking implementing the algorithm presented in [32]. An LTL formula is automatically converted into a tableau [45], which is then used to extend the original model in synchronous product. The result is provided by checking the validity of an automatically generated CTL formula from the LTL specification in the extended model.

The loose integration presented in [32] allows for the use
of CMU SMV as a black box by generating a new input file containing
both the original description of the system and the code implementing
the tableau. However, for each LTL formula to be verified the
verification process has to be restarted from scratch, starting from
the parsing of the newly generated input file.
In NUSMV the tableau generation is tightly integrated. If more than
one LTL property is specified, only the generation of the
corresponding tableau is required, thus avoiding, each time, the generation
of the whole model. The generated tableau is parsed in, compiled into `BDD`
and synchronously composed with the original model.^{12}

NuSMV <>