Differences
This shows you the differences between two versions of the page.
| Both sides previous 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 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 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]] | ||