• English only

# Differences

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

 sav08:interval_analysis_and_widening [2008/05/20 20:34]vkuncak sav08:interval_analysis_and_widening [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2009/01/21 14:53 vkuncak 2008/05/20 20:34 vkuncak 2008/05/20 20:33 vkuncak 2008/05/20 20:32 vkuncak 2008/05/20 19:58 vkuncak 2008/05/20 19:58 vkuncak 2008/05/20 19:53 vkuncak 2008/05/20 19:04 vkuncak 2008/05/20 16:46 vkuncak 2008/05/20 16:39 vkuncak 2008/05/20 16:39 vkuncak 2008/05/20 16:37 vkuncak 2008/05/20 16:20 vkuncak 2008/05/20 16:19 vkuncak 2008/05/20 16:19 vkuncak 2008/05/20 15:55 vkuncak 2008/05/20 15:48 vkuncak 2008/05/20 15:48 vkuncak 2008/05/20 15:42 vkuncak created Next revision Previous revision 2009/01/21 14:53 vkuncak 2008/05/20 20:34 vkuncak 2008/05/20 20:33 vkuncak 2008/05/20 20:32 vkuncak 2008/05/20 19:58 vkuncak 2008/05/20 19:58 vkuncak 2008/05/20 19:53 vkuncak 2008/05/20 19:04 vkuncak 2008/05/20 16:46 vkuncak 2008/05/20 16:39 vkuncak 2008/05/20 16:39 vkuncak 2008/05/20 16:37 vkuncak 2008/05/20 16:20 vkuncak 2008/05/20 16:19 vkuncak 2008/05/20 16:19 vkuncak 2008/05/20 15:55 vkuncak 2008/05/20 15:48 vkuncak 2008/05/20 15:48 vkuncak 2008/05/20 15:42 vkuncak created 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*}