## HyTech: A Model Checker for Hybrid Systems

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

A *hybrid system* is a dynamical system whose behavior exhibits both
discrete and continuous change. A *hybrid automaton* is a mathematical
model for hybrid systems, which combines, in a single formalism, automaton
transitions for capturing discrete change with differential equations for
capturing continuous change. HyTech is a symbolic model checker for
*linear hybrid automata*, a subclass of hybrid automata that can be
analyzed automatically by computing with polyhedral state sets. A key
feature of HyTech is its ability to perform parametric analysis, *i.e.*
to determine the values of design parameters for which a linear hybrid
automaton satisfies a temporal-logic requirement.

*Software Tools for Technology Transfer* 1:110-122, 1997.
A preliminary version appeared in the
*Proceedings of the
Ninth International Conference on Computer-Aided Verification*
(CAV),
Lecture Notes in Computer Science 1254,
Springer, 1997, pp. 460-463.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1997 Springer.