Deciding S1S: Down the Rabbit Hole and Through the Looking Glass

Monadic second-order logic of one successor (S1S) is a logic for specifying \(\omega \)-regular languages in a concise way. In this paper, we revisit the classical decision procedure based on translating S1S formulae into Büchi automata and employ state-of-the-art algorithms for their manipulation, in particular complementation and size reduction. We compare our implementation to the one based on loop-deterministic finite automata and observe cases where the classical approach scales better.