@article{4493,
  abstract     = {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.},
  author       = {Henzinger, Thomas A and Ho, Pei and Wong Toi, Howard},
  issn         = {1433-2779},
  journal      = {Software Tools For Technology Transfer},
  number       = {1-2},
  pages        = {110 -- 122},
  publisher    = {Springer},
  title        = {{HyTech: A model checker for hybrid systems}},
  doi          = {10.1007/s100090050008},
  volume       = {1},
  year         = {1997},
}