Abstract.
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.
|