Relational Abstractions for Continuous and Hybrid Systems
CAV 2011: International Conference on Computer Aided Verification


In this paper, we define relational abstractions of hybrid systems. A relational abstraction is obtained by replacing the continuous dynamics in each mode by a binary transition relation that relates a state of the system to any state that can potentially be reached at some future time instant using the continuous dynamics. We construct relational abstractions by reusing template-based invariant generation techniques for continuous systems described by Ordinary Differential Equations (ODE). As a result, we abstract a given hybrid system as a purely discrete, infinite-state system. We apply k-induction to this abstraction to prove safety properties, and use bounded model-checking to find potential falsifications. We present the basic underpinnings of our approach and demonstrate its use on many benchmark systems to derive simple and usable abstractions.


@string{CAV = "International Conference on Computer Aided Verification (CAV)"}
  author = {Sriram SankaranarayananAshish Tiwari},
  title = {Relational Abstractions for Continuous and Hybrid Systems},
  booktitle = CAV,
  year = {2011},