@inproceedings{HahnHZ09,
author = {Ernst Moritz Hahn and
Holger Hermanns and
Lijun Zhang},
title = {Probabilistic Reachability for Parametric Markov Models},
booktitle = {Model Checking Software, 16th International SPIN Workshop},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5578},
year = {2009},
pages = {88-106},
ee = {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.}
}