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 [math]\displaystyle{ q }[/math] and [math]\displaystyle{ q' }[/math] belonging to the same strongly connected component, [math]\displaystyle{ q }[/math] is accepting if and only if [math]\displaystyle{ q' }[/math] is accepting. A Büchi automaton accepts a word [math]\displaystyle{ w }[/math] if there exists a run, such that at least one state occurring infinitely often in the final state set [math]\displaystyle{ F }[/math]. 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 [math]\displaystyle{ O(n \log(n)) }[/math].[1]
The languages accepted by Weak Büchi automata are closed under union and intersection but not under complementation. For example, [math]\displaystyle{ (a+b)^*b^\omega }[/math] can be recognised by a Weak Büchi automaton but its complement [math]\displaystyle{ (b^*a)^\omega }[/math] cannot.
Non-deterministic Weak Büchi automata are more expressive than Weak Büchi automata. As an example, the language [math]\displaystyle{ (a+b)^*b^\omega }[/math] can be decided by a Weak Büchi automaton but by no deterministic Büchi automaton.
References
- ↑ Löding, Christof (2001). "Efficient Minimization of Deterministic Weak ω-Automata". Information Processing Letters 79 (3): 105–109. doi:10.1016/S0020-0190(00)00183-6.
- Boigelot, Bernard (3 July 2005). "An effective decision procedure for linear arithmetic over the integers and reals". ACM Transactions on Computational Logic 6 (3): 614–633. doi:10.1145/1071596.1071601. https://orbi.uliege.be/bitstream/2268/12428/2/BJW05.pdf.
 |  |
