线性时态逻辑的决策问题复杂性

不同的时态逻辑能够适应不同的推理任务。为了符合应用,关于时间的模型从离散的自然数和整数,延伸到稠密的线性实数,甚至扩展到区间代数和树代数。如果简单的时态连接词的表达力已经足够,就只需使用这些简单的时态连接词来构造的时态逻辑。在能够承担降低运算速度的风险下,我们可以为实现更强的表达力而使用更多的连接词,也可以加上度量信息或者固定点。作者近期提出了一个令人惊讶的结论:建立在实数时间上的具有足够表达力的语言和基于自然数离散时间流的传统简单算子,它们推理的计算复杂性是一样的。在这篇论文中,作者试图对建立在标准时态连接词和线性时间流的普通类上的时态逻辑中所有决策问题的计算复杂性作新的说明。尤其是,文中指出,所有标准逻辑在PSPACE中都存在决策问题。

The Complexity of Decision Problems for Linear Temporal Logics

There are a variety of temporal logics appropriate for a variety of reasoning tasks. The underlying model of time appropriate to the application can range from discrete natural numbers and integers to dense linear real numbers or to algebras of intervals and trees. The temporal language can be built from a few simple temporal connectives, if they are adequately expressive or we can have many more connectives, or add metric information or fix points if we can afford to risk sacrificing the speed of reasoning to gain increased expressiveness. The author has recently shown the surprising result that as far as computational complexity of reasoning is concerned, it is just as easy to reason with an adequately expressive language over real numbers time, as it is to reason with traditional simple operators on the discrete natural numbers flow of time. In this paper we build on that new result to give an account of the computational complexity of all the decision problems for any temporal logic using standard style temporal connectives over any of the common classes of linear flows of time. In particular we show that all the standard logics have decision problems in PSPACE.