Formal methods for probabilistic energy models | (Statusvortrag)

Datum

18.12.2015

Zeit

12:30 - 13:30

Sprecher

Marcus Daum

Sprache

en

Hauptthema

Informatik

Andere Themen

Informatik

Beschreibung

The energy consumption that arises from the utilisation of information processing systems adds a significant contribution to environmental pollution and has a big share of operation costs. When trying to save energy it is important to ensure that the utility (e.g., user experience) of a system is not unnecessarily degraded, requiring a careful trade-off analysis between energy and utility. The concept of quantiles is well-known in mathematical statistics, but its benefits for the formal quantitative analysis of probabilistic systems have been noticed only recently. For instance, with the help of quantiles it is possible to reason about the minimal energy that is required to obtain a desired system behaviour with a high probability. As another example, quantiles also allow the determination of the maximal utility that can be achieved with a reasonable probability while staying within a given energy budget. This talk demonstrates how quantiles can be used for the trade-off analysis between energy and utility in the field of probabilistic model checking. We present algorithms and their complexities for the computation of quantiles in Markovian models. We will further show results of implementations of those algorithms by means of different case studies that are driven by the cooperations in the project "Highly Adaptive Energy-efficient Computing" (HAEC). Betreuerin: Prof. Dr. Christel Baier Fachreferent: Prof. Dr. Hermann Härtig

Letztmalig verändert: 18.12.2015, 08:48:02