Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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