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 $q$ and $q'$ belonging to the same strongly connected component, $q$ is accepting if and only if $q'$ is accepting.

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$ . 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))$ .{{cite journal |last1=Löding |first1=Christof |title=Efficient Minimization of Deterministic Weak ω-Automata |journal=Information Processing Letters |date=2001 |volume=79 |issue=3 |pages=105–109 |doi=10.1016/S0020-0190(00)00183-6}}

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

{{cite journal|last1=Boigelot|first1=Bernard|title=An effective decision procedure for linear arithmetic over the integers and reals|journal=ACM Transactions on Computational Logic|date=3 July 2005|volume=6|issue=3|pages=614–633|doi = 10.1145/1071596.1071601|url=https://orbi.uliege.be/bitstream/2268/12428/2/BJW05.pdf}}

Category:Automata (computation)