文件名称：论文研究-带测试动作的动态时序逻辑扩展.pdf
文件大小：993KB
文件格式：PDF
更新时间：2022-08-11 11:51:06
测试动作, 动态时序逻辑, 扩展, tableau算法, 计算复杂性
作为一种动态知识表示形式, 动态时序逻辑DLTL尤适用于正规程序验证, 然而它不直接支持测试动作, 这使得其应用受到一定限制。为支持测试动作, 提出一个DLTL扩展DLTL 和一个判定DLTL 公式可满足性的tableau算法, 并给出了算法的正确性以及其时间复杂度为2On的证明。分析表明, DLTL 提供了一种直接的、有效的测试动作支持方式, 该方式比已知的其他方式更具有实际应用价值。