Go to the first, previous, next, last section, table of contents.

3.3.2 LTL Specifications

NuSMV allows for specifications expressed in LTL. Model checking of LTL specifications is based on the construction of a tableau corresponding to the LTL formula and on CTL model checking, along the lines described in [CGH97]. This construction is completely transparent to the user.

LTL specifications are introduced by the keyword `LTLSPEC'. The syntax of this declaration is:

ltlspec_declaration :: "LTLSPEC" ltl_expr

where

ltl_expr ::
        simple_expr                ;; a simple boolean expression
        | "(" ltl_expr ")"
        | "!" ltl_expr             ;; logical not
        | ltl_expr "&" ltl_expr    ;; logical and
        | ltl_expr "|" ltl_expr    ;; logical or
        | ltl_expr "->" ltl_expr   ;; logical implies
        | ltl_expr "<->" ltl_expr  ;; logical equivalence
        | "G" ltl_expr             ;; globally
        | "X" ltl_expr             ;; next state
        | "F" ltl_expr             ;; finally
        | ltl_expr "U" ltl_expr    ;; until

As for CTL formulas, simple_expr can not contain case statements. The counterexample generated to show the falsity of a LTL specification may contain state variables which have been introduced by the tableau construction procedure. Currently it is not possible to navigate the counterexamples for LTL formulas.