1: \begin{abstract}

2:   Fixpoints are ubiquitous in computer science and when dealing with

3:   quantitative semantics and verification one is commonly led to

4:   consider least fixpoints of (higher-dimensional) functions over the

5:   non-negative reals.

6:   %

7:   We show how to approximate the least fixpoint of such functions,

8:   focusing on the case in which they are not known precisely, but

9:   represented by a sequence of approximating functions that converge

10:   to them.

11:   %

12:   We concentrate on monotone and non-expansive functions, for which

13:   uniqueness of fixpoints is not guaranteed and standard fixpoint

14:   iteration schemes might get stuck at a fixpoint that is not the

15:   least.

16:   %

17:   Our main contribution is the identification of an iteration scheme,

18:   a variation of Mann iteration with a dampening factor, which, under

19:   suitable conditions, is shown to guarantee convergence to the least

20:   fixpoint of the function of interest.

21:   %

22:   We then argue that these results are relevant in the context of

23:   model-based reinforcement learning for Markov decision processes

24:   (MDPs), showing that the proposed iteration scheme instantiates

25:   to MDPs and allows us to derive convergence to the optimal expected return.

26:   %

27:   More generally, we show that our results can be used to iterate to

28:   the least fixpoint almost surely for systems where the function of

29:   interest can be approximated with given probabilistic error bounds,

30:   as it happens for probabilistic systems, such as simple stochastic games,

31:   that can be explored via sampling.

32: 

33:   %

34:   \keywords{Fixpoints, Approximation, Mann iteration, Markov Decision Processes}

35: \end{abstract}