Reference
[BartocciGKRS11] Model Repair for Probabilistic Systems. In TACAS, 2011.Downloads: bibURL: http://delab.csd.auth.gr/~katsaros/mrepair.pdf Abstract. We introduce the problem of Model Repair for Probabilistic Systems as follows. Given a probabilistic system M and a probabilistic temporal logic formula Phi such that M fails to satisfy Phi, the Model Repair problem is to find an M that satisfies Phi 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 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.
