Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Relational Abstractions for Continuous and Hybrid Systems
verfasst von : Sriram Sankaranarayanan, Ashish Tiwari
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.