---
res:
bibo_abstract:
- Boolean notions of correctness are formalized by preorders on systems. Quantitative
measures of correctness can be formalized by real-valued distance functions between
systems, where the distance between implementation and specification provides
a measure of “fit” or “desirability.” We extend the simulation preorder to the
quantitative setting, by making each player of a simulation game pay a certain
price for her choices. We use the resulting games with quantitative objectives
to define three different simulation distances. The correctness distance measures
how much the specification must be changed in order to be satisfied by the implementation.
The coverage distance measures how much the im- plementation restricts the degrees
of freedom offered by the specification. The robustness distance measures how
much a system can deviate from the implementation description without violating
the specification. We consider these distances for safety as well as liveness
specifications. The distances can be computed in polynomial time for safety specifications,
and for liveness specifications given by weak fairness constraints. We show that
the distance functions satisfy the triangle inequality, that the distance between
two systems does not increase under parallel composition with a third system,
and that the distance between two systems can be bounded from above and below
by distances between abstractions of the two systems. These properties suggest
that our simulation distances provide an appropriate basis for a quantitative
theory of discrete systems. We also demonstrate how the robustness distance can
be used to measure how many transmission errors are tolerated by error correcting
codes.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Pavol
foaf_name: Cerny, Pavol
foaf_surname: Cerny
foaf_workInfoHomepage: http://www.librecat.org/personId=4DCBEFFE-F248-11E8-B48F-1D18A9856A87
- foaf_Person:
foaf_givenName: Thomas A
foaf_name: Henzinger, Thomas A
foaf_surname: Henzinger
foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
orcid: 0000−0002−2985−7724
- foaf_Person:
foaf_givenName: Arjun
foaf_name: Radhakrishna, Arjun
foaf_surname: Radhakrishna
foaf_workInfoHomepage: http://www.librecat.org/personId=3B51CAC4-F248-11E8-B48F-1D18A9856A87
bibo_doi: 10.15479/AT:IST-2010-0003
dct_date: 2010^xs_gYear
dct_isPartOf:
- http://id.crossref.org/issn/2664-1690
dct_language: eng
dct_publisher: IST Austria@
dct_title: Simulation distances@
...