A Greedy Approach for the Efficient Repair of Stochastic Models

For discrete-time probabilistic models there are efficient methods to check whether they satisfy certain properties. If a property is refuted, available techniques can be used to explain the failure in form of a counterexample. However, there are no scalable approaches to repair a model, i.e. to modify it with respect to certain side conditions such that the property is satisfied. We propose such a method, which avoids expensive computations and is therefore applicable to large models. A prototype implementation is used to demonstrate the applicability and scalability of our technique.