Model measuring for discrete and hybrid systems Journal Article


Author(s): Henzinger, Thomas A; Otop, Jan
Article Title: Model measuring for discrete and hybrid systems
Affiliation IST Austria
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; 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.
Keywords: Weighted automata; Model measuring; Parametric hybrid automata; Quantitative model checking
Journal Title: Nonlinear Analysis: Hybrid Systems
Volume: 23
ISSN: 1751-570X
Publisher: Elsevier  
Date Published: 2017-02-01
Start Page: 166
End Page: 190
DOI: 10.1016/j.nahs.2016.09.001
Notes: 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. A Technical Report of this article is available via: https://repository.ist.ac.at/171/
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    398 Henzinger
  2. Jan Otop
    15 Otop
Related IST Austria Work