Verification of linear hybrid systems with large discrete state spaces using counterexample-guided abstraction refinement

Abstract We present a counterexample-guided abstraction refinement ( CEGAR) approach for the verification of safety properties of linear hybrid automata with large discrete state spaces, such as naturally arising when incorporating health state monitoring and degradation levels into the controller design. Such models can – in contrast to purely functional controller models – not be analyzed with hybrid verification engines relying on explicit representations of modes, but require fully symbolic representations for both the continuous and discrete part of the state space. The presented abstraction methods directly work on a symbolic representation of arbitrary non-convex combinations of line…