Formal Abstraction of General Stochastic Systems via Noise Partitioning

TL;DR

This paper presents a novel noise partitioning method for finite abstraction of complex stochastic systems, enabling verification with guarantees even for non-standard noise distributions.

Contribution

It introduces a general noise partitioning approach for constructing interval Markov chain abstractions applicable to diverse noise models, including data-driven systems.

Findings

Effective abstraction of nonlinear stochastic systems demonstrated

Verification guarantees provided for complex noise distributions

Method applicable to data-driven and non-Gaussian noise cases

Abstract

Verifying the performance of safety-critical, stochastic systems with complex noise distributions is difficult. We introduce a general procedure for the finite abstraction of nonlinear stochastic systems with non-standard (e.g., non-affine, non-symmetric, non-unimodal) noise distributions for verification purposes. The method uses a finite partitioning of the noise domain to construct an interval Markov chain (IMC) abstraction of the system via transition probability intervals. Noise partitioning allows for a general class of distributions and structures, including multiplicative and mixture models, and admits both known and data-driven systems. The partitions required for optimal transition bounds are specified for systems that are monotonic with respect to the noise, and explicit partitions are provided for affine and multiplicative structures. By the soundness of the abstraction procedure, verification on the IMC provides guarantees on the stochastic system against a temporal logic specification. In addition, we present a novel refinement-free algorithm that improves the verification results. Case studies on linear and nonlinear systems with non-Gaussian noise, including a data-driven example, demonstrate the generality and effectiveness of the method without introducing excessive conservatism.