Scaling Up Reachability Analysis for Rectangular Automata with Random Clocks

TL;DR

This paper enhances the scalability of reachability analysis for stochastic hybrid automata by optimizing key components and demonstrating that backward reachability is optional for certain probability computations.

Contribution

It introduces specific optimizations for reachability analysis of stochastic hybrid automata and shows that backward reachability can be omitted in some cases.

Findings

Optimizations significantly improve analysis scalability.

Backward reachability is optional for maximal probability computation.

The method applies to a subclass of hybrid automata with stochastic elements.

Abstract

This paper presents optimizations to improve the scalability of reachability analysis on a subclass of hybrid automata extended with stochasticity. The optimizations target different components of the analysis, such as quantifier elimination for state set projection, and automated parameter selection during the numerical integration. Most importantly, whereas the original method combines forward and backward reachability, we show that the usage of backward reachability is optional for computing maximal reachability probabilities.