Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
721102 | IFAC Proceedings Volumes | 2009 | 6 Pages |
Abstract
In this paper we make a step towards an algorithm for the verification of hybrid systems that, on the one hand allows very general inputs (e.g., with non-linear ordinary differential equations), but on the other hand exploits the structure of those parts of the input that represent special cases (e.g., clocks). We show how to compute slices of parallel hyperplanes separating reachable from unreachable parts of the state space for a given abstraction of the input system, and demonstrate the usefulness of such slices within an abstraction refinement algorithm based on hyper-rectangles.
Related Topics
Physical Sciences and Engineering
Engineering
Computational Mechanics
Authors
Tomas Dzetkulic, Stefan Ratschan,