Talks and Poster Presentations (with Proceedings-Entry):
E. Bartocci, R. Grosu, P. Katsaros, C. Ramakrishnan, S. Smolka:
"Model Repair for Probabilistic Systems";
Talk: 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS),
- 2011-04-03; in: "Proc. of 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)",
LNCS / Springer,
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.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
Created from the Publication Database of the Vienna University of Technology.