Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:interval_analysis_and_widening [2008/05/20 20:34] vkuncak |
sav08:interval_analysis_and_widening [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 8: | Line 8: | ||
How to interpret a command | How to interpret a command | ||
- | \[ | + | \begin{equation*} |
x = y \otimes z | x = y \otimes z | ||
- | \] | + | \end{equation*} |
for some operation $\otimes$? | for some operation $\otimes$? | ||
$m(x) = $ ++++| | $m(x) = $ ++++| | ||
- | \[ | + | \begin{equation*} |
[\min \{v_y \otimes v_z \mid v_y \in m(y), v_z \in m(z) \}, | [\min \{v_y \otimes v_z \mid v_y \in m(y), v_z \in m(z) \}, | ||
\max \{v_y \otimes v_z \mid v_y \in m(y), v_z \in m(z) \}] | \max \{v_y \otimes v_z \mid v_y \in m(y), v_z \in m(z) \}] | ||
- | \] | + | \end{equation*} |
++++ | ++++ | ||
Line 35: | Line 35: | ||
In fixpoint computation, compose $H_i$ with function | In fixpoint computation, compose $H_i$ with function | ||
- | \[ | + | \begin{equation*} |
w([a,b]) = [\max \{x \in J \mid x \le a\}, | w([a,b]) = [\max \{x \in J \mid x \le a\}, | ||
\min \{x \in J \mid b \le x\}] | \min \{x \in J \mid b \le x\}] | ||
- | \] | + | \end{equation*} |
Approaches: | Approaches: | ||
Line 55: | Line 55: | ||
Observation: if $F^{\#}$ and $W$ are $\omega$-continuous functions and $x \sqsubseteq W(x)$ for all $x$, then narrowing will improve the result, that is, if $x_* = lfp (F^{\#})$ and $y_* = lfp (W \circ F^{\#})$, then $x_* \sqsubseteq y_*$ and | Observation: if $F^{\#}$ and $W$ are $\omega$-continuous functions and $x \sqsubseteq W(x)$ for all $x$, then narrowing will improve the result, that is, if $x_* = lfp (F^{\#})$ and $y_* = lfp (W \circ F^{\#})$, then $x_* \sqsubseteq y_*$ and | ||
- | \[ | + | \begin{equation*} |
- | x_* = F(x_*) \sqsubseteq F^{\#}(y_*) \sqsubseteq (W \circ F^{\#})(y_*) \sqsubseteq y_* | + | x_* = F^{\#}(x_*) \sqsubseteq F^{\#}(y_*) \sqsubseteq (W \circ F^{\#})(y_*) \sqsubseteq y_* |
- | \] | + | \end{equation*} |