In this paper, we consider the problem of probabilistic stability analysis of
a subclass of Stochastic Hybrid Systems, namely, Polyhedral Probabilistic
Hybrid Systems (PPHS), where the flow dynamics is given by a polyhedral
inclusion, the discrete switching between modes happens probabilistically at
the boundaries of their invariant regions and the continuous state is not reset
during switching. We present an abstraction-based analysis framework that
consists of constructing a finite Markov Decision Processes (MDP) such that
verification of certain property on the finite MDP ensures the satisfaction of
probabilistic stability on the PPHS. Further, we present a polynomial-time
algorithm for verifying the corresponding property on the MDP. Our experimental
analysis demonstrates the feasibility of the approach in successfully verifying
probabilistic stability on PPHS of various dimensions and sizes.

本研究提出了基于抽象的分析方法，结合有限马尔科夫决策过程和多项式时间算法，用以验证多面体概率混合系统的稳定性。

基于抽象的多面体概率混合系统稳定性分析

Abstraction-based Probabilistic Stability Analysis of Polyhedral  Probabilistic Hybrid Systems

StocHy is a software tool for the quantitative analysis of discrete-time
stochastic hybrid systems (SHS). StocHy accepts a high-level description of
stochastic models and constructs an equivalent SHS model. The tool allows to
(i) simulate the SHS evolution over a given time horizon; and to automatically
construct formal abstractions of the SHS. Abstractions are then employed for
(ii) formal verification or (iii) control (policy, strategy) synthesis. StocHy
allows for modular modelling, and has separate simulation, verification and
synthesis engines, which are implemented as independent libraries. This allows
for libraries to be easily used and for extensions to be easily built. The tool
is implemented in C++ and employs manipulations based on vector calculus, the
use of sparse matrices, the symbolic construction of probabilistic kernels, and
multi-threading. Experiments show StocHy's markedly improved performance when
compared to existing abstraction-based approaches: in particular, StocHy beats
state-of-the-art tools in terms of precision (abstraction error) and
computational effort, and finally attains scalability to large-sized models (12
continuous dimensions). StocHy is available at www.gitlab.com/natchi92/StocHy.

StocHy 是一个用于离散时间随机混合系统 (SHS) 的定量分析的软件工具，可以模拟 SHS 的演变并自动构建抽象，该抽象可用于形式验证或控制合成。

StocHy: 随机过程的自动验证和合成

StocHy: automated verification and synthesis of stochastic processes

We present ProbReach, a tool for verifying probabilistic reachability for
stochastic hybrid systems, i.e., computing the probability that the system
reaches an unsafe region of the state space. In particular, ProbReach will
compute an arbitrarily small interval which is guaranteed to contain the
required probability. Standard (non-probabilistic) reachability is undecidable
even for linear hybrid systems. In ProbReach we adopt the weaker notion of
delta-reachability, in which the unsafe region is overapproximated by a
user-defined parameter (delta). This choice leads to false alarms, but also
makes the reachability problem decidable for virtually any hybrid system. In
ProbReach we have implemented a probabilistic version of delta-reachability
that is suited for hybrid systems whose stochastic behaviour is given in terms
of random initial conditions. In this paper we introduce the capabilities of
ProbReach, give an overview of the parallel implementation, and present results
for several benchmarks involving highly non-linear hybrid systems.

ProbReach 是一种用于验证随机混合系统中概率可达性的工具。它采用了 delta - 可达性的弱化概念，并实现了一个适用于混合系统的概率版本，在多个基准测试中表现出令人满意的结果，并且有并行实现的概率。