Previous: Model checking result consistency check, Up: Test methods


2.5 Automata intersection emptiness check

The semantics of LTL guarantees that no model of an LTL formula can be the model of the negation of the same formula. In terms of Büchi automata, this implies that the languages accepted by automata constructed from two complementary LTL formulas should be disjoint. This can be confirmed by intersecting the automata (i.e., by composing the automata to construct a third Büchi automaton that accepts precisely those inputs accepted by both of the original automata) and checking the result for emptiness. If the intersection is found to be nonempty, however, at least one of the LTL-to-Büchi translator(s) used for constructing the original automata must have failed to perform the translation of either formula correctly.