HYTECH: A Model Checker for Hybrid Systems

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 di erential equations for capturing continuous change. HyTech is a symbolic model checker for linear hybrid automata, a subclass of hybrid automatathat can be analyzed automaticallyby 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 satis es a temporal-logic requirement.

• Type: Conference
• Year: 1997
• Where: CAV
• Authors: Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi
• Keywords: CAV 1997, Hardware, Hybrid Automaton, Linear Hybrid, Linear Hybrid Automaton