Differences

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

--- sav08:using_automata_to_decide_ws1s [2012/05/15 15:11]
vkuncak
+++ sav08:using_automata_to_decide_ws1s [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-====== Using Automata to Decide WS1S ======
-Consider a formula $F$ of [[weak_monadic_logic_of_one_successor|WS1S]].  Let $V$ be a finite set of all variables in $F$.  We construct an automaton $A(F)$ in the finite alphabet
-\[
-   \Sigma = \Sigma_1^V
-\]
-for $\Sigma_1 = \{0,1\}$ such that the following property holds: for every $w \in \Sigma^*$,
-$w \in L(A(F))$ iff $e(F)(D,\alpha(w))={\it true} \ \ \ \ \ \  (*)$
-where $\alpha(w)$ is an interpretation of WS1S (mapping variables $V$ to finite sets) defined by
-\[
-   \alpha(a_0 \ldots a_n)(v) = \{ i \mid 0 \le i \le n \land a_i(v) = 1 \}
-\]
-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$ 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$
-     .......
-     .......  0
-     .......
-     bbbbbbbbbbbbbb
-     .......
-     .......  0
-     .......
-     _______
-        w
-     ______________
-      patch(w,x,b)
-Let $w = w_1 \ldots w_n$ where $w_i \in \Sigma$ and $b = b_1 \ldots b_m$ where $b_j \in \Sigma_1$.
-Let $N=\max(n,m)$. Define $patch(w,x,b) = p_1 \ldots p_N$ where $p_i \in \Sigma$ such that
-\[
-   p_i(v) = \left\{ \begin{array}{ll}
-w_i(v), & \textsf{ if } v \neq x \land i \le n \\
-, & \textsf{ if } v \neq x \land i > n \\
-b_i, & \textsf{ if } v=x \land i \le m \\
-, & \textsf{ if } v=x \land i > m
-\right.
-\]
-We define the automaton by recursion on the structure of formula.
-**Case** $A(x \subseteq y)$:
-++|Automaton for regular expression $[x \rightarrow y]^*$ ++
-**Case** $A(succ(x,y))$:
-++|Automaton for regular expression $[\lnot x \land \lnot y]^* [x \land \lnot y][\lnot x \land y] [\lnot x \land \lnot y]^*$ ++
-**Case** $A(F_1 \lor F_2)$:
-++|Automaton for union of regular languages, $A(F_1) \lor A(F_2)$ ++
-**Case** $A(\lnot F)$:
-++|Complement $\lnot A(F)$. ++
-**Example:** Use the rules above to compute (and minimize) the automaton for $\lnot ((\lnot (X \subseteq Y)) \land (\lnot (Y \subseteq X)))$.
-Proof of correctness if by induction. For example, for disjunction we have:
-  * $w \in L(A(F_1 \lor F_2))$
-  * $w \in L(A(F_1) \sqcup A(F_2)))$
-  * $w \in L(A(F_1)) \lor w \in L(A(F_2))$, so by I.H.
-  * $w \models F_1\  \lor\ w \models F_2$, so by Lemma above,
-  * $w \models (F_1 \lor F)$
-==== Existential Quantification ====
-**Case** $A(\exists x.F)$:
-To maintain the equivalence $(*)$ above, we need that for every word,
-\[
-    w \in L(A(\exists x.F))
-\]
-iff
-\[
-    \exists s \in \Sigma_1^*.\ patch(w,x,s) \in L(A(F))
-\]
-Given a deterministic automaton $A(F)$, we can construct a deterministic automaton
-accepting $\{ w \mid \exists s \in \Sigma_1^*.\ patch(w,x,s) \in L(A(F)) \}$ in two steps:
-  * take the same initial state
-  * for each transition $\delta(q,w)$ introduce transitions $\delta(q,w[x:=b])$ for all $b \in \Sigma_1$
-  * initially set final states as in the original automaton
-  * 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 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 =====
-  * [[http://www.brics.dk/mona/mona14.pdf|MONA tool manual]] (Chapter 3, page 18)