Optimizing Reachability Probabilities for a Restricted Class of Stochastic Hybrid Automata Via Flowpipe-Construction

Stochastic Hybrid automata (SHA) are increasingly used to evaluate the dependability and safety of critical infrastructures. Nondeterminism, which is present in many purely hybrid models, is often only implicitly considered in SHA. This paper instead proposes algorithms for computing optimal reachability probabilities for singular automata with urgent transitions and random clocks which follow arbitrary continuous probability distributions. We borrow a well-known approach from hybrid systems reachability analysis, namely flowpipe construction. We extract those valuations of random clocks which ensure reachability of specific goal states from the computed flowpipes and compute reachability probabilities by integrating over these valuations. We compute maximal and minimal probabilities for history-dependent prophetic and non-prophetic schedulers using set-based methods. A case study featuring a series of nondeterministic choices shows the feasibility of the approach.

International Conference on Quantitative Evaluation of Systems