Quantitative analysis under fairness constraints
From International Center for Computational Logic
Quantitative analysis under fairness constraints
Christel BaierChristel Baier, Marcus GrößerMarcus Größer, Frank CiesinskiFrank Ciesinski
Christel Baier, Marcus Größer, Frank Ciesinski
Quantitative analysis under fairness constraints
Proc. of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 5799 of Lecture Notes in Computer Science, 135--150, 2009. Springer
Quantitative analysis under fairness constraints
Proc. of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 5799 of Lecture Notes in Computer Science, 135--150, 2009. Springer
- KurzfassungAbstract
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. - Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science
@inproceedings{BGC2009,
author = {Christel Baier and Marcus Gr{\"{o}}{\ss}er and Frank Ciesinski},
title = {Quantitative analysis under fairness constraints},
booktitle = {Proc. of the 7th International Symposium on Automated Technology
for Verification and Analysis (ATVA)},
series = {Lecture Notes in Computer Science},
volume = {5799},
publisher = {Springer},
year = {2009},
pages = {135--150},
doi = {10.1007/978-3-642-04761-9_12}
}