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. This entails that we need to find ways to reduce the energy consumption of such systems. 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 the consumed energy and the resulting utility. Therefore, research on energy efficiency has become a very active and important research topic that concerns many different scientific areas, and is as well of interest for industrial companies.
The concept of quantiles is already 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 in a satisfactory manner, e.g., a required user experience will be achieved with a sufficient probability. Quantiles also allow the determination of the maximal utility that can be achieved with a reasonable probability while staying within a given energy budget. As those examples illustrate important measures that are of interest when analysing energy-aware systems, it is clear that it is beneficial to extend formal analysis-methods with possibilities for the calculation of quantiles.
In this monograph, we will see how we can take advantage of those quantiles as an instrument for analysing the trade-off between energy and utility in the field of probabilistic model checking. Therefore, we present algorithms for their computation over Markovian models. We will further investigate different techniques in order to improve the computational performance of implementations of those algorithms. The main feature that enables those improvements takes advantage of the specific characteristics of the linear programs that need to be solved for the computation of quantiles. Those improved algorithms have been implemented and integrated into the well-known probabilistic model checker PRISM. The performance of this implementation is then demonstrated by means of different protocols with an emphasis on the trade-off between the consumed energy and the resulting utility. Since the introduced methods are not restricted to the case of an energy-utility analysis only, the proposed framework can be used for analysing the interplay of cost and its resulting benefit in general.:1 Introduction
1.1 Related work
1.2 Contribution and outline
2 Preliminaries
3 Reward-bounded reachability properties and quantiles
3.1 Essentials
3.2 Dualities
3.3 Upper-reward bounded quantiles
3.3.1 Precomputation
3.3.2 Computation scheme
3.3.3 Qualitative quantiles
3.4 Lower-reward bounded quantiles
3.4.1 Precomputation
3.4.2 Computation scheme
3.5 Energy-utility quantiles
3.6 Quantiles under side conditions
3.6.1 Upper reward bounds
3.6.2 Lower reward bounds
3.6.2.1 Maximal reachability probabilities
3.6.2.2 Minimal reachability probabilities
3.7 Reachability quantiles and continuous time
3.7.1 Dualities
4 Expectation Quantiles
4.1 Computation scheme
4.2 Arbitrary models
4.2.1 Existential expectation quantiles
4.2.2 Universal expectation quantiles
5 Implementation
5.1 Computation optimisations
5.1.1 Back propagation
5.1.2 Reward window
5.1.3 Topological sorting of zero-reward sub-MDPs
5.1.4 Parallel computations
5.1.5 Multi-thresholds
5.1.6 Multi-state solution methods
5.1.7 Storage for integer sets
5.1.8 Elimination of zero-reward self-loops
5.2 Integration in Prism
5.2.1 Computation of reward-bounded reachability probabilities
5.2.2 Computation of quantiles in CTMCs
6 Analysed Protocols
6.1 Prism Benchmark Suite
6.1.1 Self-Stabilising Protocol
6.1.2 Leader-Election Protocol
6.1.3 Randomised Consensus Shared Coin Protocol
6.2 Energy-Aware Protocols
6.2.1 Energy-Aware Job-Scheduling Protocol
6.2.1.1 Energy-Aware Job-Scheduling Protocol with side conditions
6.2.1.2 Energy-Aware Job-Scheduling Protocol and expectation quantiles
6.2.1.3 Multiple shared resources
6.2.2 Energy-Aware Bonding Network Device (eBond)
6.2.3 HAECubie Demonstrator
6.2.3.1 Operational behaviour of the protocol
6.2.3.2 Formal analysis
7 Conclusion
7.1 Classification
7.2 Future prospects
Bibliography
List of Figures
List of Tables
| Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:33742 |
| Date | 11 April 2019 |
| Creators | Daum, Marcus |
| Contributors | Baier, Christel, Parker, David, Technische Universität Dresden |
| Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/acceptedVersion, doc-type:doctoralThesis, info:eu-repo/semantics/doctoralThesis, doc-type:Text |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0024 seconds