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 spec
- PDF / 315,312 Bytes
- 16 Pages / 439.363 x 666.131 pts Page_size
- 42 Downloads / 159 Views
The Hebrew University, Jerusalem, Israel The Interdisciplinary Center, Herzliya, Israel
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 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 modelchecking problem undecidable. We also discuss the complexity of the problem, as well as various extensions.
1 Introduction One of the main obstacles to the development of complex hardware and software systems lies in ensuring their correctness. A successful paradigm addressing this obstacle is temporal-logic model checking – given a mathematical model of the system and a temporal-logic formula that specifies a desired behavior of it, decide whether the model satisfies the formula [5]. Correctness is Boolean: a system can either satisfy its specification or not satisfy it. The richness of today’s systems, however, justifies specification formalisms that are multi-valued. The multi-valued setting arises directly in systems with quantitative aspects (multi-valued / probabilistic / fuzzy) [9–11, 16, 23], but is applied also with respect to Boolean systems, where it origins from the semantics of the specification formalism itself [1, 7]. When considering the quality of a system, satisfying a specification should no longer be a yes/no matter. Different ways of satisfying a specification should induce different levels of quality, which should be reflected in the output of the verification procedure. Consider for example the specification G(request → F(response grant ∨ response deny)) (“every request is eventually responded, with either a grant or a denial”). There should be a difference between a computation that satisfies it with responses generated soon after requests and one that satisfies it with long waits. Moreover, there may be a difference between grant and deny responses, or cases in which no request is issued. The issue of generating high-quality hardware and software ´ E. Abrah´ am and K. Havelund (Eds.): TACAS 2014, LNCS 8413, pp. 424–439, 2014. c Springer-Verlag Berlin Heidelberg 2014
Discounting in LTL
425
systems attrac
Data Loading...
