标题： 用于具有随机时钟的矩形自动机的可到达性分析扩展 显示英文标题

标题： Scaling Up Reachability Analysis for Rectangular Automata with Random Clocks

摘要： 本文提出了优化方法，以提高在扩展了随机性的混合自动机子类上的可达性分析的可扩展性。 这些优化针对分析的不同组件，例如状态集投影的量词消除，以及数值积分过程中的自动参数选择。 最重要的是，尽管原始方法结合了前向和后向可达性，我们表明在计算最大可达概率时，后向可达性的使用是可选的。 显示英文摘要

摘要： 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.