Automated verification and control of infinite state stochastic systems
Zikelic D. 2023. Automated verification and control of infinite state stochastic systems. Institute of Science and Technology Austria.
Download
DOI
Thesis
| PhD
| Published
| English
Author
Supervisor
Department
Grant
Series Title
ISTA Thesis
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.
Publishing Year
Date Published
2023-11-15
Publisher
Institute of Science and Technology Austria
Page
256
ISBN
ISSN
IST-REx-ID
Cite this
Zikelic D. Automated verification and control of infinite state stochastic systems. 2023. doi:10.15479/14539
Zikelic, D. (2023). Automated verification and control of infinite state stochastic systems. Institute of Science and Technology Austria. https://doi.org/10.15479/14539
Zikelic, Dorde. “Automated Verification and Control of Infinite State Stochastic Systems.” Institute of Science and Technology Austria, 2023. https://doi.org/10.15479/14539.
D. Zikelic, “Automated verification and control of infinite state stochastic systems,” Institute of Science and Technology Austria, 2023.
Zikelic D. 2023. Automated verification and control of infinite state stochastic systems. Institute of Science and Technology Austria.
Zikelic, Dorde. Automated Verification and Control of Infinite State Stochastic Systems. Institute of Science and Technology Austria, 2023, doi:10.15479/14539.
All files available under the following license(s):
Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International (CC BY-NC-SA 4.0):
Main File(s)
File Name
main.pdf
2.12 MB
Access Level
Open Access
Date Uploaded
2023-11-15
MD5 Checksum
f23e002b0059ca78e1fbb864da52dd7e
Source File
File Name
thesis_source.zip
35.88 MB
Access Level
Closed Access
Date Uploaded
2023-11-15
MD5 Checksum
80ca37618a3c7b59866875f8be9b15ed
Material in ISTA:
Part of this Dissertation
Part of this Dissertation
Part of this Dissertation
Part of this Dissertation
Part of this Dissertation
Part of this Dissertation
Part of this Dissertation