论文研究 带测试动作的动态时序逻辑扩展.pdf

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