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