Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:using_automata_to_decide_ws1s [2012/05/15 12:46] vkuncak |
sav08:using_automata_to_decide_ws1s [2012/05/15 15:11] vkuncak |
||
---|---|---|---|
Line 14: | Line 14: | ||
\] | \] | ||
- | Instead of $e(F)(D,\alpha(w))={\it true}$ we write for short $w \models F$. | + | Instead of $e(F)(D,\alpha(w))={\it true}$ we write for short $w \models F$. So, we design automata so that: |
+ | \[ | ||
+ | w \in L(A(F)) \ \ \ \iff \ \ \ w \models F | ||
+ | \] | ||
The following lemma follows from the definition of semantic evaluation function 'e' and the shorthand $w \models F$. | The following lemma follows from the definition of semantic evaluation function 'e' and the shorthand $w \models F$. | ||
Line 100: | Line 103: | ||
**Example 1:** Compute automaton for formula $\exists X. \lnot (X \subseteq Y)$. | **Example 1:** Compute automaton for formula $\exists X. \lnot (X \subseteq Y)$. | ||
- | **Example 2:** Compute automaton for formula $\exists Y. (X < Y)$ where $<$ is interpreted treating $X,Y$ as digits of natural numbers. | + | **Example 2:** Compute automaton for formula $\exists Y. (X < Y)$ where $<$ is interpreted treating $X,Y$ as digits of natural numbers. Also compute the automaton for the formula $\exists X. (X < Y)$. |
===== References ===== | ===== References ===== |