Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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 =====
 
sav08/using_automata_to_decide_ws1s.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice