Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision Next revision Both sides next revision | ||
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 ====== | ====== 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) | * [[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 | ||