Partial order reduction for model checking Markov decision processes under unconditional fairness - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2011

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

Marta Kwiatkowska
  • Fonction : Auteur
  • PersonId : 861066
Hongyang Qu
  • Fonction : Auteur

Résumé

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.

Domaines

Informatique
Fichier principal
Vignette du fichier
qest11por.pdf (237.16 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00647059 , version 1 (30-01-2012)

Identifiants

  • HAL Id : hal-00647059 , version 1

Citer

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⟩

Collections

CONNECT
117 Consultations
357 Téléchargements

Partager

Gmail Facebook X LinkedIn More