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
>