Probabilistic Reachability for Parametric Markov Models

Publication: Research - peer-reviewJournal article – Annual report year: 2011

View graph of relations

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 nondeterminism. Experimental evidence is provided, illustrating that our implementation provides meaningful insights on non-trivial models.
Original languageEnglish
JournalInternational Journal on Software Tools for Technology Transfer
Publication date2011
Volume13
Journal number1
Pages3-19
ISSN1433-2779
DOIs
StatePublished

Bibliographical note

The original publication is available at www.springerlink.com.

CitationsWeb of Science® Times Cited: No match on DOI

Keywords

  • Reachability, Model checking, Markov chains, Parametric model analysis

Download statistics

No data available

ID: 6296177