• English only

# 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] (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 =====