Talk on Approximating Fixed Points of Approximated Functions
Date:
Version of the CAV presentation associated to the paper of the same name, including first results of the TACAS paper.
Fixpoints are ubiquitous in computer science and when dealing with quantitative semantics and verification one is often interested in least fixpoints of (higher-dimensional) functions over the non-negative reals. How can one approximate the least fixpoint of such functions if they are not known precisely, but can only be approximated or sampled? In this setting, traditional fixpoint iteration schemes might get stuck at a fixpoint that is not the least or even diverge. We use a dampened variant of the Mann iteration scheme to overcome these problems and show convergence to the least fixpoint of the function of interest under suitable conditions.