Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
ws1s_expressive_power_and_quantifier_elimination [2007/06/29 16:39] vaibhav.rajan |
ws1s_expressive_power_and_quantifier_elimination [2007/06/29 17:12] vaibhav.rajan |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | We know that Weak Monadic Second-order theory of 1 Successor (WS1S) is decideable 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. | + | Introduction: |
- | The main problem with this approach is exponential blowup in the states of the automaton due to nested quantifiers [Nil01]. | + | 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. |
- | 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. | + | 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. | ||
+ | Conclusions and Future Directions: | ||
+ | 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 aim: characterizing relations in WS1S. | ||
- | * why the problem is interesting | ||
- | deciding WS1S - done through automata construction (mona)\\ | ||
- | main problem: quantifier elimination\\ | ||
- | 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 L: characterize 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 202: | 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.\\ |