Weak Büchi automaton

In automata theory, a Weak Büchi automaton is a variant of Büchi automaton. The only difference is a constraint over the set of accepting states: every step of a strongly connected component. In contrast, a Büchi automaton accepts a word $w$ if there exists a run, such that at least one state occurring infinitely often in the final state set $F$ .

Weak Büchi automata are strictly weaker than Büchi automaton and than Co-Büchi automaton.

Properties

Weak Büchi automata are equivalent to deterministic Weak Büchi automata. The determinization algorithm have exponential time. The deterministic Weak Büchi automata can be minimized in time $O(n \log(n))$ .

Weak Büchi automata are closed under union, intersection and complementation.

References

Boigelot, Bernard (3 July 2005). "An effective decision procedure for linear arithmetic over the integers and reals". ACM Transactions on Computational Logic (TOCL) 6 (3): 614–633.