Model measuring for discrete and hybrid systems

详细信息    查看全文

• 作者：Thomas A. Henzinger^a ; Jan Otop^a ; ^b ; ^{jotop@cs.uni.wroc.pl}
• 关键词：Quantitative model checking ; Weighted automata ; Parametric hybrid automata ; Model measuring
• 刊名：Nonlinear Analysis: Hybrid Systems
• 出版年：2017
• 出版时间：February 2017
• 年：2017
• 卷：23
• 期：Complete
• 页码：166-190
• 全文大小：763 K
• 卷排序：23

文摘

We define the model-measuring problem  : given a model MM and specification φφ, what is the maximal distance ρρ such that all models M′M′ within distance ρρ from MM 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.