Formalizing and reasoning about quality

S. Almagor, U. Boker, O. Kupferman, 7966 (2013) 15–27.

Download
OA 2013_ICALP_Almagor.pdf 363.03 KB

Conference Paper | Published | English

Scopus indexed
Author
Almagor, Shaull; Boker, UdiIST Austria; Kupferman, Orna
Department
Series Title
LNCS
Abstract
Traditional formal methods are based on a Boolean satisfaction notion: a reactive system satisfies, or not, a given specification. We generalize formal methods to also address the quality of systems. As an adequate specification formalism we introduce the linear temporal logic LTL[F]. The satisfaction value of an LTL[F] formula is a number between 0 and 1, describing the quality of the satisfaction. The logic generalizes traditional LTL by augmenting it with a (parameterized) set F of arbitrary functions over the interval [0,1]. For example, F may contain the maximum or minimum between the satisfaction values of subformulas, their product, and their average. The classical decision problems in formal methods, such as satisfiability, model checking, and synthesis, are generalized to search and optimization problems in the quantitative setting. For example, model checking asks for the quality in which a specification is satisfied, and synthesis returns a system satisfying the specification with the highest quality. Reasoning about quality gives rise to other natural questions, like the distance between specifications. We formalize these basic questions and study them for LTL[F]. By extending the automata-theoretic approach for LTL to a setting that takes quality into an account, we are able to solve the above problems and show that reasoning about LTL[F] has roughly the same complexity as reasoning about traditional LTL.
Publishing Year
Date Published
2013-07-01
Acknowledgement
ERC Grant QUALITY.
Volume
7966
Issue
Part 2
Page
15 - 27
Conference
ICALP: Automata, Languages and Programming
Conference Location
Riga, Latvia
Conference Date
2013-07-08 – 2013-07-12
IST-REx-ID

Cite this

Almagor S, Boker U, Kupferman O. Formalizing and reasoning about quality. 2013;7966(Part 2):15-27. doi:10.1007/978-3-642-39212-2_3
Almagor, S., Boker, U., & Kupferman, O. (2013). Formalizing and reasoning about quality. Presented at the ICALP: Automata, Languages and Programming, Riga, Latvia: Springer. https://doi.org/10.1007/978-3-642-39212-2_3
Almagor, Shaull, Udi Boker, and Orna Kupferman. “Formalizing and Reasoning about Quality.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-39212-2_3.
S. Almagor, U. Boker, and O. Kupferman, “Formalizing and reasoning about quality,” vol. 7966, no. Part 2. Springer, pp. 15–27, 2013.
Almagor S, Boker U, Kupferman O. 2013. Formalizing and reasoning about quality. 7966(Part 2), 15–27.
Almagor, Shaull, et al. Formalizing and Reasoning about Quality. Vol. 7966, no. Part 2, Springer, 2013, pp. 15–27, doi:10.1007/978-3-642-39212-2_3.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Main File(s)
File Name
Access Level
OA Open Access
Date Uploaded
2020-05-15
MD5 Checksum
85afbf6c18a2c7e377c52c9410e2d824


Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar