Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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 =====
 
sav08/remarks_on_ws1s_complexity.txt · Last modified: 2010/11/23 19:29 by hossein
 
© EPFL 2018 - Legal notice