Fairness and promptness in Muller formulas

TL;DR

This paper compares different model checking problems for LTL and its fragments, focusing on fairness and promptness, and identifies cases where complexity and efficiency differ.

Contribution

It analyzes the Muller fragment and introduces a new expressive fragment of pLTL where fair model checking is more efficient than universal checking.

Findings

Muller fragment of pLTL does not share the same algorithmic properties as LTL.

A new expressive fragment of pLTL is identified with faster fair model checking.

Universal and fair model checking problems are PSPACE-complete for LTL.

Abstract

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.