# Differences

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

Both sides previous revision Previous revision | |||

sav08:remarks_on_ws1s_complexity [2010/11/23 19:27] hossein |
sav08:remarks_on_ws1s_complexity [2010/11/23 19:29] (current) hossein |
||
---|---|---|---|

Line 6: | Line 6: | ||

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? | 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 ===== | ||

- | A. R. Meyer: [[http://publications.csail.mit.edu/lcs/pubs/pdf/MIT-LCS-TM-038.pdf|Weak monadic second order theory of successor is not elementary recursive]], Preliminary Report, 1973. | + | 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 ===== | ===== Lower Bound ===== |