---
_id: '3840'
abstract:
- lang: eng
text: 'Classical formalizations of systems and properties are boolean: given a system
and a property, the property is either true or false of the system. Correspondingly,
classical methods for system analysis determine the truth value of a property,
preferably giving a proof if the property is true, and a counterexample if the
property is false; classical methods for system synthesis construct a system for
which a property is true; classical methods for system transformation, composition,
and abstraction aim to preserve the truth of properties. The boolean view is prevalent
even if the system, the property, or both refer to numerical quantities, such
as the times or probabilities of events. For example, a timed automaton either
satisfies or violates a formula of a real-time logic; a stochastic process either
satisfies or violates a formula of a probabilistic logic. The classical black-and-white
view partitions the world into "correct" and "incorrect" systems, offering few
nuances. In reality, of several systems that satisfy a property in the boolean
sense, often some are more desirable than others, and of the many systems that
violate a property, usually some are less objectionable than others. For instance,
among the systems that satisfy the response property that every request be granted,
we may prefer systems that grant requests quickly (the quicker, the better), or
we may prefer systems that issue few unnecessary grants (the fewer, the better);
and among the systems that violate the response property, we may prefer systems
that serve many initial requests (the more, the better), or we may prefer systems
that serve many requests in the long run (the greater the fraction of served to
unserved requests, the better). Formally, while a boolean notion of correctness
is given by a preorder on systems and properties, a quantitative notion of correctness
is defined by a directed metric on systems and properties, where the distance
between a system and a property provides a measure of "fit" or "desirability."
There are many ways how such distances can be defined. In a linear-time framework,
one assigns numerical values to individual behaviors before assigning values to
systems and properties, which are sets of behaviors. For example, the value of
a single behavior may be a discounted value, which is largely determined by a
prefix of the behavior, e.g., by the number of requests that are granted before
the first request that is not granted; or a limit value, which is independent
of any finite prefix. A limit value may be an average, such as the average response
time over an infinite sequence of requests and grants, or a supremum, such as
the worst-case response time. Similarly, the value of a set of behaviors may be
an extremum or an average across the values of all behaviors in the set: in this
way one can measure the worst of all possible average-case response times, or
the average of all possible worst-case response times, etc. Accordingly, the distance
between two sets of behaviors may be defined as the worst or average difference
between the values of corresponding behaviors. In summary, we propagate replacing
boolean specifications for the correctness of systems with quantitative measures
for the desirability of systems. In quantitative analysis, the aim is to compute
the distance between a system and a property (or between two systems, or two properties);
in quantitative synthesis, the objective is to construct a system that has minimal
distance from a given property. Multiple quantitative measures can be prioritized
(e.g., combined lexicographically into a single measure) or studied along the
Pareto curve. Quantitative transformations, compositions, and abstractions of
systems are useful if they allow us to bound the induced change in distance from
a property. We present some initial results in some of these directions. We also
give some potential applications, which not only generalize tradiditional correctness
concerns in the functional, timed, and probabilistic domains, but also capture
such system measures as resource use, performance, cost, reliability, and robustness.'
acknowledgement: This talk surveys joint work with Roderick Bloem, Krishnendu Chatterjee,
Laurent Doyen, and Barbara Jobstmann.
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Henzinger TA. From boolean to quantitative notions of correctness. In: Vol
45. ACM; 2010:157-158. doi:10.1145/1706299.1706319'
apa: 'Henzinger, T. A. (2010). From boolean to quantitative notions of correctness
(Vol. 45, pp. 157–158). Presented at the POPL: Principles of Programming Languages,
Madrid, Spain: ACM. https://doi.org/10.1145/1706299.1706319'
chicago: Henzinger, Thomas A. “From Boolean to Quantitative Notions of Correctness,”
45:157–58. ACM, 2010. https://doi.org/10.1145/1706299.1706319.
ieee: 'T. A. Henzinger, “From boolean to quantitative notions of correctness,” presented
at the POPL: Principles of Programming Languages, Madrid, Spain, 2010, vol. 45,
no. 1, pp. 157–158.'
ista: 'Henzinger TA. 2010. From boolean to quantitative notions of correctness.
POPL: Principles of Programming Languages vol. 45, 157–158.'
mla: Henzinger, Thomas A. From Boolean to Quantitative Notions of Correctness.
Vol. 45, no. 1, ACM, 2010, pp. 157–58, doi:10.1145/1706299.1706319.
short: T.A. Henzinger, in:, ACM, 2010, pp. 157–158.
conference:
end_date: 2010-01-23
location: Madrid, Spain
name: 'POPL: Principles of Programming Languages'
start_date: 2010-01-17
date_created: 2018-12-11T12:05:27Z
date_published: 2010-01-17T00:00:00Z
date_updated: 2021-01-12T07:52:34Z
day: '17'
department:
- _id: ToHe
doi: 10.1145/1706299.1706319
intvolume: ' 45'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 157 - 158
publication_status: published
publisher: ACM
publist_id: '2354'
quality_controlled: '1'
scopus_import: 1
status: public
title: From boolean to quantitative notions of correctness
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 45
year: '2010'
...