Differences

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

--- complexity [2007/10/04 22:06]
philippe.suter
+++ complexity [2007/10/05 01:03]
philippe.suter
@@ Line 1: / Line 1: @@
 ===== Complexity of the verification process =====
 ==== Preliminary remarks ====
@@ Line 14: / Line 15: @@
 === 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:
@@ Line 39: / Line 40: @@
   * $\forall x . S_1(x) \vee \ldots \vee S_n(x) \Leftrightarrow T(x)$
   * and $\forall x . \neg (E(x) \wedge F(x))$ respectively.
 ==== Verifying disjunction ====
@@ Line 45: / Line 47: @@
   - Either the patterns have different signatures, in which case we ignore their guards and verify that the interesection of their sets is empty...
   - ...or they have the same signature, in which case we simply verify that the conjunction of their guards is //false//.
 Since we limit our boolean expressions to QFBAPA (FIXME do we?), the formula for verifying the disjointness of two guards $g_1$ and $g_2$, namely $\neg(g_1 \wedge g_2)$ is itself in QFBAPA and its satisfiability can hence be checked with an algorithm in NP [1]. This solves the second case.
-The first case is not much harder. We can use the abovementioned equivalence for the intersection of cartesian products of same dimensions, and we need only one quantifier to transform it to the desired form:
+The first case is not much harder. We can use the abovementioned equivalence for the intersection of cartesian products of same dimensions, and we need to insert only one quantifier to transform it to the desired form:
   * $(A_1 \times A_2 \times \ldots \times A_n) \cap (B_1 \times B_2 \times \ldots \times B_n) = \emptyset$
@@ Line 58: / Line 58: @@
 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 ====
+As an introductory remark, note that checking for reachability of a pattern //p// is equivalent to checking that the preceding patterns do __not__ form a complete set over the values matched by //p//. With this in mind, observe that all formulas for checking completeness and reachability are in the form:
+\[ (S_1 \times \ldots \times S_n) \subseteq (A_1 \times \ldots \times A_n) \cup (\ldots) \cup (Z_1 \times \ldots \times Z_n) \]
+When checking completeness, the set $(S_1 \times \ldots \times S_n)$ is the domain of the scrutinee, when checking reachability, it is the set of the observed pattern. (Note that this is in fact checking subsumption. Proper reachability checking would include verifying that the pattern set is a subset of the scrutinee set, but this does not introduce any additional complexity.) Also note that the sets over which the union is taken correspond to patterns which satisfy one of the following properties:
+  * the pattern has no guard
+  * 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.
+Using $n$ quantifiers, we translate the previous (meta-)formula to:
+\[ \forall x_1, \ldots , x_n . (S_1(x_1) \wedge \ldots \wedge S_n(x_n)) \Rightarrow (A_1(x_1) \wedge \ldots \wedge A_n(x_n)) \vee (\ldots ) \vee (Z_1(x_1) \wedge \ldots \wedge Z_n(x_n)) \]
+Along with the axioms and with proper renaming of variables, we get a formula in the decidable prefix class $[\exists^* \forall^*] _{=}$..
+(FIXME) Now I'm not so sure.. I'd like to say that it's in fact in $[\exists^* \forall^{max_p(E)}]_{=}$, and that for a given pattern matching expression $max_p(E)$ is fixed, so the satisfiability of the underlying class is in NP, but I'm not sure that's allowed.. Is the fact that we can easily put a bound on $max_p(E)$ __for a given expression__ enough to say it's a fixed constant? Since it's dependant on the input, I would not think so..
+==== References ====
 [1] Quantifier Free Boolean Algebra with Presburger Arithmetic is NP-Complete, technical report somewhere IIRC.