Probabilistic Model Checking and Non-standard Multi-objective Reasoning

Christel BaierChristel Baier, Clemens DubslaffClemens Dubslaff, Sascha KlüppelholzSascha Klüppelholz, Marcus DaumMarcus Daum, Joachim KleinJoachim Klein, Steffen MärckerSteffen Märcker, Sascha WunderlichSascha Wunderlich

DOI Link

Christel Baier, Clemens Dubslaff, Sascha Klüppelholz, Marcus Daum, Joachim Klein, Steffen Märcker, Sascha Wunderlich
Probabilistic Model Checking and Non-standard Multi-objective Reasoning
Proc. of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE), volume 8411 of Lecture Notes in Computer Science, 1--16, 2014. Springer

Details
Bibtex

KurzfassungAbstract
Probabilistic model checking is a well-established method for the automated quantitative system analysis. It has been used in various application areas such as coordination algorithms for distributed systems, communication and multimedia protocols, biological systems, resilient systems or security. In this paper, we report on the experiences we made in inter-disciplinary research projects where we contribute with formal methods for the analysis of hardware and software systems. Many performance measures that have been identified as highly relevant by the respective domain experts refer to multiple objectives and require a good balance between two or more cost or reward functions, such as energy and utility. The formalization of these performance measures requires several concepts like quantiles, conditional probabilities and expectations and ratios of cost or reward functions that are not supported by state-ofthe- art probabilistic model checkers. We report on our current work in this direction, including applications in the field of software product line verification.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-54804-8_1.

@inproceedings{BDKDKMW2014,
  author    = {Christel Baier and Clemens Dubslaff and Sascha Kl{\"{u}}ppelholz
               and Marcus Daum and Joachim Klein and Steffen M{\"{a}}rcker and
               Sascha Wunderlich},
  title     = {Probabilistic Model Checking and Non-standard Multi-objective
               Reasoning},
  booktitle = {Proc. of the 17th International Conference on Fundamental
               Approaches to Software Engineering (FASE)},
  series    = {Lecture Notes in Computer Science},
  volume    = {8411},
  publisher = {Springer},
  year      = {2014},
  pages     = {1--16},
  doi       = {10.1007/978-3-642-54804-8_1}
}