Formally Reasoning About Quality

In recent years, there has been a growing need and interest in formally reasoning about the quality of software and hardware systems. As opposed to traditional verification, in which one considers the question of whether a system satisfies a given specification or not, reasoning about quality addresses the question of how well the system satisfies the specification. We distinguish between two approaches to specifying quality. The first, propositional quality, extends the specification formalism with propositional quality operators, which prioritize and weight different satisfaction possibilities. The second, temporal quality, refines the eventually operators of the specification formalism with discounting operators, whose semantics takes into an account the delay incurred in their satisfaction. In this article, we introduce two quantitative extensions of Linear Temporal Logic (LTL), one by propositional quality operators and one by discounting operators. In both logics, the satisfaction value of a specification is a number in [0, 1], which describes the quality of the satisfaction. We demonstrate the usefulness of both extensions and study the decidability and complexity of the decision and search problems for them as well as for extensions of LTL that combine both types of operators.