Fairness and promptness in Muller formulas

May 9, 2022

Léo Tible (LACL)

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 that all the runs of the system satisfy the formula.

On the other hand, 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 differ. 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.