Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

using_automata_to_decide_msol_over_finite_strings [2007/05/16 10:46]
vkuncak
using_automata_to_decide_msol_over_finite_strings [2007/05/16 10:46] (current)
vkuncak
Line 40: Line 40:
  
 NOTE: What if the witness is longer than $k$?  NOTE: What if the witness is longer than $k$? 
-  * concatenate the language of strings of the form $[v_i \land \bigwedge_{j=1,​j\neq i}^n \lnot v_j]*$ to the language of the 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$
  
 
using_automata_to_decide_msol_over_finite_strings.txt · Last modified: 2007/05/16 10:46 by vkuncak