• English only

# Differences

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

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