LARA

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 $\exists$ and $\forall$ we obtain an exponential blowup. For formula with n alternations we have $2^{2^{\ldots 2^{n}}}$ complexity with a stack of exponentials of height $n$. Is there a better algorithm?

Reference

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.