Hi all,

Do you know any tools that can convert universal co-buchi automata into universal safety automata via bounding the number of visits to the final states? (I.e., go to absorbing bad state if visit a final state k times)

(Alternatively, convert NBW into nondet finite automaton: accept a word if it visits a final state k times)

(I am just trying to avoid work that may have already be done:)

Thanks, Ayrat