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片段并不具备相同的算法特性。同时，我们识别出一个新的表达性片段，其公平模型检测复杂度低于通用模型检测。