Probabilistic Reachability for Parametric Markov Models
, 13: 3-19, 2011.
Downloads: pdf, bibURL: http://dx.doi.org/10.1007/s10009-010-0146-x
Abstract. Given a parametric Markov model, we consider the problem of
computing the rational function 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 function 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 the growth of the regular expression relative
to the number of states (n^Θ(log n)). 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 this
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.