“Quantitative Verification for Massive Linear Systems”

The verification of linear systems, particularly within the scope of reachability analysis and safety verification, has been an active area of research for decades. Most verification methods primarily focus on qualitative verification, which answers whether or not a system may violate specified safety conditions. This paper extends this qualitative verification to quantitative verification by introducing a novel approach, employing probabilistic stars (Probstars), which augment traditional star sets by integrating Gaussian-distributed random variables with predicates. This quantitative verification enables a probabilistic understanding of reachability in high-dimensional systems, providing the probability of violation for discrete-time, linear time-invariant (LTI) systems. The set of reachable states at the discrete-time step can be written in matrix exponential, which arises from the solution to the ordinary differential equation (ODE): x’(t) = A x(t) + B u(t) starting from the given initial state. However, computing the matrix exponential is intractable for large-scale systems due to excessive memory demands and computational burdens. To tackle these challenges, our method utilizes low-dimensional projections of system variables, such as projecting the full state space onto initial and output spaces, to improve memory efficiency. Additionally, we implement efficient numerical simulations with iterative techniques to approximate solutions to linear systems. These simulations take advantage of the sparsity in high-dimensional system dynamics by employing Krylov subspace methods, such as Arnoldi and Lanczos iterations, to improve computational efficiency.

Committee members:
Dr. Dung Hoang Tran, Chair
Dr. Hamid Bagheri
Dr. Bhuvana Gopal