Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2509.03560 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914020045357056 |
|---|---|
| author | Kundu, Atanu Sarkar, Pratyay Ray, Rajarshi |
| author_facet | Kundu, Atanu Sarkar, Pratyay Ray, Rajarshi |
| contents | Reachability analysis of compositional hybrid systems, where individual components are modeled as hybrid automata, poses unique challenges. In addition to preserving the compositional semantics while computing system behaviors, algorithms have to cater to the explosion in the number of locations in the parallel product automaton. In this paper, we propose a bounded reachability analysis algorithm for compositional hybrid systems with piecewise affine dynamics, based on the principle of counterexample guided abstraction refinement (CEGAR). In particular, the algorithm searches for a counterexample in the discrete abstraction of the composition model, without explicitly computing a product automaton. When a counterexample is discovered in the abstraction, its validity is verified by a refinement of the state-space guided by the abstract counterexample. The state-space refinement is through a symbolic reachability analysis, particularly using a state-of-the-art algorithm with support functions as the continuous state representation. In addition, the algorithm mixes different semantics of composition with the objective of improved efficiency. Step compositional semantics is followed while exploring the abstract (discrete) state-space, while shallow compositional semantics is followed during state-space refinement with symbolic reachability analysis. Optimizations such as caching the results of the symbolic reachability analysis, which can be later reused, have been proposed. We implement this algorithm in the tool SAT-Reach and demonstrate the scalability benefits. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_03560 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Cegar-centric Bounded Reachability Analysis for Compositional Affine Hybrid Systems Kundu, Atanu Sarkar, Pratyay Ray, Rajarshi Logic in Computer Science Reachability analysis of compositional hybrid systems, where individual components are modeled as hybrid automata, poses unique challenges. In addition to preserving the compositional semantics while computing system behaviors, algorithms have to cater to the explosion in the number of locations in the parallel product automaton. In this paper, we propose a bounded reachability analysis algorithm for compositional hybrid systems with piecewise affine dynamics, based on the principle of counterexample guided abstraction refinement (CEGAR). In particular, the algorithm searches for a counterexample in the discrete abstraction of the composition model, without explicitly computing a product automaton. When a counterexample is discovered in the abstraction, its validity is verified by a refinement of the state-space guided by the abstract counterexample. The state-space refinement is through a symbolic reachability analysis, particularly using a state-of-the-art algorithm with support functions as the continuous state representation. In addition, the algorithm mixes different semantics of composition with the objective of improved efficiency. Step compositional semantics is followed while exploring the abstract (discrete) state-space, while shallow compositional semantics is followed during state-space refinement with symbolic reachability analysis. Optimizations such as caching the results of the symbolic reachability analysis, which can be later reused, have been proposed. We implement this algorithm in the tool SAT-Reach and demonstrate the scalability benefits. |
| title | A Cegar-centric Bounded Reachability Analysis for Compositional Affine Hybrid Systems |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2509.03560 |