Compositional verification of hybrid systems with discrete interaction using simulation relations

Simulation relations can be used to verify refinement between a system and its specification, or between models of different complexity. It is known that for the verification of safety properties, simulation between hybrid systems can be defined based on their labeled transition system semantics. We show that for hybrid systems without shared variables, which therefore only interact at discrete events, this simulation preorder is compositional, and present assume-guarantee rules that help to counter the state explosion problem. Some experimental results for simulation checking of linear hybrid automata are provided using a prototype tool with exact arithmetic and unlimited digits