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

被引：20

作者：

Bemporad, A

Torrisi, FD

Morari, M

机构：

[1] Univ Siena, Dipartimento Ingn Informaz, I-53100 Siena, Italy

[2] ETH Zentrum, ETL, Automat Control Lab, CH-8092 Zurich, Switzerland

来源：

EUROPEAN JOURNAL OF CONTROL | 2001年 / 7卷 / 04期

关键词：

discrete-time; hybrid systems; reachability analysis; verification;

D O I：

10.3166/ejc.7.382-399

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

For hybrid systems described by interconnections of linear discrete-time dynamical systems, automata, and propositional logic rules, we recently proposed the Mixed Logical Dynamical (MLD) systems formalism and the language HYSDEL (Hybrid System Description Language) as a modeling tool. For MLD models, we developed a reachability analysis algorithm which combines forward reach set computation and feasibility analysis of trajectories by linear and mixed-integer linear programming. In this paper the versatility of the overall analysis tool is illustrated on the batch evaporator benchmark process.

引用

页码：382 / 399

页数：18