ProbMeLa and Verification of Markov Decision Processes

Christel BaierChristel Baier, Frank CiesinskiFrank Ciesinski, Marcus GrößerMarcus Größer

DOI Link

Christel Baier, Frank Ciesinski, Marcus Größer
ProbMeLa and Verification of Markov Decision Processes
SIGMETRICS Performance Evaluation Review, 32(4):22--27, 2005

Details
Bibtex

KurzfassungAbstract
Markov decision processes (MDP) can serve as operational model for probabilistic distributed systems and yield the basis for model checking algorithms against qualitative or quantitative properties. In this paper, we summarize the main steps of a quantitative analysis for a given MDP and formula of linear temporal logic, give an introduction to the modelling language ProbMela which provides a simple and intuitive way to describe complex systems with a MDP-semantics and present the basic features of the MDP model checker LiQuor.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{BCG2005,
  author  = {Christel Baier and Frank Ciesinski and Marcus Gr{\"{o}}{\ss}er},
  title   = {ProbMeLa and Verification of Markov Decision Processes},
  journal = {SIGMETRICS Performance Evaluation Review},
  volume  = {32},
  number  = {4},
  year    = {2005},
  pages   = {22--27},
  doi     = {10.1145/1059816.1059821}
}