Extending dynamic linear time temporal logic to support test actions
带测试动作的动态时序逻辑扩展

As a dynamic knowledge representation formalism, dynamic linear time temporal logicDLTL 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 2On. 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.