Discounting in LTL

In recent years, there is growing need and interest in formalizing and reasoning about the quality of software and hardware systems. As opposed to traditional verification, where one handles the question of whether a system satisfies, or not, a given specification, reasoning about quality addresses the question of

how well

the system satisfies the specification. One direction in this effort is to refine the “eventually” operators of temporal logic to

discounting operators

: the satisfaction value of a specification is a value in [0,1], where the longer it takes to fulfill eventuality requirements, the smaller the satisfaction value is.

In this paper we introduce an augmentation by discounting of Linear Temporal Logic (LTL), and study it, as well as its combination with propositional quality operators. We show that one can augment LTL with an arbitrary set of discounting functions, while preserving the decidability of the model-checking problem. Further augmenting the logic with unary propositional quality operators preserves decidability, whereas adding an average-operator makes the model-checking problem undecidable. We also discuss the complexity of the problem, as well as various extensions.