# Remarks on WS1S Complexity

## Complexity of One Algorithm

The construction in Using Automata to Decide WS1S determinizes automaton whenever it needs to perform negation. Moreover, existential quantifier forces the automaton to be non-deterministic. Therefore, with every alternation between and we obtain an exponential blowup. For formula with n alternations we have complexity with a stack of exponentials of height . Is there a better algorithm?

## Lower Bound

The following paper shows that, in the worst case such behavior cannot be avoided, because of such high expressive power of MSOL over strings.