Skip to Main content Skip to Navigation
Conference papers

Partial order reduction for model checking Markov decision processes under unconditional fairness

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 execu- tions 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 probabili- ties of reaching bottom end components under fair schedulers.
Document type :
Conference papers
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-00647059
Contributor : Hongyang Qu <>
Submitted on : Monday, January 30, 2012 - 12:41:22 PM
Last modification on : Tuesday, September 8, 2020 - 4:58:02 PM
Long-term archiving on: : Tuesday, December 13, 2016 - 7:09:36 PM

File

qest11por.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00647059, version 1

Collections

Citation

Henri Hansen, Marta Kwiatkowska, Hongyang Qu. Partial order reduction for model checking Markov decision processes under unconditional fairness. 8th International Conference on Quantitative Evaluation of SysTems (QEST'11), 2011, Aachen, Germany. pp.203-212. ⟨hal-00647059⟩

Share

Metrics

Record views

255

Files downloads

545