Article ID Journal Published Year Pages File Type
721102 IFAC Proceedings Volumes 2009 6 Pages PDF
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
, ,