Lecture Notes in Computer Science, 2006, Volume 4120/2006, 196-210, DOI: 10.1007/11856290_18

Constraints for Continuous Reachability in the Verification of Hybrid Systems

Stefan Ratschan and Zhikun She

View Related Documents

Abstract

The method for verification of hybrid systems by constraint propagation based abstraction refinement that we introduced in an earlier paper is based on an over-approximation of continuous reachability information of ordinary differential equations using constraints that do not contain differentiation symbols. The method uses an interval constraint propagation based solver to solve these constraints. This has the advantage that—without complicated algorithmic changes—the method can be improved by just changing these constraints. In this paper, we discuss various possibilities of such changes, we prove some properties about the amount of over-approximations introduced by the new constraints, and provide some timings that document the resulting improvement.
This work was partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS). See www.avacs.org for more information.

Fulltext Preview

Image of the first page of the fulltext document