hide
Free keywords:
-
Abstract:
This paper provides a suite of optimization techniques 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 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
optimization techniques shown yield consistently a speedup
of about 20 against previously published results for a
similar benchmark suite, and complement these with new
results on counterexample guided abstraction refinement. In
combination with the methods guaranteeing preciseness of
abstractions, this allows to significantly extend the class
of models for which safety can be established, covering in
particular models with 23 continuous variables and 2 to the
71 discrete states, 20 continuous variables and 2 to the
199 discrete states, and 9 continuous variables and 2 to
the 271 discrete states.
