---
_id: '14539'
abstract:
- lang: eng
  text: "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"
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Dorde
  full_name: Zikelic, Dorde
  id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
  last_name: Zikelic
  orcid: 0000-0002-4681-1699
citation:
  ama: 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>
  apa: 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>
  chicago: 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>.
  ieee: D. Zikelic, “Automated verification and control of infinite state stochastic
    systems,” Institute of Science and Technology Austria, 2023.
  ista: Zikelic D. 2023. Automated verification and control of infinite state stochastic
    systems. Institute of Science and Technology Austria.
  mla: 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>.
  short: D. Zikelic, Automated Verification and Control of Infinite State Stochastic
    Systems, Institute of Science and Technology Austria, 2023.
date_created: 2023-11-15T13:39:10Z
date_published: 2023-11-15T00:00:00Z
date_updated: 2025-07-14T09:10:10Z
day: '15'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: KrCh
- _id: GradSch
doi: 10.15479/14539
ec_funded: 1
file:
- access_level: open_access
  checksum: f23e002b0059ca78e1fbb864da52dd7e
  content_type: application/pdf
  creator: cchlebak
  date_created: 2023-11-15T13:43:28Z
  date_updated: 2023-11-15T13:43:28Z
  file_id: '14540'
  file_name: main.pdf
  file_size: 2116426
  relation: main_file
  success: 1
- access_level: closed
  checksum: 80ca37618a3c7b59866875f8be9b15ed
  content_type: application/x-zip-compressed
  creator: cchlebak
  date_created: 2023-11-15T13:44:24Z
  date_updated: 2023-11-15T13:44:24Z
  file_id: '14541'
  file_name: thesis_source.zip
  file_size: 35884057
  relation: source_file
file_date_updated: 2023-11-15T13:44:24Z
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-sa/4.0/
month: '11'
oa: 1
oa_version: Published Version
page: '256'
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
  call_identifier: H2020
  grant_number: '665385'
  name: International IST Doctoral Program
publication_identifier:
  isbn:
  - 978-3-99078-036-7
  issn:
  - 2663 - 337X
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
  record:
  - id: '1194'
    relation: part_of_dissertation
    status: public
  - id: '12000'
    relation: part_of_dissertation
    status: public
  - id: '12511'
    relation: part_of_dissertation
    status: public
  - id: '14600'
    relation: part_of_dissertation
    status: public
  - id: '14601'
    relation: part_of_dissertation
    status: public
  - id: '9644'
    relation: part_of_dissertation
    status: public
  - id: '10414'
    relation: part_of_dissertation
    status: public
status: public
supervisor:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
title: Automated verification and control of infinite state stochastic systems
tmp:
  image: /images/cc_by_nc_sa.png
  legal_code_url: https://creativecommons.org/licenses/by-nc-sa/4.0/legalcode
  name: Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International (CC
    BY-NC-SA 4.0)
  short: CC BY-NC-SA (4.0)
type: dissertation
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2023'
...