Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
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] 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 $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*} | \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 37: | Line 37: | ||
**Case** $A(\exists v_i. G)$ | **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 $[v_i \land \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. | 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. |