TY - GEN
T1 - Model repair for probabilistic systems
AU - Bartocci, Ezio
AU - Grosu, Radu
AU - Katsaros, Panagiotis
AU - Ramakrishnan, C. R.
AU - Smolka, Scott A.
PY - 2011
Y1 - 2011
N2 - 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.
AB - 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.
KW - Model Repair
KW - Nonlinear Programming
KW - Probabilistic Model Checking
UR - https://www.scopus.com/pages/publications/79953188750
U2 - 10.1007/978-3-642-19835-9_30
DO - 10.1007/978-3-642-19835-9_30
M3 - Conference contribution
AN - SCOPUS:79953188750
SN - 9783642198342
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 326
EP - 340
BT - Tools and Algorithms for the Construction and Analysis of Systems - 17th Int. Conf., TACAS 2011, Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2011, Proceedings
PB - Springer Verlag
T2 - 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011
Y2 - 26 March 2011 through 3 April 2011
ER -