A formal structure for symbolic reachability analysis of rectangular hybrid systems

详细信息    查看全文

• 作者：HaiBin Zhang ; Cheng Zhao ; Rong Li
• 关键词：rectangular hybrid systems ; symbolic methods ; reachability analysis
• 刊名：SCIENCE CHINA Technological Sciences
• 出版年：2016
• 出版时间：February 2016
• 年：2016
• 卷：59
• 期：2
• 页码：347-356
• 全文大小：711 KB
• 参考文献：1.Henzinger T A, Kopke P W, Puri A, et al. What’s decidable about hybrid automata?. J Comput Syst Sci, 1998, 57: 94–124CrossRef MathSciNet
  2.Fang Y, Li D, Fan Z, et al. Study on pneumatic-fuel hybrid system based on waste heat recovery from cooling water of internal combustion engine. Sci China Tech Sci, 2013, 56: 3070–3080CrossRef
  3.Goubault E, Mullier O, Putot S, et al. Inner approximated reachability analysis. In: Proceeding of 17th International Workshop on Hybrid Systems: Computation and Control, Berlin, Germany, 2014. 163–172
  4.Gulwani S, Tiwari A. Constraint-based approach for hybrid systems. In: Proceeding of 20th International Conference on Computer Aided Verification, Princeton, USA, 2008. 190–203
  5.Bogomolov S, Mitrohin C, Podelski A. Composing reachability analyses of hybrid systems for safety and stability. In: Proceeding of 8th International Conference on Automated Technology for Verification and Analysis, Singapore, 2010. 21–24
  6.Frehse G, Guernic C L, Donz, A, et al. SpaceEx: Scalable verification of hybrid systems. In: Proceeding of 23rd International Conference on Computer Aided Verification, Snowbird, UT, USA, 2011. 379–395
  7.Clarke E M, Grumberg O, Peled D A. Model Checking. Cambridge, The MIT Press, 1999. 284–287
  8.Karmarkar N. A new polynomial-time algorithm for linear programming. Combinatorica, 1984, 4: 373–395CrossRef MathSciNet
  9.Preuibig J, Kowalewski S, Wong-Toi H, et al. An algorithm for the approximative analysis of rectangular automata. In: Proceeding of Formal Techniques in Real-Time and Fault-Tolerant Systems: 5th International Symposium, Lyngby, Denmark, 1998. 228–240
  10.Girard A. Reachability of uncertain linear hybrid systems using zonotopes. In: Proceeding of 8th International Workshop on Hybrid Systems: Computation and Control, Zurich, Switzerland, 2005. 291–305CrossRef
  11.Wang F. Symbolic parametric safety analysis of linear hybrid systems with BDD-like data-structures. In: Proceeding of 16th International Conference on Computer Aided Verification, Boston, MA, USA, 2004. 295–307CrossRef
  12.Benerecetti M, Faella M, Minopolo S. Reachability games for linear hybrid systems. In: Proceeding of 15th International Workshop on Hybrid Systems: Computation and Control, Beijing, 2012. 65–74
  13.Benerecetti M, Faella M. Tracking differentiable trajectories across polyhedra boundaries. In: Proceeding of 16th International Workshop on Hybrid Systems: Computation and Control, Philadelphia, USA, 2013. 193–202
  14.Althoff M, Krogh B H. Avoiding geometric intersection operations in reachability analysis of ybrid systems. In: Proceeding of 15th International Workshop on Hybrid Systems: Computation and Control, Beijing, 2012. 45–54
  15.Thai J, Bayen A. State estimation for polyhedral hybrid systems and application to the godunov scheme. In: Proceeding of 16th International Workshop on Hybrid Systems: Computation and Control, Philadelphia, USA, 2013. 143–152
  16.Tkachev I, Abate A. On approximation metrics for linear temporal model-checking of stochastic systems. In: Proceeding of 17th International Workshop on Hybrid Systems: Computation and Control, Berlin, Germany, 2014. 193–202
  17.Behrmannl G, Larsen K G, Pearson J, et al. Efficient timed reachability analysis using clock diffierence diagrams. In: Proceeding of 11th International Conference on Computer Aided Verification, Trento, Italy, 1999. 341–353
  18.Zhang H, Duan. Z. Symbolic algorithmic analysis of rectangular hybrid systems. J Comput Sci Technol, 2009. 24: 531–543MathSciNet
  
• 作者单位：HaiBin Zhang (1)
  Cheng Zhao (1)
  Rong Li (1)
  
  1. School of Cyber Engineering, Xidian University, Xi’an, 710071, China
  
• 刊物类别：Engineering
• 刊物主题：Chinese Library of Science
  Engineering, general
  
• 出版者：Science China Press, co-published with Springer
• ISSN：1869-1900

文摘

For symbolic reachability analysis of rectangular hybrid systems, the basic issue is finding a formal structure to represent and manipulate its infinite state spaces. Firstly, this structure must be closed to the reachability operation which means that reachable states from states expressed by this structure can be presented by it too. Secondly, the operation of finding reachable states with this structure should take as less computation as possible. To this end, a constraint system called rectangular zone is formalized, which is a conjunction of fixed amount of inequalities that compare fixed types of linear expressions with two variables to rational numbers. It is proved that the rectangular zone is closed to those reachability operations—intersection, elapsing of time and edge transition. Since the number of inequalities and the linear expression of each inequality is fixed in rectangular zones, so to obtain reachable rectangular zones, it just need to change the rational numbers to which these linear expressions need to compare. To represent rectangular zones and unions of rectangular zones, a data structure called three dimensional constraint matrix (TDCM) and a BDD-like structure rectangular hybrid diagram (RHD) are introduced. Keywords rectangular hybrid systems symbolic methods reachability analysis