Computing Conditional Probabilities in Markovian Models Efficiently

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributedpeer-review

Abstract

The fundamentals of probabilistic model checking for Markovian models and temporal properties have been studied extensively in the past 20 years. Research on methods for computing conditional probabilities for temporal properties under temporal conditions is, however, comparably rare. For computing conditional probabilities or expected values under ω-regular conditions in Markov chains, we introduce a new transformation of Markov chains that incorporates the effect of the condition into the model. For Markov decision processes, we show that the task to compute maximal reachability probabilities under reachability conditions is solvable in polynomial time, while it was conjectured to be computationally hard. Using adaptions of known automata-based methods, our algorithm can be generalized for computing the maximal conditional probabilities for ω-regular events under ω-regular conditions. The feasibility of our algorithms is studied in two benchmark examples.

Details

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
EditorsErika Ábrahám, Klaus Havelund
PublisherSpringer, Berlin [u. a.]
Pages515-530
Number of pages16
ISBN (print)978-3-642-54861-1
Publication statusPublished - 2014
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science, Volume 8413
ISSN0302-9743

Conference

TitleEuropean Joint Conferences on Theory and Practice of Software 2014
Abbreviated titleETAPS 2014
Conference number
Duration13 - 15 April 2014
Website
Degree of recognitionInternational event
Location
CityGrenoble
CountryFrance

External IDs

Scopus 84900534492
ORCID /0000-0002-5321-9343/work/142236741

Keywords

Keywords

  • conditional probabilities, Markovian Models

Library keywords