Abstraction-based Probabilistic Stability Analysis of Polyhedral Probabilistic Hybrid Systems
This work addresses stability analysis for a subclass of stochastic hybrid systems, which is incremental as it builds on existing abstraction methods for specific system types.
The paper tackles the problem of probabilistic stability analysis for Polyhedral Probabilistic Hybrid Systems by developing an abstraction-based framework that constructs a finite Markov Decision Process, with a polynomial-time verification algorithm, and demonstrates feasibility through experiments on systems of various dimensions and sizes.
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.