Computing Conditional Probabilities in Markovian Models Efficiently

Christel BaierChristel Baier, Joachim KleinJoachim Klein, Sascha KlüppelholzSascha Klüppelholz, Steffen MärckerSteffen Märcker

DOI Link

Christel Baier, Joachim Klein, Sascha Klüppelholz, Steffen Märcker
Computing Conditional Probabilities in Markovian Models Efficiently
Proc. of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 8413 of Lecture Notes in Computer Science, 515--530, 2014. Springer

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-54862-8_43.

@inproceedings{BKKM2014,
  author    = {Christel Baier and Joachim Klein and Sascha Kl{\"{u}}ppelholz and
               Steffen M{\"{a}}rcker},
  title     = {Computing Conditional Probabilities in Markovian Models
               Efficiently},
  booktitle = {Proc. of the 20th International Conference on Tools and
               Algorithms for the Construction and Analysis of Systems (TACAS)},
  series    = {Lecture Notes in Computer Science},
  volume    = {8413},
  publisher = {Springer},
  year      = {2014},
  pages     = {515--530},
  doi       = {10.1007/978-3-642-54862-8_43}
}