{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:15Z","timestamp":1776333495145,"version":"3.51.2"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986789","type":"print"},{"value":"9783031986796","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Fixpoints are ubiquitous in computer science and when dealing\u00a0with quantitative semantics and verification one often considers\u00a0least fixpoints of (higher-dimensional) functions over the non-negative reals. We show how to approximate the least fixpoint of such functions, focusing on the case in which they are not known precisely,\u00a0but represented by a sequence of approximating functions that converge to them. We concentrate on monotone and non-expansive functions, for\u00a0which uniqueness of fixpoints is not guaranteed and standard fixpoint iteration schemes might get stuck at a fixpoint that is not\u00a0the least. Our main contribution is the identification of an iteration scheme, a variation of Mann iteration with a dampening factor, which,\u00a0under suitable conditions, is shown to guarantee convergence to the\u00a0least fixpoint of the function of interest. We then argue that these results are relevant in the context\u00a0of model-based reinforcement learning for Markov decision processes, showing how the proposed iteration scheme instantiates and allows\u00a0us to derive convergence to the optimal expected return. More generally, we show that our results can be used to iterate\u00a0to the least fixpoint almost surely for systems where the function\u00a0of interest can be approximated with given probabilistic error bounds, as it happens for probabilistic systems which can be explored via sampling.<\/jats:p>","DOI":"10.1007\/978-3-031-98679-6_9","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:20:46Z","timestamp":1753089646000},"page":"193-215","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Approximating Fixpoints of\u00a0Approximated Functions"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9357-5599","authenticated-orcid":false,"given":"Paolo","family":"Baldan","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0008-4343-1384","authenticated-orcid":false,"given":"Sebastian","family":"Gurke","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4193-2889","authenticated-orcid":false,"given":"Barbara","family":"K\u00f6nig","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7814-1485","authenticated-orcid":false,"given":"Tommaso","family":"Padoan","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8307-503X","authenticated-orcid":false,"given":"Florian","family":"Wittbold","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: On-the-fly exact computation of bisimilarity distances. Log. Methods Comput. Sci. 13(2:13), 1\u201325 (2017)","DOI":"10.23638\/LMCS-13(2:13)2017"},{"key":"9_CR2","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press (2008)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Baldan, P., Gurke, S., K\u00f6nig, B., Padoan, T., Wittbold, F.: Approximating fixpoints of approximated functions (2025). arXiv:2501.08950","DOI":"10.1007\/978-3-031-98679-6_9"},{"issue":"1","key":"9_CR4","doi-asserted-by":"publisher","first-page":"133","DOI":"10.4064\/fm-3-1-133-181","volume":"3","author":"S Banach","year":"1922","unstructured":"Banach, S.: Sur les op\u00e9rations dans les ensembles abstraits et leur application aux \u00e9quations int\u00e9grales. Fundam. Math. 3(1), 133\u2013181 (1922)","journal-title":"Fundam. Math."},{"issue":"5","key":"9_CR5","first-page":"679","volume":"6","author":"R Bellman","year":"1957","unstructured":"Bellman, R.: A Markovian decision process. J. Math. Mech. 6(5), 679\u2013684 (1957)","journal-title":"J. Math. Mech."},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Berinde, V.: Iterative Approximation of Fixed Points. Lecture Notes in Mathematics, vol. 1912. Springer (2007)","DOI":"10.1109\/SYNASC.2007.49"},{"key":"9_CR7","unstructured":"Bertsekas, D.P., Tsitsiklis, J.N.: Neuro-Dynamic Programming. Athena Scientific, Belmont, Massachusetts (1996)"},{"key":"9_CR8","unstructured":"Billingsley, P.: Probability and Measure. Wiley Series in Probability and Mathematical Statistics, 3rd edn. Wiley, New York (1995)"},{"issue":"1","key":"9_CR9","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1016\/0022-247X(91)90139-Q","volume":"157","author":"D Borwein","year":"1991","unstructured":"Borwein, D., Borwein, J.: Fixed point iterations for real functions. J. Math. Anal. Appl. 157(1), 112\u2013126 (1991)","journal-title":"J. Math. Anal. Appl."},{"issue":"1","key":"9_CR10","doi-asserted-by":"publisher","first-page":"21","DOI":"10.4153\/CMB-1992-003-0","volume":"35","author":"J Borwein","year":"1992","unstructured":"Borwein, J., Reich, S., Shafrir, I.: Krasnoselski-Mann iterations in normed spaces. Can. Math. Bull. 35(1), 21\u201328 (1992)","journal-title":"Can. Math. Bull."},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-11936-6_8","volume-title":"Automated Technology for Verification and Analysis","author":"T Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil, T., et al.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98\u2013114. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8"},{"issue":"2","key":"9_CR12","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0890-5401(92)90048-K","volume":"96","author":"A Condon","year":"1992","unstructured":"Condon, A.: The complexity of stochastic games. Inf. Comput. 96(2), 203\u2013224 (1992)","journal-title":"Inf. Comput."},{"key":"9_CR13","unstructured":"Cousot, P.: Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice. Research report R.R. 88, Laboratoire IMAG, Universit\u00e9 scientifique et m\u00e9dicale de Grenoble, Grenoble, France (1977)"},{"issue":"1","key":"9_CR14","doi-asserted-by":"publisher","first-page":"43","DOI":"10.2140\/pjm.1979.82.43","volume":"82","author":"R Cousot","year":"1979","unstructured":"Cousot, R., Cousot, P.: Constructive versions of Tarski\u2019s fixed point theorems. Pac. J. Math. 82(1), 43\u201357 (1979)","journal-title":"Pac. J. Math."},{"key":"9_CR15","unstructured":"de Alfaro, L.: Formal Verification of Probabilistic Systems. Ph.D. thesis, Stanford University (1997)"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Dong, Q.-L., Cho, Y.J., He, S., Pardalos, P.M., Rassias, T.M.: The Krasnosel\u2019ski\u012d-Mann Iterative Method Recent Progress and Applications. SpringerBriefs in Optimization, 1st edn. Springer, Cham (2022)","DOI":"10.1007\/978-3-030-91654-1"},{"key":"9_CR17","unstructured":"Duflo, M.: Random Iterative Models. Number\u00a034 in Applications of Mathematics \u2013 Stochastic Modelling and Applied Probability. Springer (1991). Translated by Stephen S. Wilson"},{"issue":"1","key":"9_CR18","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1115\/1.3657260","volume":"84","author":"JH Eaton","year":"1962","unstructured":"Eaton, J.H., Zadeh, L.A.: Optimal pursuit strategies in discrete-state probabilistic systems. J. Basic Eng. 84(1), 23\u201329 (1962)","journal-title":"J. Basic Eng."},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Frommer, A., Szyld, D.B.: On asynchronous iterations. J. Comput. Appl. Math. 123(1), 201\u2013216 (2000). Numerical Analysis 2000. Vol. III: Linear Algebra","DOI":"10.1016\/S0377-0427(00)00409-X"},{"key":"9_CR20","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/j.tcs.2016.12.003","volume":"735","author":"S Haddad","year":"2018","unstructured":"Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theoret. Comput. Sci. 735, 111\u2013131 (2018)","journal-title":"Theoret. Comput. Sci."},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-030-53291-8_26","volume-title":"Computer Aided Verification","author":"A Hartmanns","year":"2020","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 488\u2013511. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_26"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"He, S., Zhu, W.: A modified Mann iteration by boundary point method for finding minimum-norm fixed point of nonexpansive mappings. Abstr. Appl. Anal. 2013 (2013). Article ID 768595","DOI":"10.1155\/2013\/768595"},{"issue":"301","key":"9_CR23","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1080\/01621459.1963.10500830","volume":"58","author":"W Hoeffding","year":"1963","unstructured":"Hoeffding, W.: Probability inequalities for sums of bounded random variables. J. Am. Stat. Assoc. 58(301), 13\u201330 (1963)","journal-title":"J. Am. Stat. Assoc."},{"key":"9_CR24","unstructured":"Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: Proceedings of LICS 1997. IEEE (1997)"},{"key":"9_CR25","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1613\/jair.301","volume":"4","author":"LP Kaelbling","year":"1996","unstructured":"Kaelbling, L.P., Littman, M.L., Moore, A.W.: Reinforcement learning: a survey. J. Artif. Intell. Res. 4, 237\u2013285 (1996)","journal-title":"J. Artif. Intell. Res."},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1007\/978-3-319-96145-3_36","volume-title":"Computer Aided Verification","author":"E Kelmendi","year":"2018","unstructured":"Kelmendi, E., Kr\u00e4mer, J., K\u0159et\u00ednsk\u00fd, J., Weininger, M.: Value iteration for simple stochastic games: stopping criterion and learning algorithm. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 623\u2013642. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_36"},{"issue":"1","key":"9_CR27","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.na.2004.11.011","volume":"61","author":"T-H Kim","year":"2005","unstructured":"Kim, T.-H., Hong-Kun, X.: Strong convergence of modified Mann iterations. Nonlinear Anal. Theory Methods Appl. 61(1), 51\u201360 (2005)","journal-title":"Nonlinear Anal. Theory Methods Appl."},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Kumar, P.R., Varaiya, P.: Stochastic Systems. Society for Industrial and Applied Mathematics, Philadelphia (2015)","DOI":"10.1137\/1.9781611974263"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Kushner, H.J., Clark, D.S.: Stochastic Approximation Methods for Constrained and Unconstrained Systems. Number\u00a026 in Applied Mathematical Sciences. Springer (1978)","DOI":"10.1007\/978-1-4684-9352-8"},{"issue":"3\u20134","key":"9_CR30","first-page":"317","volume":"150","author":"M Mio","year":"2017","unstructured":"Mio, M., Simpson, A.: \u0141ukasiewicz $$\\mu $$-calculus. Fund. Inform. 150(3\u20134), 317\u2013346 (2017)","journal-title":"Fund. Inform."},{"key":"9_CR31","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1023\/A:1022635613229","volume":"13","author":"AW Moore","year":"1990","unstructured":"Moore, A.W., Atkeson, C.G.: Prioritized sweeping: reinforcement learning with less data and less time. Mach. Learn. 13, 103\u2013130 (1990)","journal-title":"Mach. Learn."},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics. Wiley (1994)","DOI":"10.1002\/9780470316887"},{"key":"9_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1007\/978-3-319-96145-3_37","volume-title":"Computer Aided Verification","author":"T Quatmann","year":"2018","unstructured":"Quatmann, T., Katoen, J.-P.: Sound value iteration. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 643\u2013661. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_37"},{"issue":"2","key":"9_CR34","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1016\/0022-247X(79)90024-6","volume":"67","author":"S Reich","year":"1979","unstructured":"Reich, S.: Weak convergence theorems for nonexpansive mappings in banach spaces. J. Math. Anal. Appl. 67(2), 274\u2013276 (1979)","journal-title":"J. Math. Anal. Appl."},{"issue":"3","key":"9_CR35","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1214\/aoms\/1177729586","volume":"22","author":"H Robbins","year":"1951","unstructured":"Robbins, H., Monro, S.: A stochastic approximation method. Ann. Math. Stat. 22(3), 400\u2013407 (1951)","journal-title":"Ann. Math. Stat."},{"key":"9_CR36","unstructured":"Rummery, G.A., Niranjan, M.: On-line Q-learning using connectionist systems, vol. 37. University of Cambridge, Department of Engineering Cambridge, UK (1994)"},{"issue":"4","key":"9_CR37","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1145\/122344.122377","volume":"2","author":"RS Sutton","year":"1991","unstructured":"Sutton, R.S.: Dyna, an integrated architecture for learning, planning, and reacting. SIGART Bull. 2(4), 160\u2013163 (1991)","journal-title":"SIGART Bull."},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Sutton, R.S.: Planning by incremental dynamic programming. In: Proceedings of ML 1991 (Conference on Machine Learning), pp. 353\u2013357. Morgan Kaufmann (1991)","DOI":"10.1016\/B978-1-55860-200-7.50073-8"},{"key":"9_CR39","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5, 285\u2013309 (1955)","journal-title":"Pac. J. Math."},{"key":"9_CR40","first-page":"279","volume":"8","author":"J Christopher","year":"1992","unstructured":"Christopher, J.: Watkins and Peter Dayan. Q-learning. Mach. Learn. 8, 279\u2013292 (1992)","journal-title":"Mach. Learn."},{"key":"9_CR41","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/s12190-008-0139-z","volume":"29","author":"Y Yao","year":"2008","unstructured":"Yao, Y., Zhou, H., Liou, Y.-C.: Strong convergence of a modified Krasnoselski-Mann iterative algorithm for non-expansive mappings. J. Appl. Math. Comput. 29, 383\u2013389 (2008)","journal-title":"J. Appl. Math. Comput."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98679-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,7]],"date-time":"2025-09-07T16:17:56Z","timestamp":1757261876000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98679-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986789","9783031986796"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98679-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}