LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
Next revision Both sides next revision
ws1s_expressive_power_and_quantifier_elimination [2007/06/29 12:01]
ghid.maatouk
ws1s_expressive_power_and_quantifier_elimination [2007/06/29 17:12]
vaibhav.rajan
Line 1: Line 1:
-* why the problem is interesting+Introduction:​ 
 +We know that Weak Monadic Second-order theory of 1 Successor (WS1S) is decidable through automata, that is, the set of satisfying interpretations of a subformula is represented by a finite-state automaton [Buc60b, Elg61]. The decision procedures (using the automata technique) have been implemented efficiently (for WS1S with certain restrictions) in MONA. 
 +The main problem ​with this approach ​is exponential blow-up in the states of the automaton due to nested quantifiers [Kla01]. 
 +We were interested in finding another way of deciding WS1S without using the automata. We began by investigating whether we can characterize relations in WS1S in a way that helps us eliminate quantifiers. Since we couldn'​t get any substantial results, we began looking at a subset of WS1S. This paper describes the key results that we obtained. ​
  
-deciding WS1S - done through automata construction (mona)\\ +Conclusions and Future Directions:  
-main problemquantifier elimination\\ +In the course ​of our mini-project ​we proved an interesting result about the lengths of words of a regular language. We used this result to characterize relations in the language $L^R$. We hope that this is a step in the direction ​of our original aimcharacterizing ​relations ​in WS1S
-is there another way of QE? can we characterize relations in WS1S in some other way?\\ +
-WS1S too big: look at a smaller subset ​of the language\\ +
-our Lcharacterize unary relations, binary relations,...n-ary\\  ​+
  
-* what was done before 
  
-p-recognizability 
  
-* what the main idea is 
- 
-* what you did (precise description) 
- 
-* the most surprising/​interesting things you found 
- 
-* limitations 
- 
-* future directions 
- 
-look at other subsets of WS1S, whole of WS1S 
  
 **START** **START**
Line 197: Line 184:
 The above reasoning can be extended to the n-ary case. The input string has n non-zero elements and n+1 expressions of the form $(\{(0...0)^{-1}\})^k$. A tuple $(x_1, x_2,​...x_n)$ belongs to an n-ary relation iff the possible values of each exponent $k$  forms an ultimately periodic set. The above reasoning can be extended to the n-ary case. The input string has n non-zero elements and n+1 expressions of the form $(\{(0...0)^{-1}\})^k$. A tuple $(x_1, x_2,​...x_n)$ belongs to an n-ary relation iff the possible values of each exponent $k$  forms an ultimately periodic set.
  
 +References:​\\
 +[Buc60a] Julius Richard Buchi. On a decision method in restricted second-order arithmetic. In Proc. Internat. Cong. on Logic, Methodol., and Philos. of Sci. Stanford University Press, 1960.\\
 +[Elg61] Calvin C. Elgot. Decision problems of Finite automata design and related arithmetics. Transactions of the American Mathematical Society, 98:21{52, 1961.\\
 +[Kla01] Nils Klarlund, Anders Moller. MONA Version 1.4 User Manual. BRICS, Department of Computer Science, University of Aarhus, 2001.\\