Discrete-time hybrid modeling and verification of the batch evaporator process benchmark

For hybrid systems described by interconnections of linear discrete-time dy namical systems, automata, and propositional logic rules, we recently propo sed the Mixed Logical Dynamical (MLD) systems formalism and the language HY SDEL (Hybrid System Description Language) as a modeling tool. For MLD model s, we developed a reachability analysis algorithm which combines forward re ach set computation and feasibility analysis of trajectories by linear and mixed-integer linear programming. In this paper the versatility of the over all analysis tool is illustrated on the batch evaporator benchmark process.