## Abstract:

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.

## Bibtex Entry:

@inproceedings{BGKRS:TACAS11, author = {Ezio Bartocci and Radu Grosu and Panagiotis Katsaros and C. R. Ramakrishnan and Scott A. Smolka}, title = {Model Repair for Probabilistic Systems}, booktitle = {17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS})}, address = {Saarbrucken, Germany}, month = {March}, series = {Lecture Notes in Computer Science}, volume = {6605}, publisher = {Springer}, pages = {326--340}, year = {2011} }

Full Paper: |
[pdf] |

Home | Papers

C. R. Ramakrishnan

`(cram@cs.sunysb.edu)`