Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
sav08:remarks_on_ws1s_complexity [2010/11/23 19:22] hossein |
sav08:remarks_on_ws1s_complexity [2010/11/23 19:27] hossein |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Remarks on WS1S Complexity ====== | ====== Remarks on WS1S Complexity ====== | ||
| + | |||
| ===== Complexity of One Algorithm ===== | ===== 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 ===== | ===== Reference ===== | ||