Differences

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

--- using_automata_to_decide_msol_over_finite_strings [2007/05/16 02:19]
vkuncak
+++ using_automata_to_decide_msol_over_finite_strings [2007/05/16 10:46] (current)
vkuncak
@@ Line 3: / Line 3: @@
 Compare this to [[Using automata to decide Presburger arithmetic]].
-We will define $A(G)$ such that for every $k$ and 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*}
   [\![G]\!] [v_i \mapsto \{j \mid a_{ij}=1 \}]_{i=1}^n = \mbox{true}
@@ Line 37: / Line 37: @@
 **Case** $A(\exists v_i. G)$
-This is projection operation on an automaton.  Take $A(G)$ and replace each transition with label $(a_1,\ldots,a_i,\ldots,a_n)$ with two transitions $(a_1,\ldots,0,\ldots,a_n)$ and $(a_1,\ldots,1,\ldots,a_n)$ into the same destination state.
+This is projection operation on an automaton.  Take $A(G)$ and replace each transition with label $(a_1,\ldots,a_i,\ldots,a_n)$ with two transitions $(a_1,\ldots,0,\ldots,a_n)$ and $(a_1,\ldots,1,\ldots,a_n)$ into the same destination state.  This is because existentially quantifying over an integer is the same as existentially quantifying over all of its bits.
+NOTE: What if the witness is longer than $k$?
+  * concatenate the language of strings of the form $[\bigwedge_{j=1,j\neq i}^n \lnot v_j]*$ to the language of the automaton
+  * there exists $k_0$ so that equivalence holds for all $k \ge k_0$
-This is because existentially quantifying over an integer is the same as existentially quantifying over all of its bits.
 As in the case of [[Using automata to decide Presburger arithmetic|Presbuger arithmetic]], to check if $F$ is satisfiable, we construct $A(F)$ as a deterministic automaton and check whether the graph of $A(F)$ has a reachable accepting state.