Generalized Büchi automaton
 |
 | This article provides insufficient context for those unfamiliar with the subject. (October 2010) |
In automata theory, generalized Büchi automaton (GBA) is a variant of Büchi automata. Its accepting condition is defined by 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.
This variant is interesting because an LTL formula can be easily translated into GBA.
Labeled generalized Büchi automaton
Labeled Generalized Büchi automaton is one where the labels actually apply to the states rather than the edges. To obtain the non labeled version, the labels are moved from the nodes to the incoming arcs.
Transformation from LTL to GBA
There is an algorithm over structure of LTL formula that translates it to a GBA.