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

摘要

作为一种动态知识表示形式,动态时序逻辑( DLTL)尤适用于正规程序验证,然而它不直接支持测试动作,这使得其应用受到一定限制.为支持测试动作,提出一个DLTL扩展DLTL+和一个判定DLTL+公式可满足性的tableau算法,并给出了算法的正确性以及其时间复杂度为20(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.