Bartocci/Grosu/Katsaros/Ramakrishnan/Smolka
## Model Repair for Probabilistic Systems.*

*
E. Bartocci, R. Grosu, P. Katsaros, C.R. Ramakrishnan and S.A. Smolka
*
We introduce the problem of Model Repair for Probabilistic
Systems as follows. Given a probabilistic system M and a probabilistic
temporal logic formula f such that M fails to satisfy f, the Model Repair
problem is to find an M' that satisfies f 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. We show how the Model Repair problem can
be formulated as an extended version of parametric probabilistic model
checking, which translates into 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 signicant 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.

*
In Proc. of TACAS'11, the 7th International Conference on
Tools and Algorithms for the Construction and Analysis of
Systems, Saarbruecken, Germany, March, 2011. Springer LNCS.
*

*This work was supported by the NSF Faculty Early Career
Development Award CCR01-33583, the NSF Expeditions Award
CNS-09-26190 and the NSF CCF05-23863 Award and the AFOSR
FA-0550-09-1-0481 Award.