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/14 15:36] vkuncak |
using_automata_to_decide_msol_over_finite_strings [2007/05/16 02:19] 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]]. | ||
Line 11: | Line 9: | ||
iff | iff | ||
\begin{equation*} | \begin{equation*} | ||
- | (a_{11},a_{12},\ldots,a_{1n}) ... (a_{k1},a_{k2},\ldots,a_{kn}) \in L(A(G)) | + | (a_{11},a_{21},\ldots,a_{n1}) ... (a_{1k},a_{2k},\ldots,a_{nk}) \in L(A(G)) |
\end{equation*} | \end{equation*} | ||
Line 44: | Line 42: | ||
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]] | ||