Advertisement
Published in:
2011 | OriginalPaper | Chapter
Model Repair for Probabilistic Systems
Authors : Ezio Bartocci, Radu Grosu, Panagiotis Katsaros, C. R. Ramakrishnan, Scott A. Smolka
Published in: Tools and Algorithms for the Construction and Analysis of Systems
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. 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.