Henzinger, Thomas A.; Ho, Pei-Hsin; Wong-Toi, Howard HyTech: A model checker for hybrid systems. (English) Zbl 1060.68603 Int. J. Softw. Tools Technol. Transf. 1, No. 1-2, 110-122 (1997). Summary: 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. Cited in 97 Documents MSC: 68Q45 Formal languages and automata 68Q60 Specification and verification (program logics, model checking, etc.) 93A30 Mathematical modelling of systems (MSC2010) Keywords:hybrid systems; symbolic model checking; hybrid automata; HyTech Software:HyTech PDFBibTeX XML Full Text: DOI