基于多面体包含的非线性混成系统可达性分析

doi:10.3724/SP.J.1087.2013.01289

摘要
图/表
参考文献
相关文章 (2)

全文: PDF (732 KB) HTML (1 KB)
输出: BibTeX | EndNote (RIS)

摘要针对一类非线性混成系统的可达性问题，提出了一种基于多面体包含的分析方法。首先介绍了混成系统及其可达性，讨论了如何应用多面体包含对多项式混成系统进行线性近似，并采用量词消去和非线性优化方法来构造相应的线性混成系统，然后运用验证工具SpaceEx求得原非线性混成系统的过近似可达集，并应用于验证系统的安全性。

	服务

	把本文推荐给朋友
	加入我的书架
	加入引用管理器
	E-mail Alert
	RSS
	作者相关文章
	邹进
	林望
	罗勇
	曾振柄

关键词 ：混成系统, 可达性分析, 安全性验证, 多面体包含, 线性近似

Abstract：To study the reachability of a class of nonlinear hybrid systems, this paper presented an verification method based on polyhedron inclusion. Firstly, some notions about hybrid systems and reachability were introduced. The method based on polyhedron inclusion was proposed to compute the linear approximation of polynomial hybrid systems. Quantifier elimination and nonlinear optimization method were applied to obtain the associated linear hybrid systems. Then the over-approximation of reachable set of original polynomial hybrid systems can be computed by using SpaceEx. Furthermore, the safety properties of the systems also can be verified.

Key words： hybrid system reachability analysis safety verification polyhedron inclusion linear approximation

收稿日期: 2012-11-19 出版日期: 2013-05-08

基金资助:

国家自然科学基金资助项目(11001204);国家973计划项目(2011CB302904);浙江省教育厅科研项目(Y201120383);温州大学实验室研究项目(JWS20120612)

通讯作者: 林望 E-mail: linwang@wzu.edu.cn

作者简介: 邹进(1990-)，男，江西抚州人，硕士研究生，主要研究方向：微分方程、计算机数学；林望(1982-)，男，浙江温州人，博士研究〖CM(61〗生，主要研究方向：程序验证、混成系统分析与验证；罗勇(1978-)，男，安徽合肥人，副教授，主要研究方向：符号计算、微分方程定性理论；〖CM)〗曾振柄(1963-)，男，甘肃皋兰人，教授，博士生导师，主要研究方向：数学机械化、定理机器证明、自动推理。

引用本文:

邹进林望罗勇曾振柄. 基于多面体包含的非线性混成系统可达性分析[J]. 计算机应用, 2013, 33(05): 1289-1293. ZOU Jin LIN Wang LUO Yong ZENG Zhenbing. Reachability analysis of nonlinear hybrid systems based on polyhedron inclusion. Journal of Computer Applications, 2013, 33(05): 1289-1293.

链接本文:

http://www.joca.cn/CN/10.3724/SP.J.1087.2013.01289 或 http://www.joca.cn/CN/Y2013/V33/I05/1289