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.
Type de document :
Communication dans un congrès
8th International Conference on Quantitative Evaluation of SysTems (QEST'11), 2011, Aachen, Germany. IEEE CS Press, pp.203-212, 2011, 8th International Conference on Quantitative Evaluation of SysTems (QEST'11)
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00647059
Contributeur : Hongyang Qu <>
Soumis le : lundi 30 janvier 2012 - 12:41:22
Dernière modification le : lundi 30 janvier 2012 - 14:18:32
Document(s) archivé(s) le : mardi 13 décembre 2016 - 19:09:36

Fichier

qest11por.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. IEEE CS Press, pp.203-212, 2011, 8th International Conference on Quantitative Evaluation of SysTems (QEST'11). 〈hal-00647059〉

Partager

Métriques

Consultations de la notice

176

Téléchargements de fichiers

155