Trade-off Analysis Meets Probabilistic Model Checking

Christel BaierChristel Baier, Clemens DubslaffClemens Dubslaff, Sascha KlüppelholzSascha Klüppelholz

DOI Link

Christel Baier, Clemens Dubslaff, Sascha Klüppelholz
Trade-off Analysis Meets Probabilistic Model Checking
Proc. of the 23rd Conference on Computer Science Logic and the 29th Symposium on Logic In Computer Science (CSL-LICS), 1:1--1:10, 2014. ACM

Details
Bibtex

KurzfassungAbstract
Probabilistic model checking (PMC) is a well-established and powerful method for the automated quantitative analysis of parallel distributed systems. Classical PMC-approaches focus on computing probabilities and expectations in Markovian models annotated with numerical values for costs and utility, such as energy and performance. Usually, the utility gained and the costs invested are dependent and a trade-off analysis is of utter interest. In this paper, we provide an overview on various kinds of non-standard multi-objective formalisms that enable to specify and reason about the trade-off between costs and utility. In particular, we present the concepts of quantiles, conditional probabilities and expectations as well as objectives on the ratio between accumulated costs and utility. Such multi-objective properties have drawn very few attention in the context of PMC and hence, there is hardly any tool support in state-of-the-art model checkers. Furthermore, we broaden our results towards combined quantile queries, computing conditional probabilities those conditions are expressed as formulas in probabilistic computation tree logic, and the computation of ratios which can be expected on the long-run.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{BDK2014,
  author    = {Christel Baier and Clemens Dubslaff and Sascha Kl{\"{u}}ppelholz},
  title     = {Trade-off Analysis Meets Probabilistic Model Checking},
  booktitle = {Proc. of the 23rd Conference on Computer Science Logic and the
               29th Symposium on Logic In Computer Science (CSL-LICS)},
  publisher = {ACM},
  year      = {2014},
  pages     = {1:1--1:10},
  doi       = {10.1145/2603088.2603089}
}