Explicit state model checking with generalized Büchi and Rabin automata
Vincent Bloemen, Alexandre Duret-Lutz, Jaco van de Pol · 2017
In the automata theoretic approach to explicit state LTL model checking, the synchronized product of the model and an automaton that represents the negated formula is checked for emptiness. In practice, a (transition-based generalized) Büchi automaton (TGBA) is used for this procedure.