Using Redundant Constraints for Refinement

Abstract. This paper is concerned with a method for computing reachable sets of linear continuous systems with uncertain input. Such a method is required for verification of hybrid systems and more generally embedded systems with mixed continuous-discrete dynamics. In general, the reachable sets of such systems (except for some linear systems with special eigenstructures) are hard to compute exactly and are thus often over-approximated. The approximation accuracy is important especially when the computed over-approximations do not allow proving a property. In this paper we address the problem of refining the reachable set approximation by adding redundant constraints which allow bounding the reachable sets in some critical directions. We introduce the notion of directional distance which is appropriate for measuring approximation effectiveness with respect to verifying a safety property. We also describe an implementation of the reachability algorithm which favors the constraint-based ...

• Type: Conference
• Year: 2010
• Where: ATVA
• Authors: Eugene Asarin, Thao Dang, Oded Maler, Romain Testylier
• Keywords: ATVA 2010, Hardware, Reachable Set Approximation, Reachable Sets, Systems