Compiling Probabilistic Model Checking into Probabilistic Planning


  • Michaela Klauck Saarland University
  • Marcel Steinmetz Saarland University
  • Jörg Hoffmann Saarland University
  • Holger Hermanns Saarland University



Probabilistic Planning, Probabilistic Model Checking, Goal Probability Analysis


It has previously been observed that the verification of safety properties in deterministic model-checking frameworks can be compiled into classical planning. A similar connection exists between goal probability analysis on either side, yet that connection has not been explored. We fill that gap with a translation from Jani, an input language for quantitative model checkers including the Modest toolset and PRISM, into PPDDL. Our experiments motivate further cross-fertilization between both research areas, specifically the exchange of algorithms. Our study also initiates the creation of new benchmarks for goal probability analysis.




How to Cite

Klauck, M., Steinmetz, M., Hoffmann, J., & Hermanns, H. (2018). Compiling Probabilistic Model Checking into Probabilistic Planning. Proceedings of the International Conference on Automated Planning and Scheduling, 28(1), 150-154.