Traditionally, the goal of formal methods is to determine whether a system satisfies its specification. In other words, the outcome is a yes/no answer. This yields the important practical result of model checkers that verify whether a finite-state system satisfies a specification expressed in linear temporal logic (LTL). This paper generalizes this traditional view by also addressing the quality of a system by finding the degree to which it meets its specification.

For this purpose, a logic LTL[F] is introduced in which the value of a formula is not just true or false, but also a real number from zero to one. If a specification expressed in LTL[F] for a system S yields a higher value than for a system S’, then S satisfies the specification better than S’. The logic is parameterized to a set F of functions over the interval [0,1]. These functions can be used to combine the values of subformulas. In other words, they replace the classical logical connectives. By selecting different choices for F, different variants of the logic for different domains can be derived.

A core property of LTL[F] is that its formulas have only finitely many satisfaction values. Generalizing the classical translation of LTL formulas to automata thus enables the effective solution of problems such as model checking LTL[F].

The paper sketches the core ideas in terms that are easy to read. It also shows possible generalizations such as weighted atomic propositions, branching time logic, and more efficiently decidable fragments. The presentation may thus lead to additional fruitful research.