Differences

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

--- sav08:remarks_on_ws1s_complexity [2009/04/17 15:22]
vkuncak created
+++ sav08:remarks_on_ws1s_complexity [2009/04/29 10:56]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Remarks on WS1S Complexity ======
-===== Complexity =====
+===== Complexity of One Algorithm =====
-The above construction 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 following paper shows that, in the worst case such behavior cannot be avoided, because of such high expressive power of MSOL over strings.
+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?
+===== 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.
   * [[http://theory.csail.mit.edu/~meyer/stock-circuit-jacm.pdf|Cosmological Lower Bound on the Circuit Complexity of a Small Problem in Logic]] (See the introduction and the conclusion sections)
-    * circuit versus assymptotic time complexity (uniformity, specific instance versus assymptotic bound)
-    * the density question
-    * do we need to know how to check validity for all MSOL formulas