Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
complexity [2007/10/04 23:18] philippe.suter |
complexity [2007/10/05 01:03] philippe.suter |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ===== Complexity of the verification process ===== | ===== Complexity of the verification process ===== | ||
| + | |||
| ==== Preliminary remarks ==== | ==== Preliminary remarks ==== | ||
| Line 14: | Line 15: | ||
| === Consistency of the dimensions of the cartesian products === | === Consistency of the dimensions of the cartesian products === | ||
| - | We know that to every pattern corresponds one cartesian product. By construction, the dimension of these products is always the same since it corresponds to $max_p(E)$. In particular, this means that taking the union of two "pattern sets" will yield yet another cartesian product with the same cardinality. | + | For every pattern, we build a cartesian product representing the set of inputs which it would match. By construction, the dimension of these products is always the same since it corresponds to $max_p(E)$. In particular, this means that taking the union of two "pattern sets" will yield yet another cartesian product with the same cardinality. |
| Note that we now also have: | Note that we now also have: | ||
| Line 39: | 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. | ||
| + | |||
| ==== Verifying disjunction ==== | ==== Verifying disjunction ==== | ||
| Line 55: | Line 57: | ||
| 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. | ||
| ==== Verifying completeness/reachability ==== | ==== Verifying completeness/reachability ==== | ||