Differences
This shows you the differences between two versions of the page.
sav08:using_automata_to_decide_ws1s [2012/05/15 12:48] 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 \\ | ||
- | 0, & \textsf{ if } v \neq x \land i > n \\ | ||
- | b_i, & \textsf{ if } v=x \land i \le m \\ | ||
- | 0, & \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. | ||
- | |||
- | ===== References ===== | ||
- | |||
- | * [[http://www.brics.dk/mona/mona14.pdf|MONA tool manual]] (Chapter 3, page 18) | ||