[HKQ11]
Henri Hansen, Marta Kwiatkowska and Hongyang Qu.
Partial Order Reduction for Model Checking Markov Decision Processes under Unconditional Fairness.
In Proc. 8th International Conference on Quantitative Evaluation of SysTems (QEST'11), pages 203-212, IEEE CS Press.
September 2011.
[pdf]
[bib]
[Presents partial-order reduction methods for MDPs, implemented in an extension of PRISM.]
|
Links:
[Google]
[Google Scholar]
|
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.
|