Differences

This shows you the differences between two versions of the page.

--- sav08:remarks_on_ws1s_complexity [2009/04/29 10:56]
vkuncak
+++ sav08:remarks_on_ws1s_complexity [2010/11/23 19:29]
hossein
@@ Line 1: / Line 1: @@
 ====== 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}}$ complexity with a stack of exponentials of height $n$.  Is there a better 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 =====
+A. R. Meyer: [[http://publications.csail.mit.edu/lcs/specpub.php?id=37|Weak monadic second order theory of successor is not elementary recursive]], Preliminary Report, 1973.
 ===== Lower Bound =====