co-Büching Them All
We want Spot to support some algorithms related to co-Büchi described in:
-
http://www.cs.huji.ac.il/~ornak/publications/lics09.pdf
and http://www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf
The first paper introduces a way to convert any Nondeterministic Büchi Automaton (NBA
) to a Deterministic co-Büchi Automaton (DCA
). The second paper is a generalization of the first and expands this conversion to all common classes of ω-Automata (Street
, Rabin
, Parity
).