Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Model Repair for Probabilistic Systems
verfasst von : Ezio Bartocci, Radu Grosu, Panagiotis Katsaros, C. R. Ramakrishnan, Scott A. Smolka
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We introduce the problem of Model Repair for Probabilistic Systems as follows. Given a probabilistic system
M
and a probabilistic temporal logic formula
φ
such that
M
fails to satisfy
φ
, the Model Repair problem is to find an
M
′ that satisfies
φ
and differs from
M
only in the transition flows of those states in
M
that are deemed controllable. Moreover, the cost associated with modifying
M
’s transition flows to obtain
M
′ should be minimized. Using a new version of parametric probabilistic model checking, we show how the Model Repair problem can be reduced to a nonlinear optimization problem with a minimal-cost objective function, thereby yielding a solution technique. We demonstrate the practical utility of our approach by applying it to a number of significant case studies, including a DTMC reward model of the Zeroconf protocol for assigning IP addresses, and a CTMC model of the highly publicized Kaminsky DNS cache-poisoning attack.