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

doi:10.3724/SP.J.1087.2013.01289

计算机应用 ›› 2013, Vol. 33 ›› Issue (05): 1289-1293.DOI: 10.3724/SP.J.1087.2013.01289

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

邹进¹,林望¹,²,罗勇¹,曾振柄²

1. 温州大学数学与信息科学学院，浙江温州 325035
2. 华东师范大学上海市高可信计算重点实验室，上海 200062

收稿日期:2012-11-19 修回日期:2012-12-31 出版日期:2013-05-01 发布日期:2013-05-08
通讯作者: 林望
作者简介:邹进(1990-)，男，江西抚州人，硕士研究生，主要研究方向：微分方程、计算机数学；林望(1982-)，男，浙江温州人，博士研究〖CM(61〗生，主要研究方向：程序验证、混成系统分析与验证；罗勇(1978-)，男，安徽合肥人，副教授，主要研究方向：符号计算、微分方程定性理论；〖CM)〗曾振柄(1963-)，男，甘肃皋兰人，教授，博士生导师，主要研究方向：数学机械化、定理机器证明、自动推理。
基金资助:
国家自然科学基金资助项目(11001204);国家973计划项目(2011CB302904);浙江省教育厅科研项目(Y201120383);温州大学实验室研究项目(JWS20120612)

Reachability analysis of nonlinear hybrid systems based on polyhedron inclusion

ZOU Jin¹,LIN Wang¹,²,LUO Yong¹,ZENG Zhenbing²

1. College of Mathematics and Information Science, Wenzhou University, Wenzhou Zhejiang 325035, China
2. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China

Received:2012-11-19 Revised:2012-12-31 Online:2013-05-08 Published:2013-05-01
Contact: LIN Wang

摘要/Abstract

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

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

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

中图分类号:

TP311

邹进林望罗勇曾振柄. 基于多面体包含的非线性混成系统可达性分析[J]. 计算机应用, 2013, 33(05): 1289-1293.

ZOU Jin LIN Wang LUO Yong ZENG Zhenbing. Reachability analysis of nonlinear hybrid systems based on polyhedron inclusion[J]. Journal of Computer Applications, 2013, 33(05): 1289-1293.

参考文献

［1］KOPKE P, HENZINGER T A, PURL, A， et al. What's decidable about hybrid automata?［J］. Journal of Computer and System Sciences, 1995，57(1): 94-124.

［2］LAFFERRIERE G, PAPPAS G, YOVINE S. A new class of decidable hybrid systems［C］// Hybrid Systems: Computation and Control, LNCS 1569. Berlin: Springer, 1999: 137-151.

［3］ZHANG H B, DUAN Z H. Symbolic algorithmic analysis of rectangular hybrid systems［J］. Journal of Computer Science and Technology, 2009, 24(3): 531-543.

［4］HARTMANNS A, HERMANNS H. A modest approach to checking probabilistic timed automata［C］// Proceedings of the 6th International Conference on Quantitative Evaluation of Systems. Washington, DC: IEEE Computer Society, 2009: 187-196.

［5］COLLINS P. Continuity and computability of reachable sets ［J］. Theoretical Computer Science, 2005, 341(1): 162-195.

［6］ASARIN E, BOURNEZ O, DANG T, et al. Approximate reachability analysis of piecewise linear dynamical systems［C］// Hybrid Systems: Computation and Control, LNCS 1790. London: Springer, 2000: 21-31.

［7］KURZHANSKIY A, VARAIYA P. Ellipsoidal techniques for reachability analysis of discrete-time linear systems［J］. IEEE Transactions on Automatic Control, 2007, 52(1): 26-38.

［8］THOMAS S, ASHISH T. Verification and synthesis using real quantifier elimination［C］// The 36th International Symposium on Symbolic and Algebraic Computation. New York: ACM, 2011: 329-336.

［9］COLAS L G, ANTOINE G. Reachability analysis of hybrid systems using support functions［C］// Proceedings of the 21th International Conference on Computer Aided Verification, LNCS 5643. Berlin: Springer, 2009: 540-554.

［10］FREHSE G. PHAVer: algorithmic verification of hybrid systems past HyTech［J］. International Journal on Software Tools for Technology Transfer, 2008, 10(3): 263-279.

［11］SILVA B, RICHESON K, KROGH B, et al. Modeling and verifying hybrid dynamic systems using CheckMate［C］// Proceedings of the 4th International Conference on Automation of Mixed Processes. Dortmund: Shaker, 2000: 323-328.
［12］FREHSE G, GUERNIC C L, DONZE A, et al. SpaceEx: Scalable verification of hybrid systems［C］// Proceedings of the 23th International Conference on Computer Aided Verification, LNCS 6806. Berlin: Springer, 2011: 379-395.

［13］EUGENE A, THAO D, ODED M. The d/dt tool for verification of hybrid systems［C］// Proceedings of the 14th International Conference on Computer Aided Verification, LNCS 2404. Berlin: Springer, 2002: 365-370.

［14］

EUGENE A, THAO D, ANTOINE G. Reachability analysis of nonlinear systems using conservative approximation［C］// Proceedings of the 6th ACM International Conference on Hybrid Systems: Computation and Control. New York: ACM, 2003: 20-35.

［15］ASARIN E, DANG T, GIRARD A. Hybridization methods for the analysis of nonlinear systems［J］. Acta Informatica, 2007, 43(7): 451-476.

［16］DANG T, MALER O, TESTYLIER R. Accurate hybridization of nonlinear systems［C］// Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control. New York: ACM, 2010: 11-20.

［17］HENZINGER T A, WONG-TOI H. Linear phase-portrait approximations for nonlinear hybrid systems［C］// Hybrid Systems Ⅲ: Verication and Control, LNCS 1066. Berlin: Springer, 1996: 377-388.

［18］YANG L, ZHOU C, ZHAN N, et al. Recent advances in program verification through computer algebra［J］. Frontiers of Computer Science in China, 2010, 4(1): 1-16.

［19］XIA B. DISCOVERER: A tool for solving semi-algebraic systems［J］. ACM Communications in Computer Algebra, 2007, 41(3): 102-103.

［20］HONG H, EI DIN M S. Variant real quantifier elimination: algorithm and application［C］// Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation. New York: ACM, 2009: 183-190.

［21］BROWN C W. QEPCAD B - a program for computing with semi-algebraic sets using CADs［J］. ACM SIGSAM Bulletin, 2003, 37(4): 97-108.

［22］STURM T. REDLOG online resources for applied quantifier elimination［J］. Acta Academiae Aboensis, 2007, 67(2): 177-191.

［23］RATSCHAN S, SHE Z. Safety verification of hybrid systems by constraint propagation-based abstraction refinement［J］. ACM Transactions on Embedded Computing Systems, 2007,6(1): Article No. 8.

[1]	陈发堂, 张友寿, 杜铮. 5G低密度奇偶校验码的低复杂度偏移最小和算法[J]. 计算机应用, 2020, 40(7): 2028-2032.
[2]	沈敏捷, 曾振柄, 林望, 杨争峰. 基于随机障碍验证的随机连续系统安全性验证[J]. 计算机应用, 2018, 38(6): 1737-1744.
[3]	任志宇陈性元. 基于属性的用户-角色委派模型可达性分析[J]. 计算机应用, 2014, 34(2): 428-432.
[4]	莫铁强段珊. 硬实时调度的线性近似分析方法[J]. 计算机应用, 2010, 30(2): 427-429.

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

Reachability analysis of nonlinear hybrid systems based on polyhedron inclusion

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 4

编辑推荐

Metrics