Preview

Description

We address the problem of verifying PCTL properties of Markov Decision Processes whose state transition probabilities are only known to lie within uncertainty sets. Using results from convex theory and duality, we propose a suite of verification algorithms and prove their soundness, completeness and termination when arbitrary convex models of uncertainty are considered. Furthermore, soundness and termination can also be guaranteed when non-convex models of uncertainty are adopted. We validate the proposed approach on two case studies: the verification of a consensus protocol when one of the processes behaves erroneously and the dining philosopher problem.

Details

Files

Actions

Statistics

from
to
Export
Download Full History