*
Thomas A. Henzinger,
Pei-Hsin Ho, and Howard Wong-Toi*

Hybrid systems are digital real-time systems that are embedded in analog
environments. Model-checking tools are available for the automatic analysis
of *linear hybrid automata*, whose environment variables are subject to
piecewise-constant polyhedral differential inclusions. In most embedded
systems, however, the environment variables have differential inclusions that
vary with the values of the variables. Such inclusions are prohibited in the
linear hybrid automaton model. We present two methods for translating
nonlinear hybrid systems into linear hybrid automata. Properties of the
nonlinear systems can then be inferred from the automatic analysis of the
translated linear hybrid automata.

The first method, called *clock translation*, replaces constraints on
nonlinear variables by constraints on clock variables. The clock translation
is efficient but has limited applicability. The second method, called
*linear phase-portrait approximation*, conservatively overapproximates
the phase portrait of a hybrid automaton using piecewise-constant polyhedral
differential inclusions. Both methods are sound for safety properties; that
is, if we establish a safety property of the translated linear system, we may
conclude that the original nonlinear system satisfies the property. When
applicable, the clock translation is also complete for safety properties;
that is, the original system and the translated system satisfy the same
safety properties. The phase-portrait approximation method is not complete
for safety properties, but it is asymptotically complete; intuitively, for
every safety property, and for every relaxed nonlinear system arbitrarily
close to the original, if the relaxed system satisfies the safety property,
then there is a linear phase-portrait approximation that also satisfies the
property.

We illustrate both methods by using HyTech--a symbolic model checker for linear hybrid automata--to automatically check properties of a nonlinear temperature controller and of a predator-prey ecology.

*IEEE Transactions on Automatic Control* 43:540-554, 1998.
Preliminary reports on this work appeared in the
T.A. Henzinger and P.-H. Ho,
"Algorithmic analysis of nonlinear hybrid systems,"
*Proceedings of the
Seventh International Conference on Computer-Aided Verification*
(CAV),
Lecture Notes in Computer Science 939,
Springer, 1995, pp. 225-238, and in
T.A. Henzinger and H. Wong-Toi,
"Linear phase-portrait approximations for nonlinear hybrid systems,"
in
*Hybrid Systems III*,
Lecture Notes in Computer Science 1066,
Springer, 1996, pp. 377-388.

Download inofficial, sometimes updated PostScript / PDF document. © 1995, 1996 Springer, 1998 IEEE.