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 03:21] 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$ there exists $k_0$ so that 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$, |
| \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. What if the witness is longer than $k$? Then increase $k_0$. |
| This is because existentially quantifying over an integer is the same as existentially quantifying over all of its bits. | 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 50: | ||
| * 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]] | ||