An omega-language is omega-regular iff it is definable in monadic second-order logic S1S. Accepting runs translate to second-order existential quantifiers, while logical connectives translate to automata operations, proving S1S decidability.