LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:interval_analysis_and_widening [2009/01/21 14:53]
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*}