Time-aware relational abstractions for hybrid systems

Hybrid Systems model both discrete switches and continuous dynamics and are suitable to represent embedded systems where discrete controllers interact with a physical plant. Relational abstraction is a new approach for verifying hybrid systems. In relational abstraction, the continuous dynamics in each location of the hybrid system is abstracted by a binary relation that relates the current value of the continuous variables with all future values of the variables that are reachable after a time elapse (continuous) transition. The abstract system is an infinite-state system, which can be verified using k-induction or abstract interpretation. Existing techniques for computing relational abstractions are time-agnostic: they do not construct any relationship between the state variables and the time elapsed during the continuous evolution. Time-agnostic abstractions cannot verify timing properties. We present a technique to compute a time-aware relational abstraction for verifying (timing-related) safety properties of cyber-physical systems. We show the effectiveness of the new abstraction on several case studies on which the previous techniques fail.