Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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