摘要：
针对一类非线性混成系统的可达性问题，提出了一种基于多面体包含的分析方法。首先介绍了混成系统及其可达性，讨论了如何应用多面体包含对多项式混成系统进行线性近似，并采用量词消去和非线性优化方法来构造相应的线性混成系统，然后运用验证工具SpaceEx求得原非线性混成系统的过近似可达集，并应用于验证系统的安全性。
关键词：
混成系统；可达性分析；安全性验证；多面体包含；线性近似
0引言
信息物理融合系统（CyberPhysical System， CPS）作为计算进程与物理过程的结合体，是集传感、通信、计算与控制于一身的下一代智能系统，已广泛应用于汽车、电力、航空航天、国防、工业自动化等重要领域。混成系统作为CPS的数学模型，是一类既包含连续动态行为又包含离散动态行为的复杂系统，其动力学行为既随时间而连续变化，又受事件而离散驱动。混成系统的分析与验证已成为当今计算机科学与控制学科的前沿研究热点。
可达性分析是混成系统分析与验证中的重要问题，是指系统是否可由初始状态开始，经系统轨迹到达某个给定的目标状态。许多混成系统验证问题，如安全性验证等，都可以转化为可达性分析问题。近年来，混成系统可达性分析已得到广泛研究，并取得了一些重要结果。文献[1-4]通过计算可达集对矩形自动机、多速率自动机、时间自动机等几类特殊的混成系统的可达性问题进行了研究。然而，对于大多数混成系统，连续变量和离散事件间相互作用的特性，使得可达集的精确计算非常困难，因而文献[5]提出了近似计算可达集的思想。在此基础上，文献[6]和文献[7]分别采用多面体（Polyhedron）、椭球体（Ellipsoid）等几何对象表示系统状态空间，并运用图论、几何方法和最优化方法等来近似计算一类线性混成系统的可达集。文献[8]将线性混成系统可达性问题归化为实闭域上的量词消去问题，进而运用现有的计算机代数系统进行有效求解。文献[9]考虑了一类带微分包含的线性混成系统的可达性问题，并通过构造支撑函数来得到系统的过近似可达集。目前，可应用于线性混成系统可达性分析的工具主要有Phaver[10]、CheckMate[11]、SpaceEx[12]、d/dt[13]等。而对于非线性混成系统，一般先将非线性混成系统转化为近似的线性混成系统，再通过对线性混成系统的研究来实现原先的非线性混成系统的分析与验证。文献[14-16]运用单纯形构造方法对系统状态空间进行划分，从而将非线性系统转化为带外部扰动的线性混成系统，并实现了原系统的近似可达集的计算。文献[17]运用线性phaseportrait近似方法一类特殊的非线性混成系统的可达性问题进行了研究。
本文将讨论多项式混成系统的可达性分析问题。首先提出了一个多面体包含方法来对多项式混成系统进行线性近似，并采用量词消去和非线性优化方法来构造相应的线性混成系统，然后运用验证工具SpaceEx计算系统的过近似可达集，并应用于系统的安全性验证。与已有的方法相比，本文的方法具有普遍性，适用于一般的多项式混成系统的分析与验证。
4结语
基于多面体包含线性近似方法，本文讨论了一类非线性混成系统的可达性问题，并进一步考虑了系统的安全性验证。提出了运用多面体包含来对非线性混成系统进行线性近似，采用半代数系统求解或量词消去与非线性优化方法相结合来构造相应的线性混成系统，然后运用验证工具SpaceEx计算原非线性混成系统的过近似可达集，并应用于验证系统的安全性。
参考文献：
[1]
KOPKE P， HENZINGER T A， PURL， A， et al. Whats 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 discretetime 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， WONGTOI H. Linear phaseportrait 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 semialgebraic 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 semialgebraic 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 propagationbased abstraction refinement[J]. ACM Transactions on Embedded Computing Systems， 2007，6（1）： Article No. 8.