thesis published Dorde Zikelic author 294AA7A6-F248-11E8-B48F-1D18A9856A870000-0002-4681-1699 Krishnendu Chatterjee supervisor KrCh department GradSch department Formal Methods for Stochastic Models: Algorithms and Applications project International IST Doctoral Program project Stochastic systems provide a formal framework for modelling and quantifying uncertainty in systems and have been widely adopted in many application domains. Formal verification and control of finite state stochastic systems, a subfield of formal methods also known as probabilistic model checking, is well studied. In contrast, formal verification and control of infinite state stochastic systems have received comparatively less attention. However, infinite state stochastic systems commonly arise in practice. For instance, probabilistic models that contain continuous probability distributions such as normal or uniform, or stochastic dynamical systems which are a classical model for control under uncertainty, both give rise to infinite state systems. The goal of this thesis is to contribute to laying theoretical and algorithmic foundations of fully automated formal verification and control of infinite state stochastic systems, with a particular focus on systems that may be executed over a long or infinite time. We consider formal verification of infinite state stochastic systems in the setting of static analysis of probabilistic programs and formal control in the setting of controller synthesis in stochastic dynamical systems. For both problems, we present some of the first fully automated methods for probabilistic (a.k.a. quantitative) reachability and safety analysis applicable to infinite time horizon systems. We also advance the state of the art of probability 1 (a.k.a. qualitative) reachability analysis for both problems. Finally, for formal controller synthesis in stochastic dynamical systems, we present a novel framework for learning neural network control policies in stochastic dynamical systems with formal guarantees on correctness with respect to quantitative reachability, safety or reach-avoid specifications. https://research-explorer.ista.ac.at/download/14539/14540/main.pdf application/pdfno https://research-explorer.ista.ac.at/download/14539/14541/thesis_source.zip application/x-zip-compressed https://creativecommons.org/licenses/by-nc-sa/4.0/ Institute of Science and Technology Austria2023 eng 2663-337X 978-3-99078-036-710.15479/14539 256 https://research-explorer.ista.ac.at/record/10414 https://research-explorer.ista.ac.at/record/12000 https://research-explorer.ista.ac.at/record/9644 https://research-explorer.ista.ac.at/record/12511 https://research-explorer.ista.ac.at/record/14600 https://research-explorer.ista.ac.at/record/14601 https://research-explorer.ista.ac.at/record/1194 Zikelic D. Automated verification and control of infinite state stochastic systems. 2023. doi:<a href="https://doi.org/10.15479/14539">10.15479/14539</a> Zikelic D. 2023. Automated verification and control of infinite state stochastic systems. Institute of Science and Technology Austria. Zikelic, Dorde. <i>Automated Verification and Control of Infinite State Stochastic Systems</i>. Institute of Science and Technology Austria, 2023, doi:<a href="https://doi.org/10.15479/14539">10.15479/14539</a>. Zikelic, Dorde. “Automated Verification and Control of Infinite State Stochastic Systems.” Institute of Science and Technology Austria, 2023. <a href="https://doi.org/10.15479/14539">https://doi.org/10.15479/14539</a>. D. Zikelic, “Automated verification and control of infinite state stochastic systems,” Institute of Science and Technology Austria, 2023. D. Zikelic, Automated Verification and Control of Infinite State Stochastic Systems, Institute of Science and Technology Austria, 2023. Zikelic, D. (2023). <i>Automated verification and control of infinite state stochastic systems</i>. Institute of Science and Technology Austria. <a href="https://doi.org/10.15479/14539">https://doi.org/10.15479/14539</a> 145392023-11-15T13:39:10Z2026-04-07T13:27:56Z