基于混合逻辑动态模型的预测控制与形式验证技术

摘要

在现代流程工业中,过程控制对象日益复杂以及对控制精度的要求日益提高,工业过程控制中连续过程动态和离散事件动态的混杂特性越来越明显,传统的理论方法对这些系统进行建模和控制,已很难满足控制要求。针对这种情况,本文采用混合逻辑动态(Mixed Logical Dynamical,MLD)模型理论,进行混杂系统的建模、控制与形式验证研究。
　　 本文在前人研究工作的基础上,对混杂系统理论作了进一步的研究和探索。研究的内容包括基于MLD的混杂系统控制和形式验证研究两个部分,主要体现在以下几个方面:
　　 深入研究了混合逻辑动态系统建模机理,讨论了逻辑命题的转换及其线性整数规划的方法,分别以机理建模和Hysdel方法建立了CSTR系统的MLD模型,总结了混杂系统不同模型之间的等价性。
　　 将传统的模型预测控制应用到基于MLD模型的混杂系统中,研究了混合逻辑动态系统的开环约束最优控制,分别探讨了基于MIQP和MILP问题的模型预测控制,通过数值仿真验证了两种算法的有效性。
　　 探讨了定理证明和模型检验两种混杂系统形式验证方法,详细介绍了基于模型检验的形式验证工具,利用CheckMate验证工具对弹跳球系统进行了形式验证的仿真研究。
　　 研究了混合逻辑动态系统的形式验证问题,针对混合逻辑动态系统,在理论上深入研究了基于数学规划的混杂系统形式验证算法,将该算法应用到非线性CSTR系统中,探讨了CSTR系统的安全性问题,对混杂系统控制的正确性和可靠性进行了有益的探索。
　　 最后,对全文工作进行了总结,对混杂系统控制及形式验证技术未来的发展方向做了展望。

目录

文摘

英文文摘

第1章 绪论

1.1 课题的来源及意义

1.2 混杂系统国内外研究现状

1.2.1 混杂系统建模

1.2.2 混杂系统控制

1.2.3 混杂系统应用

1.2.4 混杂系统形式验证

1.3 本文主要内容及结构安排

第2章 混杂系统混合逻辑动态建模

2.1 混合逻辑动态(MLD)模型

2.1.1 命题演算与线性整数规划

2.1.2 Hysdel语言建模

2.2 基于MLD的CSTR建模研究

2.2.1 CSTR工艺过程及数学分析

2.2.2 CSTR模型线性化

2.2.3 CSTR系统MLD建模

2.3 模型等价

2.4 本章小结

第3章 基于混合逻辑动态模型的预测控制研究

3.1 模型预测控制(Model Predictive Control,MPC)

3.1.1 模型预测控制的发展

3.1.2 预测控制的基本原理

3.2 基于MLD的混杂系统优化控制

3.2.1 混合MLD的稳定性分析

3.2.2 混合逻辑动态系统的开环约束最优控制

3.3 基于MLD的模型预测控制

3.3.1 基于MIQP的MLD系统的模型预测控制

3.3.2 基于MILP的MID系统的模型预测控制

3.4 本章小结

第4章 混杂系统形式化验证研究

4.1 混杂系统形式验证基本原理

4.1.1 混杂系统形式化验证

4.1.2 混杂系统形式验证方法

4.2 混杂系统验证工具

4.3 形式验证仿真研究

4.3.1 弹跳球系统描述

4.3.2 弹跳球的CheckMate模型

4.3.3 仿真结果分析

4.4 本章小结

第5章 基于MLD的CSTR混杂形式验证技术

5.1 混合逻辑动态系统形式验证问题

5.2 MLD系统形式验证的一般步骤

5.3 基于数学规划的MID系统形式验证

5.3.1 基于MLD的形式验证算法研究

5.3.2 算法的复杂性

5.4 基于MID的CSTR形式验证

5.4.1 简单系统验证实例

5.4.2 基于MLD的CSTR形式验证

5.5 本章小结

总结与展望

参考文献

附录

附录A 基于HYSDEL语言的CSTR系统MLD模型

附录B MLD预测控制问题转化为MIQP问题

攻读硕士期间学术成果

致谢