Quantitative Analysis under Fairness Constraints

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

Beitragende

Abstract

It is well-known that fairness assumptions can be crucial for verifying progress, reactivity or other liveness properties for interleaving models. This also applies to Markov decision processes as an operational model for concurrent probabilistic systems and the task to establish tight lower or upper probability bounds for events that are specified by liveness properties. In this paper, we study general notions of strong and weak fairness constraints for Markov decision processes, formalized in an action- or state-based setting. We present a polynomially time-bounded algorithm for the quantitative analysis of an MDP against ω-automata specifications under fair worst- or best-case scenarios. Furthermore, we discuss the treatment of strong and weak fairness and process fairness constraints in the context of partial order reduction techniques for Markov decision processes that have been realized in the model checker LiQuor and rely on a variant of Peled’s ample set method.

Details

OriginalspracheEnglisch
TitelAutomated Technology for Verification and Analysis
Redakteure/-innenZhiming Liu, Anders P. Ravn
ErscheinungsortBerlin, Heidelberg
Herausgeber (Verlag)Springer, Berlin, Heidelberg
Seiten135-150
Seitenumfang16
ISBN (elektronisch)978-3-642-04761-9
ISBN (Print)978-3-642-04760-2
PublikationsstatusVeröffentlicht - 2009
Peer-Review-StatusJa

Publikationsreihe

ReiheLecture Notes in Computer Science
Band5799
ISSN0302-9743

Konferenz

Titel7th International Symposium on Automated Technology for Verification and Analysis
KurztitelATVA 2009
Veranstaltungsnummer
Dauer14 - 16 Oktober 2009
Webseite
BekanntheitsgradInternationale Veranstaltung
Ort
StadtMacao
LandChina

Externe IDs

Scopus 71549171144
ORCID /0000-0002-5321-9343/work/205988093

Schlagworte