Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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*}
  
  
 
sav08/interval_analysis_and_widening.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice