Weak Büchi automaton
In computer science and automata theory, a Weak Büchi automaton is a formalism which represents a set of infinite words. A Weak Büchi automaton is a modification of Büchi automaton such that for all pair of states formula_1 and formula_2 belonging to the same strongly connected component, formula_1 is accepting if and only if formula_2 is accepting. A Büchi automaton accepts a word formula_5 if there exists a run, such that at least one state occurring infinitely often in the final state set formula_6. For Weak Büchi automata, this condition is equivalent to the existence of a  run which ultimately stays in the set of accepting states. Weak Büchi automata are strictly less-expressive than Büchi automaton and than Co-Büchi automaton. Properties. The deterministic Weak Büchi automata can be minimized in time formula_7. The languages accepted by Weak Büchi automata are closed under union, intersection and complementation. Non-deterministic Weak Büchi automata are more expressive than Weak Büchi automata. As an example, the language formula_8 can be decided by a weak Büchi automaton but by no deterministic Büchi automaton