Model-checking is a search technique that explores the state space of a modelled system looking for states that match specific criteria. Model-checkers generally rely on Boolean values, enumerations and small integer ranges to make the state space search tractable. Where possible, abstraction techniques are used in the process of building the model to further reduce the state space. For example, a property of an open-loop controller may depend on the relationship between the continuously-varying input and a static threshold. The input and the threshold need not be modelled individually in this case, a simple Boolean value will be enough to indicate whether the threshold is exceeded. The model-checker will then check both scenarios without having to consider all of the different possible values of the input variable.

For a realistic system, this type of abstraction is difficult to use. There may be feedback, dynamic thresholds or multiple thresholds to consider, for example. As an alternative to this type of abstraction, an interval analysis approach is proposed. The approach divides each continuously-varying input into a number of fixed-size intervals between a fixed minimum and a fixed maximum. Case-study results show that the technique is useful in practice, but would benefit from automated tool support.