论文标题
穆勒公式的公平和及时性
Fairness and promptness in Muller formulas
论文作者
论文摘要
在本文中，我们考虑了模型检查线性时间逻辑（LTL）的两个不同视图。一方面，我们考虑了LTL的通用模型检查问题，其中有人要求给定系统和给定的公式所有系统的运行均可满足该公式。另一方面，LTL的公平模型检查问题要求，对于给定的系统和给定的公式，系统的所有运行几乎所有运行均可满足该公式。结果表明，这两个问题具有相同的理论复杂性，即pspace complete。出现问题是人们是否可以找到这两个问题的复杂性不同的LTL片段。在先前的作品中，即穆勒碎片中发现了一个这样的碎片。我们解决了LTL（PLTL）迅速片段的类似比较。 PLTL用其他操作员（即及时的）扩展LTL。该操作员确保存在界限，以使其在此界限内满足可耐受性能。我们表明，相对于所考虑的比较，PLTL的相应Muller片段不具有相同的算法属性。我们还确定了一个新的表达片段，公平模型检查比通用模型更快。
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.
