article
Model measuring for discrete and hybrid systems
published
yes
Thomas A
Henzinger
author 40876CD8-F248-11E8-B48F-1D18A9856A870000−0002−2985−7724
Jan
Otop
author 2FC5DA74-F248-11E8-B48F-1D18A9856A87
ToHe
department
Quantitative Reactive Modeling
project
Rigorous Systems Engineering
project
The Wittgenstein Prize
project
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.
Elsevier2017
eng
Nonlinear Analysis: Hybrid Systems10.1016/j.nahs.2016.09.001
23166 - 190
T. A. Henzinger and J. Otop, “Model measuring for discrete and hybrid systems,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, pp. 166–190, 2017.
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>
Henzinger TA, Otop J. 2017. Model measuring for discrete and hybrid systems. Nonlinear Analysis: Hybrid Systems. 23, 166–190.
Henzinger, Thomas A, and Jan Otop. “Model Measuring for Discrete and Hybrid Systems.” <i>Nonlinear Analysis: Hybrid Systems</i> 23 (2017): 166–90. <a href="https://doi.org/10.1016/j.nahs.2016.09.001">https://doi.org/10.1016/j.nahs.2016.09.001</a>.
T.A. Henzinger, J. Otop, Nonlinear Analysis: Hybrid Systems 23 (2017) 166–190.
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>.
Henzinger, T. A., & Otop, J. (2017). Model measuring for discrete and hybrid systems. <i>Nonlinear Analysis: Hybrid Systems</i>, <i>23</i>, 166–190. <a href="https://doi.org/10.1016/j.nahs.2016.09.001">https://doi.org/10.1016/j.nahs.2016.09.001</a>
11962018-12-11T11:50:39Z2020-08-11T10:09:00Z