---
_id: '1196'
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. 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;
    robustness problems that measure how much a model can be perturbed without violating
    the specification; and parameter synthesis for hybrid systems. We show that for
    automatic distance functions, and (a) . ω-regular linear-time, (b) . ω-regular
    branching-time, and (c) hybrid specifications, the model-measuring problem can
    be solved.We use automata-theoretic model-checking methods for model measuring,
    replacing the emptiness question for word, tree, and hybrid automata by the .
    optimal-value question for the weighted versions of these automata. For automata
    over words and trees, we consider weighted automata that accumulate weights by
    maximizing, summing, discounting, and limit averaging. For hybrid automata, we
    consider monotonic (parametric) hybrid automata, a hybrid counterpart of (discrete)
    weighted automata.We give several examples of using the model-measuring problem
    to compute various notions of robustness and quantitative satisfaction for temporal
    specifications. Further, we propose the modeling framework for model measuring
    to ease the specification and reduce the likelihood of errors in modeling.Finally,
    we present a variant of the model-measuring problem, called the . model-repair
    problem. The model-repair problem applies to models that do not satisfy the specification;
    it can be used to derive restrictions, under which the model satisfies the specification,
    i.e., to repair the model.'
acknowledgement: "This research was supported in part by the European Research Council
  (ERC) under grant 267989 (QUAREM), by the Austrian Science Fund1 (FWF) under grants
  S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), and by the National Science
  Centre (NCN), Poland under grant 2014/15/D/ST6/04543.\r\nA Technical Report of this
  article is available via: https://repository.ist.ac.at/171/"
article_processing_charge: No
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. Model measuring for discrete and hybrid systems. <i>Nonlinear
    Analysis: Hybrid Systems</i>. 2017;23:166-190. doi:<a href="https://doi.org/10.1016/j.nahs.2016.09.001">10.1016/j.nahs.2016.09.001</a>'
  apa: 'Henzinger, T. A., &#38; Otop, J. (2017). Model measuring for discrete and
    hybrid systems. <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier. <a href="https://doi.org/10.1016/j.nahs.2016.09.001">https://doi.org/10.1016/j.nahs.2016.09.001</a>'
  chicago: 'Henzinger, Thomas A, and Jan Otop. “Model Measuring for Discrete and Hybrid
    Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier, 2017. <a href="https://doi.org/10.1016/j.nahs.2016.09.001">https://doi.org/10.1016/j.nahs.2016.09.001</a>.'
  ieee: 'T. A. Henzinger and J. Otop, “Model measuring for discrete and hybrid systems,”
    <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23. Elsevier, pp. 166–190, 2017.'
  ista: 'Henzinger TA, Otop J. 2017. Model measuring for discrete and hybrid systems.
    Nonlinear Analysis: Hybrid Systems. 23, 166–190.'
  mla: 'Henzinger, Thomas A., and Jan Otop. “Model Measuring for Discrete and Hybrid
    Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, Elsevier, 2017,
    pp. 166–90, doi:<a href="https://doi.org/10.1016/j.nahs.2016.09.001">10.1016/j.nahs.2016.09.001</a>.'
  short: 'T.A. Henzinger, J. Otop, Nonlinear Analysis: Hybrid Systems 23 (2017) 166–190.'
date_created: 2018-12-11T11:50:39Z
date_published: 2017-02-01T00:00:00Z
date_updated: 2025-04-15T06:25:59Z
day: '01'
department:
- _id: ToHe
doi: 10.1016/j.nahs.2016.09.001
ec_funded: 1
external_id:
  isi:
  - '000390637000011'
intvolume: '        23'
isi: 1
language:
- iso: eng
month: '02'
oa_version: None
page: 166 - 190
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: Formal methods for the design and analysis of complex systems
publication: 'Nonlinear Analysis: Hybrid Systems'
publication_status: published
publisher: Elsevier
publist_id: '6154'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Model measuring for discrete and hybrid systems
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 23
year: '2017'
...