Compiling Probabilistic Model Checking into Probabilistic Planning

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.

Authors

• Michaela Klauck
• Marcel Steinmetz
• Jörg Hoffmann 0001
• Holger Hermanns

Keywords

• Probabilistic Planning
• Probabilistic Model Checking
• Goal Probability Analysis