Efficient inclusion testing for simple classes of unambiguous ω-automata

We show that language inclusion for languages of infinite words defined by nondeterministic automata can be tested in polynomial time if the automata are unambiguous and have simple acceptance conditions, namely safety or reachability conditions. An automaton with safety condition accepts an infinite word if there is a run that never visits a forbidden state, and an automaton with reachability condition accepts an infinite word if there is a run that visits an accepting state at least once.

► We consider omega-automata with safety and reachability conditions. ► We show that for unambiguous automata of this kind the inclusion problem can be solved in polynomial time. ► The algorithms work by a reduction to the problem of inclusion testing for unambiguous NFAs.