Verification of PCTL Properties of MDPs with convex uncertainties in PRISM

by Alberto Puggelli for PRISM Model Checker

We plan to integrate within PRISM an algorithm for the verification of Probabilistic Computation Tree Logic (PCTL) properties of Markov Decision Processes (MDPs) whose state transition probabilities are only known to lie within convex uncertainty sets. We have recently presented the first-known polynomial time verification algorithm for PCTL properties of CMDPs. We now plan to integrate this algorithm within PRISM, and to demonstrate it with case studies.