期刊文献+

带测试动作的动态时序逻辑扩展

Extending dynamic linear time temporal logic to support test actions
下载PDF
导出
摘要 作为一种动态知识表示形式,动态时序逻辑(DLTL)尤适用于正规程序验证,然而它不直接支持测试动作,这使得其应用受到一定限制。为支持测试动作,提出一个DLTL扩展DLTL+和一个判定DLTL+公式可满足性的tableau算法,并给出了算法的正确性以及其时间复杂度为2O(n)的证明。分析表明,DLTL+提供了一种直接的、有效的测试动作支持方式,该方式比已知的其他方式更具有实际应用价值。 As a dynamic knowledge representation formalism,dynamic linear time temporal logic(DLTL) is especially suitable for being applied in verifying regular programs.But for the reason of no direct supporting for test actions,the application of DLTL is quite restricted.To support test actions,this paper proposed an extension of DLTL,DLTL+,presented a tableau algorithm for determining DLTL+ formulas’ satisfiability,and showed that the algorithm was correct and its time complexity was 2O(n).Analysis results demonstrate that DLTL+ provides a direct and efficient way for supporting test actions,which has more practical application value than other known ways
出处 《计算机应用研究》 CSCD 北大核心 2012年第9期3269-3273,共5页 Application Research of Computers
基金 国家自然科学基金资助项目(60970040)
关键词 测试动作 动态时序逻辑 扩展 TABLEAU算法 计算复杂性 test action dynamic linear temporal logic(DLTL) extension tableau algorithm computational complexity
  • 相关文献

参考文献7

  • 1HENRIKSEN J G, THIAGARAJAN P S. Dynamic linear time temporal logic[ J]. Annals of Pure and Applied logic,1999,96(1-3) ; 187-207.
  • 2HAREL D, KOZEN D,TIUR N J. Dynamic logic[ M]. Cambridge: The MIT Press, 2000.
  • 3KROGER F, MERZ S. Temporal logic and state systems [ M ] . New York : Springer-V erlag, 2008.
  • 4GIORDANO L,MARTELLI A,SCHWIND C. Reasoning about actions in dynamic linear time temporal logic [J]. Logic Journal Of IGPL, 2001,9(2) : 273-287.
  • 5GIORDANO L,MARTELLI A,SCHWIND C. Specifying and verifying interaction protocols in a temporal action logic [ J ]. Journal of Applied Logic,2007,5(2) :214-234.
  • 6孙永新,赵希顺,符志强.描述逻辑的动态时序扩展[J].计算机应用研究,2012,29(2):536-541. 被引量:5
  • 7WOLPER P,The tableau method for temporal logic : an overview[ J]. Logique et Analyse, 1985,28(110-111) :119-136.

二级参考文献15

  • 1BAADER F, CALVANSES D, McGUINNESS D, et al. The desCrip- tion logic handbook : theory, implementation, and applications [ M]. Cambridge: Cambridge University Press, 2003.
  • 2WOLTER F, ZAKHARYASCHEV M. Temporalizing description log- ics [ M ]//GABBAY D, De.RIJKE M. Frontiers of Combining Systems 2. [ S. 1. ] : Studies Press/Wiley, 1999:379-402.
  • 3ARTALE A, FRANCONI E. Temporal description logics [ M ]//GAB- BAY D, FISHER M, VILA L. Handbook of Time and Temporal Rea- soning in Artificial Intelligence. [ S. 1. ] : Elsevier, 2005: 375-388.
  • 4WOLTER F, ZAKHARYASCHEV M. Dynamic description logics [ C]//ZAKHARYASCHEV M, SEGERBERG K, RIJKE M, et al.Advances in Modal Logic. Stanford : CSLI Publications, 2000 : 449- 463.
  • 5STURM H, WOLTER F. A tableau calculus for temporal description logic: the expanding domain case[ J]. Journal of Logic and Com- putation,2002.12(5) : 809-838.
  • 6HENRIKSEN J G, THIGARAJAN P S. Dynamic linear time temporal logic[J]. Annals of Pure and Applied Iogic,1999,96(1-3) :187- 207.
  • 7HAREL D, KOZEN D, TIURYN J. Dynamic logic[ M]. Cambridge: MIT Press, 2000.
  • 8HOPCROFT J E, MOTWANI R, ULLMAN J D. Introduction to au- tomata theory, languages and computation [M]. MA : Addison Wes- ley Reading, 1979.
  • 9WOLPER P. The tableau method for temporal logic: an overview [ J ]. Logique et Analyse,1985,28(110-111 ) : H9-136.
  • 10BAADER F, SATFLER U. Tableau algorithms for description logics [J]. Studia Logica,2001,69( 1 ) :5-40.

共引文献4

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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