Model Repair for Probabilistic Systems

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]

C. R. Ramakrishnan
(cram@cs.sunysb.edu)