---
res:
bibo_abstract:
- 'We define the model-measuring problem: given a model M and specification φ, what
is the maximal distance ρ such that all models M′ within distance ρ from M satisfy
(or violate) φ. The model measuring problem presupposes a distance function on
models. We concentrate on automatic distance functions, which are defined by weighted
automata. The model-measuring problem subsumes several generalizations of the
classical model-checking problem, in particular, quantitative model-checking problems
that measure the degree of satisfaction of a specification, and robustness problems
that measure how much a model can be perturbed without violating the specification.
We show that for automatic distance functions, and ω-regular linear-time and branching-time
specifications, the model-measuring problem can be solved. We use automata-theoretic
model-checking methods for model measuring, replacing the emptiness question for
standard word and tree automata by the optimal-weight question for the weighted
versions of these automata. We consider weighted automata that accumulate weights
by maximizing, summing, discounting, and limit averaging. We give several examples
of using the model-measuring problem to compute various notions of robustness
and quantitative satisfaction for temporal specifications.@eng'
bibo_authorlist:
- 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: Jan
foaf_name: Otop, Jan
foaf_surname: Otop
foaf_workInfoHomepage: http://www.librecat.org/personId=2FC5DA74-F248-11E8-B48F-1D18A9856A87
bibo_doi: 10.1007/978-3-642-40184-8_20
bibo_volume: 8052
dct_date: 2013^xs_gYear
dct_language: eng
dct_publisher: Springer@
dct_title: From model checking to model measuring@
...