Partial Order Reduction for Model Checking Markov Decision Processes under Unconditional Fairness

Fairness assumptions are needed to verify liveness properties of concurrent systems. In this paper we explore the so-called unconditional fairness in Markov decision processes (MDPs), which is a prerequisite for quantitative assume-guarantee reasoning. Unconditional fairness refers to executions where all processes are guaranteed to participate. We prove that realisability of unconditional fairness coincides with the absence of partial deadlocks, i.e., end components where a process suffers from starvation. We propose a weak variant of the stubborn set method to reduce MDPs, while preserving the realisability of unconditional fairness and maximal probabilities of reaching bottom end components under fair schedulers.