- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

Both sides previous revision Previous revision Next revision | Previous revision | ||

complexity [2007/10/05 01:03] philippe.suter |
complexity [2015/04/21 17:32] (current) |
||
---|---|---|---|

Line 19: | Line 19: | ||

Note that we now also have: | Note that we now also have: | ||

- | \[ (A_1 \times A_2 \times \ldots \times A_n) \cap (B_1 \times B_2 \times \ldots \times B_n) = \emptyset \iff (A_1 \cap B_1 = \emptyset ) \vee (A_2 \cap B_2 = \emptyset ) \vee \ldots \vee (A_n \cap B_n = \emptyset ) \] | + | \begin{equation*} (A_1 \times A_2 \times \ldots \times A_n) \cap (B_1 \times B_2 \times \ldots \times B_n) = \emptyset \iff (A_1 \cap B_1 = \emptyset ) \vee (A_2 \cap B_2 = \emptyset ) \vee \ldots \vee (A_n \cap B_n = \emptyset ) \end{equation*} |

The proof is straightforward, but still requires that the dimensions match, otherwise the intersection could be empty for this other reason. | The proof is straightforward, but still requires that the dimensions match, otherwise the intersection could be empty for this other reason. | ||

Line 60: | Line 60: | ||

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. | 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 65: | Line 66: | ||

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: | 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) \] | + | \begin{equation*} (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) \end{equation*} |

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: | 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: | ||

Line 71: | 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: | ||

- | \[ \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)) \] | + | \begin{equation*} \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)) \end{equation*} |

Along with the axioms and with proper renaming of variables, we get a formula in the decidable prefix class $[\exists^* \forall^*] _{=}$.. | Along with the axioms and with proper renaming of variables, we get a formula in the decidable prefix class $[\exists^* \forall^*] _{=}$.. |