Formal Abstraction of General Stochastic Systems via Noise Partitioning

Formal Abstraction of General Stochastic Systems via Noise Partitioning

Skovbekk, John (University of Colorado)
Laurenti, L. (TU Delft Team Luca Laurenti)
Frew, Eric (University of Colorado)
Lahijanian, Morteza (University of Colorado)

2023

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 nonstandard (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.

Autonomous systems
Kernel
Markov processes
Nonlinear systems
Probabilistic logic
Standards
Stochastic systems
stochastic systems
Uncertainty

http://resolver.tudelft.nl/uuid:ee18af1f-40d2-4df0-91b5-185fa338fb4b

https://doi.org/10.1109/LCSYS.2023.3340621

2024-06-07

2475-1456

IEEE Control Systems Letters, 7, 3711-3716

Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public.

Institutional Repository

journal article

© 2023 John Skovbekk, L. Laurenti, Eric Frew, Morteza Lahijanian