تقرير
Formal Abstraction of General Stochastic Systems via Noise Partitioning
| العنوان: | Formal Abstraction of General Stochastic Systems via Noise Partitioning |
|---|---|
| المؤلفون: | Skovbekk, John, Laurenti, Luca, Frew, Eric, Lahijanian, Morteza |
| سنة النشر: | 2023 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Electrical Engineering and Systems Science - Systems and Control |
| الوصف: | 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. Comment: 6 pages, 6 figures, submitted jointly to IEEE Control Systems Letters and 2024 ACC |
| نوع الوثيقة: | Working Paper |
| URL الوصول: | http://arxiv.org/abs/2309.10702 |
| رقم الأكسشن: | edsarx.2309.10702 |
| قاعدة البيانات: | arXiv |
| الوصف غير متاح. |