Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
using_automata_to_decide_msol_over_finite_strings [2007/05/16 03:50] vkuncak |
using_automata_to_decide_msol_over_finite_strings [2007/05/16 10:45] vkuncak |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| Compare this to [[Using automata to decide Presburger arithmetic]]. | Compare this to [[Using automata to decide Presburger arithmetic]]. | ||
| - | We will define $A(G)$ such that for every $G$ and for all $k \ge k_0$, for every matrix $a_{ij} \in \{0,1\}$ where for $1 \leq i \leq n$ and $1 \leq j \leq k$, | + | We will define $A(G)$ such that for every $G$ and for all $k$, for every matrix $a_{ij} \in \{0,1\}$ where for $1 \leq i \leq n$ and $1 \leq j \leq k$, |
| \begin{equation*} | \begin{equation*} | ||
| [\![G]\!] [v_i \mapsto \{j \mid a_{ij}=1 \}]_{i=1}^n = \mbox{true} | [\![G]\!] [v_i \mapsto \{j \mid a_{ij}=1 \}]_{i=1}^n = \mbox{true} | ||
| Line 40: | Line 40: | ||
| NOTE: What if the witness is longer than $k$? | NOTE: What if the witness is longer than $k$? | ||
| - | * add the strings of the form $[v_i]*$ to the language of automaton | + | * add the strings of the form $[v_i \land \bigwedge_{j=1,j\neq i}^n \lnot v_j]*$ to the language of automaton |
| * there exists $k_0$ so that equivalence holds for all $k \ge k_0$ | * there exists $k_0$ so that equivalence holds for all $k \ge k_0$ | ||