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 q {\displaystyle q} and q ′ {\displaystyle q'} belonging to the same strongly connected component, q {\displaystyle q} is accepting if and only if q ′ {\displaystyle q'} is accepting. A Büchi automaton accepts a word w {\displaystyle w} if there exists a run, such that at least one state occurring infinitely often in the final state set F {\displaystyle F} . 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 automata and than Co-Büchi automata.
Properties The deterministic Weak Büchi automata can be minimized in time O ( n log ( n ) ) {\displaystyle O(n\log(n))} . The languages accepted by Weak Büchi automata are closed under union and intersection but not under complementation. For example, ( a + b ) ∗ b ω {\displaystyle (a+b)^{*}b^{\omega }} can be recognised by a Weak Büchi automaton but its complement ( b ∗ a ) ω {\displaystyle (b^{*}a)^{\omega }} cannot. Non-deterministic Weak Büchi automata are more expressive than Weak Büchi automata. As an example, the language ( a + b ) ∗ b ω {\displaystyle (a+b)^{*}b^{\omega }} can be decided by a Weak Büchi automaton but by no deterministic Büchi automaton.
References
Boigelot, Bernard (3 July 2005). "An effective decision procedure for linear arithmetic over the integers and reals" (PDF). ACM Transactions on Computational Logic. 6 (3): 614–633. doi:10.1145/1071596.1071601.
