Jun 13, 2017: Arnd Hartmanns: Time- and Reward-Bounded Probabilistic Model Checking Techniques

June 13, 2017Time- and Reward-Bounded Probabilistic Model Checking Techniques
Room: Hal B 2BArnd Hartmanns

In the design of probabilistic timed systems, requirements concerning behaviour that occurs within a given time or energy budget are of central importance. Model-checking such requirements for probabilistic timed automata can be reduced to checking reward-bounded properties on Markov decision processes. This is traditionally implemented by unfolding the model according to the bound, or by solving a sequence of linear programs. Neither scales well to large models. Using value iteration in place of linear programming achieves scalability but accumulates approximation error. In this talk, based on recent joint work with Moritz Hahn, I will present a correction of the value iteration-based scheme, two new approaches based on scheduler enumeration and state elimination, and a comparison of the practical performance and scalability of all techniques on a number of case studies from the literature. I will show that state elimination can significantly reduce runtime for large models or high bounds.