Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
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
 
© EPFL 2018 - Legal notice