Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
using_automata_to_decide_msol_over_finite_strings [2007/05/16 10:44] vkuncak |
using_automata_to_decide_msol_over_finite_strings [2007/05/16 10:46] vkuncak |
||
---|---|---|---|
Line 40: | Line 40: | ||
NOTE: What if the witness is longer than $k$? | NOTE: What if the witness is longer than $k$? | ||
- | * add the strings of the form $[v_i \land \bigwedge_{j=1,j\neq i}^n v_j]*$ to the language of automaton | + | * concatenate the language of strings of the form $[\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$ | * there exists $k_0$ so that equivalence holds for all $k \ge k_0$ | ||