Safety verification of discrete-time stochastic systems

Abstract

Cyber-physical systems integrate digital control and physical processes and often operate in complex, uncertain environments. The consequence of operational failures in such systems can be catastrophic and may include loss of life, environmental damage, irreparable system damage, and economic disruption. Therefore, safety is a critical concern and traditional engineering approaches that only rely on extensive testing and conservative design margins are insufficient to guarantee safety in the face of uncertainty. The issue is that testing only assesses the performance on a limited number of scenarios or samples, while in practice the collection of possible scenarios is uncountable due to the physical process and uncertainties therein. Formal methods provide a powerful alternative, offering mathematically rigorous verification that accounts for all possible behaviours subject to ranges of disturbances and uncertainties. A key challenge in applying formal methods to stochastic dynamical systems is a fundamental tension between computational tractability and conservatism. Existing approaches either scale poorly with the system dimension and complexity or produce loose bounds on safety probabilities that limit their practical applicability. This creates a critical gap between theory and practice: while formal verification methods exist, their practical applicability to real-world systems remains severely limited. Therefore, the core research question driving this work is: How to efficiently compute tight bounds on the satisfaction probabilities for safety, reachability, and reach-avoid specifications of stochastic systems?

To answer this question and address the gap, the present dissertation develops several complementary approaches for efficiently verifying properties of stochastic systems. The focus is on discrete-time, continuous-space stochastic systems and simple specifications over given sets. The approaches represent points along the spectrum of the scalability-conservatism trade-off and rely on different system assumptions. The methods developed belong to two families: stochastic barrier functions and finite-state abstractions.

Stochastic barrier functions are Lyapunov-like functions that provide certificates of safety by imposing conditions on the expected value of the barrier function along system trajectories. The core idea is that if the composition of the barrier function with the dynamics of the system forms a c-martingale, then the probability of safety can be bounded using martingale inequalities. The main challenge is to construct a barrier that is optimal with respect to the martingale inequalities. Hand-crafting such functions is difficult and time-consuming, and existing synthesis methods are often limited to low-dimensional and simple systems for non-trivial results. To enable efficient synthesis of stochastic barrier functions, we develop multiple synthesis techniques, including a neural network-based method that offers flexibility but requires post hoc verification to confirm correctness. More significantly, we introduce piecewise-constant stochastic barrier function theory and synthesis methods that are guaranteed to asymptotically approach optimality. The synthesis methods include a dual linear programming formulation, a counterexample-guided inductive synthesis with linear programming solvers, and gradient descent optimization; their trade-off is between scalability and required parameter tuning. The theoretical analysis of piece-wise constant barriers reveals deep insights into the relationship between barrier functions and system dynamics, illuminates fundamental sources of conservatism inherent to the approach, and establishes clear connections to Interval Markov Decision Process (IMDP)-based finite-state abstractions. Additionally, we develop a data-driven scenario-theoretic approach for systems with partially unknown dynamics, leveraging scenario theory to handle uncertainty in system models.

Finite-state abstractions, on the other hand, reduce the original continuous-space system to a finite-state model that can be analysed using probabilistic model checking techniques. While abstraction-based methods are exceedingly flexible -- they have been successfully applied to a wide range of systems, including partially-unknown systems, and specifications -- they often suffer from high computational complexity of using probabilistic model checking and scalability issues due to the pervasive state-space explosion problem.  To address the first issue, we develop hardware-aware algorithmic innovations for faster model checking of IMDPs via dynamic programming. Dynamic programming over IMDPs relies for efficiency on an algorithm named O-maximization, or order-maximization, which by theoretical analysis is revealed to be composed of two phases: a sorting phase and a cumulative summation phase. We introduce parallel algorithms to both phases, which allows us to exploit modern highly parallel computing architectures to achieve significant speedups in verifying IMDPs. To address the second issue, we introduce a novel finite-state model called factored Interval Markov Decision Processes (fIMDPs) that exploits structural properties of the system dynamics to significantly reduce memory requirements while maintaining formal guarantees. Factored models encode data-dependencies more fine-grained than flat models, which is the key driver for the reduction in memory. Moreover, factored models have been successfully used in the context of abstraction to Markov Decision Processes (MDPs), but have not been applied until now to IMDPs. An insight of abstracting to factored models is that the structural exploitation inadvertently tightens the ambiguity sets that characterize IMDPs conservatism, thereby reducing the pessimism of the bounds.

The methods developed in this dissertation represent significant algorithmic and theoretical advances to address the scalability-conservatism trade-off and enable more efficient computation of tighter safety probability bounds, advancing formal verification of stochastic dynamical systems. By advancing stochastic barrier function synthesis and IMDP-based finite-state abstractions, this work pushes the frontier of formal verification for stochastic systems, providing new tools and insights to bridge the gap between theory and practice.  The findings suggest that future progress in scalable safety verification for stochastic systems depends critically on designing algorithms that respect and exploit inherent problem structure, offering a promising, albeit challenging path toward making formal methods practical for real-world stochastic cyber-physical systems.