Computation of complete abstractions of quantised systems

Discrete abstractions are discrete-event models that describe a quantised continuous-variable system with direct reference to the quantised inputs and outputs. If these models should be used in diagnostic or verification tasks, they have to be complete. The paper concerns discrete abstractions that have the form of stochastic automata. It describes a method for determining the behavioural relation of the stochastic automaton so that the automaton is a complete model of a given quantised system. First, it is shown that well-known cell-to-cell mapping algorithms cannot ensure that the resulting model is complete. A new method based on the mapping of hyperboxes is introduced that yields a complete model.