×

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.

MSC:

68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
93A30 Mathematical modelling of systems (MSC2010)

Software:

HyTech
Full Text: DOI