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.