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

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 linear constraints and boolean variables using LinAIGs. Several interpolation methods allow us to compute abstractions consisting of fewer linear constraints, and hence reduce the complexity of the reachable state set computation. In combination with methods that guarantee the preciseness of abstractions, this leads to a significant reduction of the runtimes of the verification process compared with exact verification.