Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2508.19795 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908593243029504 |
|---|---|
| author | Stübbe, Jonas Remke, Anne Ábrahám, Erika |
| author_facet | Stübbe, Jonas Remke, Anne Ábrahám, Erika |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_19795 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Scaling Up Reachability Analysis for Rectangular Automata with Random Clocks Stübbe, Jonas Remke, Anne Ábrahám, Erika Symbolic Computation 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. |
| title | Scaling Up Reachability Analysis for Rectangular Automata with Random Clocks |
| topic | Symbolic Computation |
| url | https://arxiv.org/abs/2508.19795 |