Click here to flash read.
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.
No creative common's license