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

• 作者: 孙永新 赵希顺
• 来源期刊: 计算机应用研究
• 关键词: 测试动作 动态时序逻辑 扩展 tableau算法 计算复杂性
• 年，卷（期）: 2012,（9）
• 所属期刊栏目: 算法研究探讨
• 页码范围: 3269-3273
• 分类号: TP301
• 语种: 中文
• DOI: 10.3969/j.issn.1001-3695.2012.09.018

摘要

作为一种动态知识表示形式,动态时序逻辑( DLTL)尤适用于正规程序验证,然而它不直接支持测试动作,这使得其应用受到一定限制.为支持测试动作,提出一个DLTL扩展DLTL+和一个判定DLTL+公式可满足性的tableau算法,并给出了算法的正确性以及其时间复杂度为20(n)的证明.分析表明,DLTL+提供了一种直接的、有效的测试动作支持方式,该方式比已知的其他方式更具有实际应用价值.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	赵希顺	中山大学逻辑与认知研究所	16	17	3.0	4.0
2	孙永新	仲恺农业工程学院计算机科学与工程学院	4	7	1.0	2.0