Checking Bounded Reachability of Compositional Linear Hybrid Automata Using Interaction Relations

For compositional linear hybrid automata (CLHA), whose dynamics can be characterized by linear constraints, bounded model checking (BMC) is challenging due to the complexity caused by interactions among member automata. Classical BMC approaches encode CLHA behavior using interleaving semantics, where compositions are handled with Cartesian product; as a result, the encoding is often large and complex, significantly limiting the scalability and efficiency of BMC. To address this problem, we propose three interaction relations to categorize and describe CLHA interactions through shared-label synchronization, discrete-variable read-write, and time-duration read-write. Based on the interaction relations, we devise interaction-oriented synchronization (IOS) semantics for CLHA behavior, which provides for a concise BMC encoding. In BMC, we employ a path-oriented method to check bounded reachability of CLHA, by enumerating candidate paths and checking each path’s feasibility. To prune the search space of candidate paths, we introduce a temporal relation graph (TRG) to quickly rule out infeasible paths via graph-based checking. Our method is implemented into a CLHA bounded reachability checker, BACH . Experiments indicate that it enables significant efficiency improvement over state-of-the-art tools, and performs scalable bounded reachability analysis on practical CLHA cases within seconds.