A Cegar-centric Bounded Reachability Analysis for Compositional Affine Hybrid Systems

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.