Transform Alternating Automata into Weak Alternating Automata
A construction allowing to translate co-Büchi alternating automata into weak alternating automata is introduced in [KV97]. Another construction translating Rabin and Parity alternating automata into weak alternating automata is introduced in [KV98].
The goal is to Implement those constructions into Spot:
- Implement co-Büchi alternating automata -> weak alternating automata.
- Support Büchi alternating automata -> Weak alternating automata by complementing a Büchi automaton, translating it into weak and then complementing it back.
- See if it is possible to improve the co-Büchi -> weak construction so that it is not always performing as the worst-case complexity.
- Implement Rabin alternating -> Weak alternating
[KV97] O. Kupferman and M. Vardi. Weak alternating automata are not that weak. In Proc. 5th Israeli Symposium on Theory of Computing and Systems, pages 147-158. IEEE Computer Society Press, 1997.
[KV98] O. Kupferman and M. Vardi. Weak alternating automata and tree automata emptiness. In Proc 30th ACM Symposium on Theory of Computing, pages 224-233, Dallas, 1998.