LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
complexity [2007/10/05 01:03]
philippe.suter
complexity [2007/10/05 01:58]
philippe.suter
Line 40: Line 40:
   * $\forall x . S_1(x) \vee \ldots \vee S_n(x) \Leftrightarrow T(x)$   * $\forall x . S_1(x) \vee \ldots \vee S_n(x) \Leftrightarrow T(x)$
   * and $\forall x . \neg (E(x) \wedge F(x))$ respectively.   * and $\forall x . \neg (E(x) \wedge F(x))$ respectively.
 +
  
  
Line 58: Line 59:
 Note that checking the satifiability should be doable in polynomial time, as all needs to be done is find one pair of sets among a finite list which are disjoint (and this information can only come from the assumptions/​axioms,​ which are themselves in a finite number. (FIXME : I know this doesn'​t sound convincing.. let's do better). Note that checking the satifiability should be doable in polynomial time, as all needs to be done is find one pair of sets among a finite list which are disjoint (and this information can only come from the assumptions/​axioms,​ which are themselves in a finite number. (FIXME : I know this doesn'​t sound convincing.. let's do better).
  
-We can also rely on the fact that we introduced only one quantifier and that the size of the generated formula is linear in terms of the size of the original one. This formula is hence in $[\exists^{*} \forall^{1}]_{=}]$ and checking its validity can be done in NP time.+We can also rely on the fact that we introduced only one quantifier and that the size of the generated formula is linear in terms of the size of the original one. This formula is hence in $[\exists^{*} \forall^{1}]_{=}$ and checking its validity can hence be done in NP time. 
  
 ==== Verifying completeness/​reachability ==== ==== Verifying completeness/​reachability ====
Line 70: Line 72:
   * the pattern has a guard, but there exists a set of patterns with the same signature such that the disjunction of their guards is equivalent to the true statement   * the pattern has a guard, but there exists a set of patterns with the same signature such that the disjunction of their guards is equivalent to the true statement
  
-Again, checking that second property on a disjunction of guards $\bigvee_i g_i$ can be checked ​in NPTIME.+Again, checking that second property on a disjunction of guards $\bigvee_i g_i$ can be done in NPTIME.
  
 Using $n$ quantifiers,​ we translate the previous (meta-)formula to: Using $n$ quantifiers,​ we translate the previous (meta-)formula to: