期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

Symbolic Algorithmic Analysis of Rectangular Hybrid Systems 被引量：1

Symbolic Algorithmic Analysis of Rectangular Hybrid Systems
原文传递
导出
摘要 This paper investigates symbolic algorithmic analysis of rectangular hybrid systems. To deal with the symbolic reachability problem, a restricted constraint system called hybrid zone is formalized for the representation and manipulation of rectangular automata state-spaces. Hybrid zones are proved to be closed over symbolic teachability operations of rectangular hybrid systems. They are also applied to model-checking procedures for verifying some important classes of timed computation tree logic formulas. To represent hybrid zones, a data structure called difference constraint matrix is defined. These enable us to deal with the symbolic algorithmic analysis of rectangular hybrid systems in an efficient way. This paper investigates symbolic algorithmic analysis of rectangular hybrid systems. To deal with the symbolic reachability problem, a restricted constraint system called hybrid zone is formalized for the representation and manipulation of rectangular automata state-spaces. Hybrid zones are proved to be closed over symbolic teachability operations of rectangular hybrid systems. They are also applied to model-checking procedures for verifying some important classes of timed computation tree logic formulas. To represent hybrid zones, a data structure called difference constraint matrix is defined. These enable us to deal with the symbolic algorithmic analysis of rectangular hybrid systems in an efficient way.
作者 张海宾 段振华
机构地区 Institute of Computing Theory and Technology
出处 《Journal of Computer Science & Technology》 SCIE EI CSCD 2009年第3期534-543,共10页 计算机科学技术学报（英文版）
基金 supported by the National Natural Science Foundation of China under Grant Nos.60433010 and 60873018 the Specialized Research Foundation for the Doctoral Program of Chinese Higher Education under Grant No.200807010012 the Defense Pre-Research Project of China under Grant No.51315050105
关键词 hybrid systems model checking AUTOMATA temporal logic hybrid systems, model checking, automata, temporal logic
分类号 TP338 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献1

二级参考文献17

  • 1Duan ZH. Modeling of Hybrid Systems. Beijing: Science Press, 2005.
  • 2Henzinger TA, Majumdar R. Symbolic model checking for rectangular hybrid systems. In: Graf S, Schwartzbach M, eds. Proc. of the 6th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. LNCS 1785, Berlin: Springer-Verlag, 2000. 142-156.
  • 3Li GY. LTLC: A continuous-time temporal logic for real-time and hybrid systems [Ph.D. Thesis]. Beijing: Institute of Software, the Chinese Academy of Sciences, 2001 (in Chinese with English abstract).
  • 4Jr Clarke EM, Grumberg O, Peled DA. Model Checking. London: MIT Press, 1999.
  • 5Dill DL. Timing assumptions and verification of finite-state concurrent systems. In: Sifakis J, ed. Proc. of the Int'l Workshop on Automatic Verification Methods for Finite State Systems. LNCS 407, Berlin: Springer-Verlag, 1990. 197-212.
  • 6Wang F. Symbolic parametric safety analysis of linear hybrid systems with BDD-like data-structures. In: Alur R, Peled D, eds. Proc. of the 16th Int'l Conf. on Computer Aided Verification. LNCS 3114, Berlin: Springer-Verlag, 2004. 295-307.
  • 7Frehse G. PHAVer: Algorithmic verification of hybrid systems past HyTech. In: Morari M, Thiele L, eds. Proc. of the 8th Int'l Workshop on Hybrid Systems: Computation and Control. LNCS 3414, Berlin: Springer-Verlag, 2005. 258-273.
  • 8Alur R, Courcoubetis C, Halbwachs N, Henzinger TA, Ho PH, Nicollin X, Olivero A, Sifakis J, Yovine S. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 1995,138:3-34.
  • 9Alur R, Courcoubetis C, Henzinger TA, Ho PH. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In: Morari M, Thiele L, eds. Proe. of the Hybrid Systems. LNCS 736, Berlin: Springer-Verlag, 1993. 209-229.
  • 10Chutinan A, Krogh BH. Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In: Vaandrager FW,van Schuppen JH, eds. Proc. of the 2th Int'l Workshop on Hybrid Systems: Computation and Control. LNCS 1569, Berlin: Springer-Verlag, 1999. 76-90.

同被引文献22

  • 1KOPKE P, HENZINGER T A, PURL, A, et al. What's decidable about hybrid automata? [ J]. Journal of Computer and System Sci- ences, 1995, 57(1) : 94 - 124.
  • 2LAFFERRIERE G, PAPPAS G, YOVINE S. A new class of decid- able hybrid systems[C]// Hybrid Systems: Computation and Con- trol, LNCS 1569. Berlin: Springer, 1999:137-151.
  • 3HARTMANNS A, HERMANNS H. A modest approach to checking probabilistic timed automata[ C]// Proceedings of the 6th Interna- tional Conference on Quantitative Evaluation of Systems. Washing- ton, DC: IEEE Computer Society, 2009: 187-196.
  • 4COLLINS P. Continuity and computability of reachable sets [ J]. Theoretical Computer Science, 2005, 341(1) : 162 - 195.
  • 5ASARIN E, BOURNEZ O, DANG T, et al. Approximate reach- ability analysis of piecewise linear dynamical systems[ C]// Hybrid Systems: Computation and Control, LNCS 1790. London: Spring- er, 2000:21-31.
  • 6KURZHANSKIY A, VARAIYA P. Ellipsoidal techniques for reach- ability analysis of discrete-time linear systems[ J]. IEEE Transac- tions on Automatic Control, 2007, 52( 1): 26 -38.
  • 7THOMAS S, ASHISH T. Verification and synthesis using real quan- tifier elimination[ C]// The 36th International Symposium on Sym- bolic and Algebraic Computation. New York: ACM, 2011: 329- 336.
  • 8COLAS 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.
  • 9FREHSE G. PHAVer: algorithmic verification of hybrid systems past HyTech[ J]. International Journal on Software Tools for Tech- nology Transfer, 2008, 10(3) : 263 -279.
  • 10SILVA B, RICHESON K, KROGH B, et al. Modeling and verif- ying hybrid dynamic systems using CheckMate[ C]// Proceedings of the 4th International Conference on Automation of Mixed Proces- ses. Dortmund: Shaker, 2000:323-328.

引证文献1

二级引证文献1

Journal of Computer Science & Technology
2009年 第3期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部