Automated verification and control of infinite state stochastic systems

Thesis

Abstract

Acknowledgments

About the Author

List of Collaborators and Publications

Table of Contents

List of Figures

List of Tables

List of Algorithms

1 Introduction

2 Preliminaries

3 Lexicographic Methods for Almost-sure Termination Analysis in PPs

4 Quantitative Termination and Safety Analysis in PPs

5 Non-termination Analysis in Programs

6 Learning-based Stochastic Control with Almost-sure Reachability

7 Learning-based Stochastic Control with Quantitative Reach-avoidance

8 Discussion and Conclusion

Bibliography

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.