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

We develop an algorithm for computing bounded reachability probability forhybrid systems, i.e., the probability that the system reaches an unsafe regionwithin a finite number of discrete transitions. In particular, we focus onhybrid systems with continuous dynamics given by solutions of nonlinearordinary differential equations (with possibly nondeterministic initialconditions and parameters), and probabilistic behaviour given by initialparameters distributed as continuous (with possibly infinite support) anddiscrete random variables. Our approach is to define an appropriate relaxationof the (undecidable) reachability problem, so that it can be solved by$\delta$-complete decision procedures. In particular, for systems withcontinuous random parameters only, we develop a validated integration procedurewhich computes an arbitrarily small interval that is guaranteed to contain thereachability probability. In the more general case of systems with bothnondeterministic and probabilistic parameters, our procedure computes aguaranteed enclosure for the range of reachability probabilities. We haveapplied our approach to a number of nonlinear hybrid models and validated theresults by comparison with Monte Carlo simulation.

Probabilistic bounded reachability for hybrid systems with continuous nondeterministic and probabilistic parameters