From model checking to model measuring

T.A. Henzinger, J. Otop, 8052 (2013) 273–287.

Download
OA IST-2013-129-v1+1_concur.pdf 378.59 KB

Conference Paper | Published | English
Department
Series Title
LNCS
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, and robustness problems that measure how much a model can be perturbed without violating the specification. We show that for automatic distance functions, and ω-regular linear-time and branching-time specifications, the model-measuring problem can be solved. We 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. We give several examples of using the model-measuring problem to compute various notions of robustness and quantitative satisfaction for temporal specifications.
Publishing Year
Date Published
2013-08-01
Volume
8052
Page
273 - 287
Conference
CONCUR: Concurrency Theory
Conference Location
Buenos Aires, Argentina
Conference Date
2013-08-27 – 2013-08-30
IST-REx-ID

Cite this

Henzinger TA, Otop J. From model checking to model measuring. 2013;8052:273-287. doi:10.1007/978-3-642-40184-8_20
Henzinger, T. A., & Otop, J. (2013). From model checking to model measuring. Presented at the CONCUR: Concurrency Theory, Buenos Aires, Argentina: Springer. https://doi.org/10.1007/978-3-642-40184-8_20
Henzinger, Thomas A, and Jan Otop. “From Model Checking to Model Measuring.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-40184-8_20.
T. A. Henzinger and J. Otop, “From model checking to model measuring,” vol. 8052. Springer, pp. 273–287, 2013.
Henzinger TA, Otop J. 2013. From model checking to model measuring. 8052, 273–287.
Henzinger, Thomas A., and Jan Otop. From Model Checking to Model Measuring. Vol. 8052, Springer, 2013, pp. 273–87, doi:10.1007/978-3-642-40184-8_20.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Main File(s)
File Name
Access Level
OA Open Access
Date Uploaded
2018-12-12
MD5 Checksum
4c04695c4bfdf2119cd4f5d1babc3e8a


Material in IST:
Earlier Version

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar