[HahnHZ09] Probabilistic Reachability for Parametric Markov Models Hahn, E. M.; Hermanns, H. and Zhang, L. In Model Checking Software, 16th International SPIN Workshop, pages 88-106, Springer, Lecture Notes in Computer Science 5578, 2009.
Downloads: pdf, bibURL: http://dx.doi.org/10.1007/978-3-642-02652-2_10 Abstract. Given a parametric Markov model, we consider the problem of computing the formula expressing the probability of reaching a given set of states. To attack this principal problem, Daws has suggested to first convert the Markov chain into a finite automaton, from which a regular expression is computed. Afterwards, this expression is evaluated to a closed form expression representing the reachability probability. This paper investigates how this idea can be turned into an effective procedure. It turns out that the bottleneck lies in an exponential growth of the regular expression relative to the number of states. We therefore proceed differently, by tightly intertwining the regular expression computation with its evaluation. This allows us to arrive at an effective method that avoids the exponential blow up in most practical cases. We give a detailed account of the approach, also extending to parametric models with rewards and with non-determinism. Experimental evidence is provided, illustrating that our implementation provides meaningful insights on non-trivial models.