Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Scaling Up Reachability Analysis for Rectangular Automata with Random Clocks

Jonas Stübbe, Anne Remke, Erika Ábrahám

TL;DR

This work tackles the scalability of time-bounded reachability analysis for rectangular automata with random clocks by introducing optimizations across state-set representations, Fourier-Motzkin quantifier elimination with redundancy checks, and adaptive integration bounds. It demonstrates that maximal reachability probabilities can be obtained using forward reachability alone when schedulers are not of interest, while still enabling scheduler analysis when needed. Empirical results on CAR and EBIKE show that forward analysis yields significant speedups, FM+ mitigates constraint explosion, and tightened integration bounds drastically reduce integration volume and improve efficiency. The combined approach enhances the practicality of automated worst-case analysis for stochastic hybrid systems and lays groundwork for further efficiency improvements.

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.

Scaling Up Reachability Analysis for Rectangular Automata with Random Clocks

TL;DR

This work tackles the scalability of time-bounded reachability analysis for rectangular automata with random clocks by introducing optimizations across state-set representations, Fourier-Motzkin quantifier elimination with redundancy checks, and adaptive integration bounds. It demonstrates that maximal reachability probabilities can be obtained using forward reachability alone when schedulers are not of interest, while still enabling scheduler analysis when needed. Empirical results on CAR and EBIKE show that forward analysis yields significant speedups, FM+ mitigates constraint explosion, and tightened integration bounds drastically reduce integration volume and improve efficiency. The combined approach enhances the practicality of automated worst-case analysis for stochastic hybrid systems and lays groundwork for further efficiency improvements.

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.

Paper Structure

This paper contains 22 sections, 1 theorem, 8 equations, 6 figures, 4 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related work.
  3. Outline.
  4. Theoretical Background
  5. State-Set Representations and Conversion Methods
  6. Model Definition
  7. Maximal Schedulers
  8. Reachability Analysis
  9. Optimizations
  10. Description of E-Bike case study
  11. Parameter settings
  12. Fourier-Motzkin Quantifier Elimination
  13. Checking for redundant constraints
  14. Results
  15. Optionality of Backward Refinement
  16. ...and 7 more sections

Key Result

Lemma 1

Let $\mathcal{C}_{u}\xspace$ with set of states $\mathcal{S}_{\mathcal{C}_{u}\xspace}\xspace$ be an unrolled RAC with ${d_{{\hbox{$R$}}}^{u}}\xspace$ random clocks. Assume ${\mathcal{S}_\textsl{goal}}\xspace \subseteq \mathcal{S}_{\mathcal{C}_{u}\xspace}\xspace$, $T_{\textsl{max}}\xspace \in \mathbb

Figures (6)

  • Figure 1: Operational semantics for RAC $\mathcal{C}\xspace= (\mathcal{R}\xspace\xspace,\mathit{Lab}\xspace,\mathit{Distr}\xspace,\mathit{Event}\xspace)$ with $\mathcal{R}\xspace\xspace=(\mathit{Loc}\xspace, \mathit{Var}\xspace, \mathit{Inv}\xspace, \mathit{Init}\xspace,\mathit{Flow}\xspace\xspace,\mathit{Jump}\xspace)$.
  • Figure 2: RAC $\mathcal{C}\xspace$ for a simplified version of the CAR case study presented in delicaris2024Journaldelicaris2023maximizing and the structure of the corresponding reach tree $\mathtt{R}$ for one cycle and goal state set ${\mathcal{S}_\textsl{goal}}\xspace = \{(\text{empty}, \nu\xspace, \mu\xspace, s\xspace) \in \mathcal{S}_{\mathcal{C}\xspace}\xspace\}$, omitting parts that do not reach the goal.
  • Figure 3: EBIKE model with cycles modeled as RAC.
  • Figure 4: Computation times for reachability analysis for 1 cycle per method for E-Bike and Car case study.
  • Figure 5: EBIKE model with cycles modeled as RAC.
  • ...and 1 more figures

Theorems & Definitions (14)

  • Definition 1: H- and V-polyhedra ziegler2012lectures
  • Definition 2: RA syntax
  • Definition 3: RAC syntax
  • Definition 4: Run of $\mathcal{C}\xspace$ delicaris2024Journal
  • Definition 5: Scheduler delicaris2024Journal
  • Definition 6: Run induced by scheduler $\mathfrak{s}\xspace_{\kappa\xspace}$ for RAC $\mathcal{C}\xspace$ delicaris2024Journal
  • Definition 7: Prophetic maximum reachability probability delicaris2024Journal
  • Definition 8: Reach tree delicaris2024Journal
  • Example 1
  • Definition 9
  • ...and 4 more