---
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.\r\nThe 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.\r\nWe
    show that for automatic distance functions, and ω-regular linear-time and branching-time
    specifications, the model-measuring problem can be solved.\r\nWe 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. \r\nWe 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.15479/AT:IST-2014-172-v1-1
  dct_date: 2014^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/2664-1690
  dct_language: eng
  dct_publisher: IST Austria@
  dct_title: From model checking to model measuring@
...