states in the NB and is the number of Rabin acceptance pairs (see, for example, ). with exponential blow-up in the state space. with exponential blow-up in the state space. This determinization result uses Safra's construction. A comprehensive overview of translations can be found on the referenced web source. Applications to decidability ω-automata can be used to prove decidability of S1S, the monadic second-order (MSO) theory of natural numbers under successor. Infinite-tree automata extend ω-automata to infinite trees and can be used to prove decidability of S2S, the MSO theory with two successors, and this can be extended to the MSO theory of graphs with bounded (given a fixed bound) treewidth. Further reading . References Finite automata