Reference
Abstract
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.
BibTeX
@string{CAV = "International Conference on Computer Aided Verification (CAV)"}
@inproceedings{relationalization-cav11,
author = {Sriram SankaranarayananAshish Tiwari},
title = {Relational Abstractions for Continuous and Hybrid Systems},
booktitle = CAV,
year = {2011},
}