Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:using_automata_to_decide_ws1s [2012/05/15 15:11] vkuncak |
sav08:using_automata_to_decide_ws1s [2015/04/21 17:30] (current) |
||
|---|---|---|---|
| Line 2: | Line 2: | ||
| 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 | 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 | ||
| - | \[ | + | \begin{equation*} |
| \Sigma = \Sigma_1^V | \Sigma = \Sigma_1^V | ||
| - | \] | + | \end{equation*} |
| for $\Sigma_1 = \{0,1\}$ such that the following property holds: for every $w \in \Sigma^*$, | for $\Sigma_1 = \{0,1\}$ such that the following property holds: for every $w \in \Sigma^*$, | ||
| Line 10: | Line 10: | ||
| where $\alpha(w)$ is an interpretation of WS1S (mapping variables $V$ to finite sets) defined by | where $\alpha(w)$ is an interpretation of WS1S (mapping variables $V$ to finite sets) defined by | ||
| - | \[ | + | \begin{equation*} |
| \alpha(a_0 \ldots a_n)(v) = \{ i \mid 0 \le i \le n \land a_i(v) = 1 \} | \alpha(a_0 \ldots a_n)(v) = \{ i \mid 0 \le i \le n \land a_i(v) = 1 \} | ||
| - | \] | + | \end{equation*} |
| Instead of $e(F)(D,\alpha(w))={\it true}$ we write for short $w \models F$. So, we design automata so that: | Instead of $e(F)(D,\alpha(w))={\it true}$ we write for short $w \models F$. So, we design automata so that: | ||
| - | \[ | + | \begin{equation*} |
| w \in L(A(F)) \ \ \ \iff \ \ \ w \models F | w \in L(A(F)) \ \ \ \iff \ \ \ w \models F | ||
| - | \] | + | \end{equation*} |
| 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 40: | Line 40: | ||
| 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 $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 | Let $N=\max(n,m)$. Define $patch(w,x,b) = p_1 \ldots p_N$ where $p_i \in \Sigma$ such that | ||
| - | \[ | + | \begin{equation*} |
| p_i(v) = \left\{ \begin{array}{ll} | p_i(v) = \left\{ \begin{array}{ll} | ||
| w_i(v), & \textsf{ if } v \neq x \land i \le n \\ | w_i(v), & \textsf{ if } v \neq x \land i \le n \\ | ||
| Line 47: | Line 47: | ||
| 0, & \textsf{ if } v=x \land i > m | 0, & \textsf{ if } v=x \land i > m | ||
| \right. | \right. | ||
| - | \] | + | \end{equation*} |
| Line 85: | Line 85: | ||
| To maintain the equivalence $(*)$ above, we need that for every word, | To maintain the equivalence $(*)$ above, we need that for every word, | ||
| - | \[ | + | \begin{equation*} |
| w \in L(A(\exists x.F)) | w \in L(A(\exists x.F)) | ||
| - | \] | + | \end{equation*} |
| iff | iff | ||
| - | \[ | + | \begin{equation*} |
| \exists s \in \Sigma_1^*.\ patch(w,x,s) \in L(A(F)) | \exists s \in \Sigma_1^*.\ patch(w,x,s) \in L(A(F)) | ||
| - | \] | + | \end{equation*} |
| Line 101: | 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 | * 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. Also compute the automaton for the formula $\exists X. (X < Y)$. | ||
| + | |||
| + | Define less-than relation in MONA and encode this example. | ||
| ===== References ===== | ===== References ===== | ||