Weak Büchi automaton explained

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

and

belonging to the same strongly connected component,

is accepting if and only if

is accepting.

A Büchi automaton accepts a word

if there exists a run, such that at least one state occurring infinitely often in the final state set

. 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(nlog(n))

.^[1]

The languages accepted by Weak Büchi automata are closed under union and intersection but not under complementation. For example,

(a+b)^*b^\omega

can be recognised by a Weak Büchi automaton but its complement

(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^\omega

can be decided by a Weak Büchi automaton but by no deterministic Büchi automaton.

References

Boigelot. Bernard. An effective decision procedure for linear arithmetic over the integers and reals. ACM Transactions on Computational Logic. 3 July 2005. 6. 3. 614–633. 10.1145/1071596.1071601.

Notes and References

Löding . Christof . Efficient Minimization of Deterministic Weak ω-Automata . Information Processing Letters . 2001 . 79 . 3 . 105–109 . 10.1016/S0020-0190(00)00183-6.