In automata theory, generalized Büchi automaton (GBA) is a variant of Büchi automaton. The difference with the Büchi automaton is its accepting condition, i.e., a set of sets of states. A run is accepted by the automaton if it visits at least one state of every set of the accepting condition infinitely often. Generalized büchi automata (GBA) is equivalent in expressive power with Büchi automata; a transformation is given here.
In formal verification, the model checking method needs to obtain an automaton from a LTL formula that specifies the program property. There are algorithms that translate a LTL formula into a GBA[1] [2] [3] [4] for this purpose. The notion of GBA was introduced specifically for this translation.
Source: https:
//en.wikipedia.org/wiki/Generalized_B%C3%BCchi_automaton
