In this paper we consider two different views of the model checking problems for the Linear Temporal Logic (LTL). On the one hand, we consider the universal model checking problem for LTL, where one asks that for a given system and a given formula all the runs of the system satisfy the formula. On the other hand, the fair model checking problem for LTL asks that for a given system and a given formula almost all the runs of the system satisfy the formula. It was shown that these two problems have the same theoretical complexity i.e. PSPACE-complete. The question arises whether one can find a fragment of LTL for which the complexity of these two problems differs. One such fragment was identified in a previous work, namely the Muller fragment. We address a similar comparison for the prompt fragment of LTL (pLTL). pLTL extends LTL with an additional operator, i.e. the prompt-eventually. This operator ensures the existence of a bound such that liveness properties are satisfied within this bound. We show that the corresponding Muller fragment for pLTL does not enjoy the same algorithmic properties with respect to the comparison considered. We also identify a new expressive fragment for which the fair model checking is faster than the universal one.

翻译：本文探讨线性时序逻辑（LTL）模型检测问题的两种不同视角。一方面，我们考虑LTL的通用模型检测问题，即对于给定系统和公式，要求系统的所有运行轨迹均满足该公式。另一方面，LTL的公平模型检测问题则要求对于给定系统和公式，系统的几乎所有运行轨迹都满足该公式。已有研究表明这两个问题具有相同的理论复杂度，即均为PSPACE完全问题。这引发了一个疑问：能否找到LTL的一个片段，使得这两个问题的复杂度产生差异？先前研究已发现一个这样的片段，即Muller片段。本文针对LTL的及时片段（pLTL）进行了类似的比较研究。pLTL通过引入"及时最终"算子扩展了LTL，该算子能确保存在一个界限，使得活性性质在该界限内得到满足。我们证明，对于所考虑的对比维度，pLTL对应的Muller片段并不具备相同的算法特性。同时，我们识别出一个新的表达性片段，其公平模型检测的复杂度低于通用模型检测。