Discounting in LTL

TL;DR

This paper introduces a discounting extension to Linear Temporal Logic (LTL) that quantifies how quickly system requirements are met, enabling reasoning about system quality and satisfaction levels.

Contribution

It formalizes discounting in LTL, studies its combination with propositional quality operators, and analyzes the decidability and complexity of model checking with these extensions.

Findings

Augmenting LTL with discounting functions preserves decidability.

Adding unary propositional quality operators maintains decidability.

Introducing an average-operator leads to undecidability.

Abstract

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 \emph{how well} the system satisfies the specification. One direction in this effort is to refine the "eventually" operators of temporal logic to {\em 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 some problems undecidable. We also discuss the complexity of the problem, as well as various extensions.