The complexity of the temporal logic with “until” over general linear time
作者:
Highlights:
•
摘要
It is shown that the decision problem for the temporal logic with the strict until operator over general linear time is PSPACE-complete. This shows that it is no harder to reason with arbitrary linear orderings than with discrete linear time temporal logics. New techniques are used to give a PSPACE procedure for the logic.
论文关键词:
论文评审过程:Received 3 June 1999, Revised 8 March 2002, Available online 23 April 2003.
论文官网地址:https://doi.org/10.1016/S0022-0000(03)00005-9