Ernst Moritz Hahn

 

Probabilistic Reachability for Parametric Markov Models

 

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 talk 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^(Theta(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. Experimental evidence is provided,
illustrating that our implementation provides meaningful insights on
non-trivial models.