Certifying Inexpressibility
Certifying Inexpressibility
Different classes of automata on infinite words have different expressive power.Deciding whether a given language L ⊆ Σ ω can be expressed by an automaton of a desired class can be reduced to deciding a game between Prover and Refuter: in each turn of the game, Refuter provides a letter …