English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Verifying the performance of safety-critical, stochastic systems with complexnoise distributions is difficult. We introduce a general procedure for thefinite abstraction of nonlinear stochastic systems with non-standard (e.g.,non-affine, non-symmetric, non-unimodal) noise distributions for verificationpurposes. The method uses a finite partitioning of the noise domain toconstruct an interval Markov chain (IMC) abstraction of the system viatransition probability intervals. Noise partitioning allows for a general classof distributions and structures, including multiplicative and mixture models,and admits both known and data-driven systems. The partitions required foroptimal transition bounds are specified for systems that are monotonic withrespect to the noise, and explicit partitions are provided for affine andmultiplicative structures. By the soundness of the abstraction procedure,verification on the IMC provides guarantees on the stochastic system against atemporal logic specification. In addition, we present a novel refinement-freealgorithm that improves the verification results. Case studies on linear andnonlinear systems with non-Gaussian noise, including a data-driven example,demonstrate the generality and effectiveness of the method without introducingexcessive conservatism.

Formal Abstraction of General Stochastic Systems via Noise Partitioning