---
_id: '5417'
abstract:
- lang: eng
  text: "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."
alternative_title:
- IST Austria Technical Report
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Jan
  full_name: Otop, Jan
  id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
  last_name: Otop
citation:
  ama: Henzinger TA, Otop J. <i>From Model Checking to Model Measuring</i>. IST Austria;
    2014. doi:<a href="https://doi.org/10.15479/AT:IST-2014-172-v1-1">10.15479/AT:IST-2014-172-v1-1</a>
  apa: Henzinger, T. A., &#38; Otop, J. (2014). <i>From model checking to model measuring</i>.
    IST Austria. <a href="https://doi.org/10.15479/AT:IST-2014-172-v1-1">https://doi.org/10.15479/AT:IST-2014-172-v1-1</a>
  chicago: Henzinger, Thomas A, and Jan Otop. <i>From Model Checking to Model Measuring</i>.
    IST Austria, 2014. <a href="https://doi.org/10.15479/AT:IST-2014-172-v1-1">https://doi.org/10.15479/AT:IST-2014-172-v1-1</a>.
  ieee: T. A. Henzinger and J. Otop, <i>From model checking to model measuring</i>.
    IST Austria, 2014.
  ista: Henzinger TA, Otop J. 2014. From model checking to model measuring, IST Austria,
    14p.
  mla: Henzinger, Thomas A., and Jan Otop. <i>From Model Checking to Model Measuring</i>.
    IST Austria, 2014, doi:<a href="https://doi.org/10.15479/AT:IST-2014-172-v1-1">10.15479/AT:IST-2014-172-v1-1</a>.
  short: T.A. Henzinger, J. Otop, From Model Checking to Model Measuring, IST Austria,
    2014.
date_created: 2018-12-12T11:39:13Z
date_published: 2014-02-19T00:00:00Z
date_updated: 2024-10-21T06:02:58Z
day: '19'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2014-172-v1-1
file:
- access_level: open_access
  checksum: fcc3eab903cfcd3778b338d2d0d44d18
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:20Z
  date_updated: 2020-07-14T12:46:49Z
  file_id: '5481'
  file_name: IST-2014-172-v1+1_report.pdf
  file_size: 383052
  relation: main_file
file_date_updated: 2020-07-14T12:46:49Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '14'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '175'
related_material:
  record:
  - id: '2327'
    relation: later_version
    status: public
status: public
title: From model checking to model measuring
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...