@phdthesis{14539,
  abstract     = {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.
},
  author       = {Zikelic, Dorde},
  isbn         = {978-3-99078-036-7},
  issn         = {2663 - 337X},
  pages        = {256},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Automated verification and control of infinite state stochastic systems}},
  doi          = {10.15479/14539},
  year         = {2023},
}