2.4 Model checking result consistency check

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).