---
res:
  bibo_abstract:
  - "Stochastic systems provide a formal framework for modelling and quantifying uncertainty
    in systems and have been widely adopted in many application domains. Formal\r\nverification
    and control of finite state stochastic systems, a subfield of formal methods\r\nalso
    known as probabilistic model checking, is well studied. In contrast, formal verification
    and control of infinite state stochastic systems have received comparatively\r\nless
    attention. However, infinite state stochastic systems commonly arise in practice.\r\nFor
    instance, probabilistic models that contain continuous probability distributions
    such\r\nas normal or uniform, or stochastic dynamical systems which are a classical
    model for\r\ncontrol under uncertainty, both give rise to infinite state systems.\r\nThe
    goal of this thesis is to contribute to laying theoretical and algorithmic foundations\r\nof
    fully automated formal verification and control of infinite state stochastic systems,\r\nwith
    a particular focus on systems that may be executed over a long or infinite time.\r\nWe
    consider formal verification of infinite state stochastic systems in the setting
    of\r\nstatic analysis of probabilistic programs and formal control in the setting
    of controller\r\nsynthesis in stochastic dynamical systems. For both problems,
    we present some of the\r\nfirst fully automated methods for probabilistic (a.k.a.
    quantitative) reachability and\r\nsafety analysis applicable to infinite time
    horizon systems. We also advance the state\r\nof the art of probability 1 (a.k.a.
    qualitative) reachability analysis for both problems.\r\nFinally, for formal controller
    synthesis in stochastic dynamical systems, we present a\r\nnovel framework for
    learning neural network control policies in stochastic dynamical\r\nsystems with
    formal guarantees on correctness with respect to quantitative reachability,\r\nsafety
    or reach-avoid specifications.\r\n@eng"
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Dorde
      foaf_name: Zikelic, Dorde
      foaf_surname: Zikelic
      foaf_workInfoHomepage: http://www.librecat.org/personId=294AA7A6-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-4681-1699
  bibo_doi: 10.15479/14539
  dct_date: 2023^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/2663-337X
  - http://id.crossref.org/issn/978-3-99078-036-7
  dct_language: eng
  dct_publisher: Institute of Science and Technology Austria@
  dct_title: Automated verification and control of infinite state stochastic systems@
...