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

时间自动机与自动验证 被引量：3

Timed Automaton and Automatic Verification
下载PDF
导出
摘要 给出时间自动机的基本概念 ,描述了区域自动机的构造方法 ,并且实现了区域自动机的构造算法 .简述了通过时间自动机进行自动验证的过程 。 The property of timed automaton is presented. The basic concept of the timed automaton is given. The construction of the region automaton is described, and the algorithm to realize it is given. As an application of the timed automaton, the process of automatic verification by timed automaton is introduced. Finally the hardness of construction is analyzed briefly.
作者 宋煌 郑丽萍 庄雷 苏锦祥
机构地区 郑州大学计算机科学系
出处 《郑州大学学报（自然科学版）》 CAS 2001年第2期30-34,共5页 Journal of Zhengzhou University (Natural Science)
基金 国家自然科学基金资助项目 (项目编号 698730 40 )
关键词 时间转换表 时间自动机 区域自动机 时间后续 自动验证 构造算法 timed transaction table timed automaton region automaton time successive
分类号 TP301.1 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献8

  • 1[1]Alur R, Dill D L. A theory of timed automata. Theoret Comput Sci,1994,126:183～235.
  • 2[2]Alur R, Itai A, Kurshan R P, et al. Timing verification by successive approximation. Information and Computation, 1995,118:142～157.
  • 3[3]Rina S Cohen, Arie Y Gold. Theory of ω-language. Journal of Computer and System Science, 1977,15:168～184.
  • 4[4]Sistla A P, Vardi M, Wolper P. The complementation problem for Bichi automation with application to temporal logic. Theoret Comput Sci, 1987,49:217～237.
  • 5[5]Safra S. On the complexity of ω-automata. Proc 29th IEEE Symp on Foundations of Computer Science, 1988:319～327.
  • 6[6]Aggarwal S, Kurahan R P, Sharma D. A language for specification and analysis of protocols. IFIP Protocol Specification, Testing and Verification, 1983,3:181～402.
  • 7[7]Clarke E M, Emerson E A, Sistla A P. Automatic verification of finite-state concurrent systems using temporallogic specifications. ACM Trans Programing Languages Systems, 1986,8 (2):244～263.
  • 8[8]Browne M C, Clarke E M, Dill D L, et al. Automatic verification of sequential circuits using temporal logic.IEEE Trans Comput System Sci, 1986,8:117～141.

同被引文献26

  • 1万敏,莫智文.用构造性神经网络推导模糊有限状态自动机[J].四川师范大学学报（自然科学版）,2005,28(6):631-634. 被引量：3
  • 2晏荣杰,李广元,徐雨波,刘春明,唐稚松.有限精度时间自动机的可达性检测[J].软件学报,2006,17(1):1-10. 被引量：5
  • 3Moszkowski B. Executing temporal logic program[D]. Cambridge:Cambridge University, 1986.
  • 4Moszkowski B. An automata-theoretic completeness proof for interval temporal logic[C]//ICALP2000, Lecture Notes in Computer Science 1853. Berlin: Springer, 2000: 223-234.
  • 5Owre S, Rushby J,Shankar N. PVS: a prototype verification systemiC]// 11th International Conference on Automated Deduction. Lecture Notes in Artificial Imtelligence 107. London: Springer-Verlag, 1992:748-752.
  • 6Owre S, Shankan N. The formal semantics of PVS[-R]// SRI International Computer Science Laboratory. California: Menlo Park,1999.
  • 7Lin C, Shan Z, Liu T,et al. Modeling and inference of extended interval temporal logic for nondeterministic intervals[J]. IEEE Transactions on Systems, Man, and Cybernetics, 2005, 35(5):682-696.
  • 8Alur R.Timed Automata. In Halbwachs N, Peled D, eds. Proceedings of the 11th conference on Computer-Aided Verification[C] .LNCS1633,London: Springer-Verlag,1999:8-22.
  • 9陈江.基于UML时间顺序图的实时系统形式化分析及自动验证[D].中国计量学院硕士学位论文,2010.
  • 10Alur R, Dill D L. A theory of timed automata[ J]. Theoretical Computer Science, 1994, 126(2) : 183 -235.

引证文献3

二级引证文献7

郑州大学学报（自然科学版）
2001年 第2期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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