• 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 Both sides previous revision Previous revision 2010/11/23 19:29 hossein 2010/11/23 19:27 hossein 2010/11/23 19:22 hossein 2009/04/29 10:56 vkuncak 2009/04/17 15:23 vkuncak 2009/04/17 15:22 vkuncak 2009/04/17 15:22 vkuncak created 2010/11/23 19:29 hossein 2010/11/23 19:27 hossein 2010/11/23 19:22 hossein 2009/04/29 10:56 vkuncak 2009/04/17 15:23 vkuncak 2009/04/17 15:22 vkuncak 2009/04/17 15:22 vkuncak created 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 =====