Next: Automata intersection emptiness check, Previous: Model checking result cross-comparison test, Up: Test methods

LTL model checking tells whether any of the infinite paths starting from some
state of a state space satisfies a given LTL formula. If there
are no such paths beginning from the state, it follows that all infinite paths
beginning from the state must then satisfy the *negation* of the same
formula. Since all state spaces used by `lbtt` always have at least
one path beginning from each state of the state space (guaranteed by the
state space generation algorithms), at least
one path beginning from any state must satisfy either the formula or its
negation, i.e., it cannot be the case that none of the paths is a model of
either formula.

However, implementation errors in an LTL-to-Büchi translator used for model
checking may actually lead to this inconsistent model checking result if the
translation of either of the formulas results in an incorrect automaton, in
which case `lbtt` will report an error.

Similarly to the model checking result cross-comparison test, the model checking result consistency check can be performed either in all states of the state space (“globally”) or only in a single state of the state space (“locally”), with the same trade-offs between testing speed and number of tests as described in the previous section (see Model checking result cross-comparison test).