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/15 21:06] vkuncak |
using_automata_to_decide_msol_over_finite_strings [2007/05/16 10:44] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Using automata to decide MSOL over strings ====== | ====== Using automata to decide MSOL over strings ====== | ||
- | |||
- | |||
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 39: | 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$? | ||
+ | * add the strings of the form $[v_i]*$ to the language of 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. | ||
- | |||
- | |||
===== Complexity ===== | ===== Complexity ===== | ||
Line 54: | Line 53: | ||
* the density question | * the density question | ||
* do we need to know how to check validity for all MSOL formulas | * do we need to know how to check validity for all MSOL formulas | ||
+ | |||
+ | ===== References ===== | ||
+ | |||
+ | * [[http://www.brics.dk/mona/mona14.pdf|MONA tool manual]] | ||