  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.
