Probabilistic Reachability for Parametric Markov Models

Ernst Moritz Hahn, Holger Hermanns, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

28 Citations (Scopus)

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 Θ(logn)). 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.
Original languageEnglish
Title of host publicationModel Checking Software
Subtitle of host publication16th International SPIN Workshop, Grenoble, France, June 26-28, 2009. Proceedings
PublisherSpringer
Pages88-106
ISBN (Electronic)978-3-642-02652-2
ISBN (Print)978-3-642-02651-5
DOIs
Publication statusPublished - 2009
Externally publishedYes
Event16th International SPIN Workshop on Model Checking Software 2009 - Grenoble, France
Duration: 26 Jun 200928 Jun 2009
Conference number: 16

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume5578
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference16th International SPIN Workshop on Model Checking Software 2009
CountryFrance
CityGrenoble
Period26/06/0928/06/09

Fingerprint Dive into the research topics of 'Probabilistic Reachability for Parametric Markov Models'. Together they form a unique fingerprint.

Cite this