Differences

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

--- sav08:using_automata_to_decide_ws1s [2011/04/12 15:09]
vkuncak
+++ sav08:using_automata_to_decide_ws1s [2012/05/15 15:38]
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$.
 **Lemma**: Let $F,F_i$ denote formulas, $w \in \Sigma^*$. Then
-  * $w \models (F_1 \lor F_2)$ iff $w \models F_1$ and $w \models F_2$
+  * $w \models (F_1 \lor F_2)$ iff $w \models F_1$ or $w \models F_2$
   * $w \models \lnot F$ iff $\lnot (w \models F)$
   * $w \models \exists x.F$ iff $\exists b. patch(w,x,b) \models F$
@@ Line 98: / Line 101: @@
   * if $q$ is a final state and $zero_x \in \Sigma$ is such that $zero_x(v)=0$ for all $x \neq v$, and if $\delta(q',zero_x)=q$, then set $q'$ also to be final
-**Example 1:** Compute automaton for formula $\exists X. \lnot (X \subseteq Y)$.
+**Example 1:** Compute automaton for formula $\exists X. \lnot (X \subseteq Y)$. MONA syntax:
+  var2 Y;
+  ex2 X: ~(X sub Y);
+Command to produce dot file:
+  mona -gw $1 | dot -Tps > output.ps
+**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)$.
-**Example 2:** Compute automaton for formula $\exists Y. (X < Y)$ where $<$ is interpreted treating $X,Y$ as digits of natural numbers.
+Define less-than relation in MONA and encode this example.
 ===== References =====