I did my PhD at the Chair of Algebraic and Logical Foundations of Computer Science headed by Christel Baier at the TU Dresden. During this time I developed a quantile-based framework in order to support the analysis of energy-aware systems. The basis for the implementation of this framework builds the probabilistic model checker PRISM in version 4.3.1. This basis gave me support for some of the necessary fundamental methods that are required for the computation of quantiles over Markovian models. For example, PRISM delivers some of the infrastructure for the handling of Markovian models or the related reward structures.

My dissertation ‘Formal Methods for Probabilistic Energy Models’ describes all the relevant details. If you are interested in using the implementation or if you have any questions, do not hesitate to contact me.

Sources for the calculation of quantiles

All the referenced archives are based on the probabilistic model checker PRISM in version 4.3.1. They do extend PRISM in order to support the calculation of quantiles over Markovian models. The focus of my work was on the computation of quantiles using the explicit engine of PRISM. Whereas the support for the different symbolic engines provided by PRISM (Hybrid, Sparse, MTBDD) was done by Joachim Klein.

Quantiles integrated into PRISM
This version uses PRISM as it is and just extends it by integrating the computation of quantiles. As a consequence this version can be easily integrated into PRISM in order to provide the presented quantile-based framework with PRISM.
Quantiles integrated into PRISM using BitSetInterface
In contrast to the previous version the base classes of PRISM were slightly changed by replacing each usage of the class BitSet with the usage of the tailored data structure BitSetInterface. The main advantage is that small sets of indices (or states) are not stored using BitSets. Instead a dynamic adapting data structure is used that uses integer-arrays for the storage of a few elements, and as soon as more elements need to be stored, the storage automatically utilises BitSets. The analysed protocols revealed that this improved both the calculation speed and the memory consumption for the computation of quantiles when using PRISMs explicit engine.
This version was used for calculating the results presented in the monograph ‘Formal Methods for Probabilistic Energy Models’.
Quantiles integrated into PRISM using BitSet only
Here, we do not use the self-adapting storage described previously. We only utilise the class BitSet as it is shipped with the programming language JAVA. The analysed protocols revealed that the utilisation of BitSets for the calculation of quantiles in the explicit engine restricted the applicability of the calculation of quantiles in many cases. Therefore, a lot of protocols could not be analysed using this implementation.
The only reason for considering this version is for demonstrating the impact of the self-adapting data structure on the performance of the quantile calculations.

All the listed archives were created using the command-line tool tar with the options -czf in order to obtain a compressed archive. The best way for decompressing the archive is to use

tar -xzf archive.tar.gz

in the command line. After the archives were successfully extracted to the specified path one needs to follow the instructions stated under Building PRISM from source.

Specifying a quantile query in PRISM

For the following it is assumed that the reader is familiar with PRISM and is able to build and verify a model using the possibilities that are provided by PRISM.

Since there exists support for a variety of quantile queries we will give a short introduction concerning the different possibilities. At first we differentiate between quantiles that aim at fulfilling some (constrained) reachability formula with some desired probability (reachability quantiles), and expectation quantiles that aim at optimising the accumulation of two reward functions.

Before continuing I want to introduce a useful interactive tool that presents an overview over the different syntactic possibilities for reachability quantiles and their interplay. It was written by Joachim Klein and can be found here. It allows to explore the different variants for (probability) quantiles, conversion between the two syntax notations and exploration of the transformations between quantiles. Those transformations allow to rely on a limited number of base cases for implementing the computations.

In the explicit engine of PRISM, the computation of quantiles is supported for DTMCs and MDPs, while the implementation for the symbolic engines is currently limited to MDPs. Additionally, there is support for computing time-bounded reachability quantiles for CTMCs, as introduced below.

Reachability quantiles

The reachability quantiles can be partitioned into plain reachability quantiles and quantiles under side conditions. Plain reachability quantiles can be specified using the following syntax (called normal-form):

Quantile (Ex, P>0.5 [ F<=_q goal ], R{"try"})

This quantile asks for the minimal number of tries that are needed in order to finally reach the desired goal with a probability greater than 0.5. We hereby ask for the best scheduler that is able to guarantee our demand (due to the specification of Ex).
It is as well possible to specify a step-bounded quantile by simply dropping the specification of the reward structure:

Quantile (Ex, P>0.5 [ F<=_q goal ])

So, this quantile asks for the minimal number of steps in order to reach the goal. The keyword Ex specifies an existential quantile that optimises for the best scheduler. It can be replaced by Un for the calculation of all schedulers.

In order to provide a more convenient user-friendly (human-readable) form the parser also supports queries of the form:

quantile (min t, Pmax>0.5 [ F{reward{"try"}<=t} goal ])

It is implicitly specified that we are interested in the computation of the best scheduler by using Pmax. (If interested in the computation for all schedulers, we need to replace Pmax by Pmin.) With the given formula we explicitly specify that we want to compute the minimal number of attempts t in order to finally reach a state in goal with a probability greater than 0.5. When interested in the minimal number of steps one can specify the following:

quantile (min s, Pmax>0.5 [ F{steps<=s} goal ])

Whenever the specified probability operator is either >0 or >=1 the implementation integrated into the explicit engine of PRISM will automatically compute the quantiles using the (graph-based) algorithm for qualitative quantiles.

All presented queries support the usage of multi-thresholds. So, instead of specifying just one threshold like 0.5, it is possible to use many different thresholds inside the computation of one quantile query. An example is given by the following query:

 quantile (min t, Pmax>{0, 0.01, [0.05:0.95:0.1], 0.99} [ F{reward{"try"}<=t} goal ])

The curly brackets contain an enumeration of different thresholds. The square brackets define a computation specification for multiple thresholds that will be expanded during the process of parsing. The 0.05 specifies the starting value, meaning that we start with the threshold 0.05. 0.95 defines the end of the block. So, the highest specified threshold is not greater than 0.95. And the stepping is defined by 0.1, meaning that 0.1 will be added to the previously computed value. The presented specification results in the following sequence of thresholds:

0.05, 0.15, 0.25, 0.35, ..., 0.85, 0.95

In summary the following sequence will be derived by the specification:

0, 0.01, 0.05, 0.15, 0.25, 0.35, ..., 0.85, 0.95, 0.99

Reachability quantiles under side conditions

The previously considered plain reachability quantiles can be extended by the specification of some ω-regular side condition. Now, the objective is to compute the specified reachability quantile and at the same time fulfilling this side condition.

The specification of such a quantile can be done by the following (at the moment only the syntax for the normal-form supports the specification of quantiles under side conditions):

Quantile (Ex, P>0.5 [ (F<=_q success) & (G(boost_1=0)) ], R{"energy"})

G(boost_1=0) hereby defines the side condition. This side condition will be transformed into a deterministic automaton that runs in parallel to the model under consideration. So, with the specified query we ask for the minimal energy that needs to be invested in order to be successful with a probability greater than 0.5. At the same time we want to make sure that the turbo boost provided by the model under consideration is inactive all the time.

Reward-bounded reachability properties

Since the algorithm for the computation of quantiles relies on an iterated computation of reward-bounded reachability probabilities, the employed computation methods can be used as well for the computation of reward-bounded reachability probabilities, without the need to introduce a counter to the model. In contrast to a quantile query a reward-bounded reachability query is already equipped with a certain bound determining the exact number of iterations that need to be performed in order to calculate the demanded reachability probabilities. The utilisation of the quantile backend hereby takes advantage of all the improvements that were implemented for the computation of quantiles.

An example for a reward-bounded reachability property is as follows:

Pmax=? [ F{reward{"energy"}<=200} goal ]

This property asks for the maximal probability to finally reach the goal when there are 200 energy units allowed for consumption.

It is as well possible to specify multiple reward bounds for a reachability property. For N specified bounds the last N-1 bounds will be encoded into the state space of the model by using a counter-based transformation. The very first bound specified in a property will be not encoded as a counter. So, the property

Pmax=? [ F{reward{"energy"}<=200,reward{"send_messages"}<=5} goal ]

will be solved by transforming the bound for the transmission of the messages into a counter. Afterwards the previously introduced algorithm for the computation of reward-bounded probabilities will be used to reason about the energy of the resulting counter-equipped model. As a consequence the user needs to be careful which reward structure should be represented by the counters and which reward structure should be analysed using the quantile backend. In the considered example the encoding of 5 messages might perform better than using a counter for the representation of the consumed energy (the main problem is that counting up to 200 may result in much more reachable states than simply counting to 5). If one has to deal with a mixture of step- and reward-bounds the counter-based transformation will always prefer the step-bounds for encoding as counters and the very first reward-bound will be analysed using the quantile backend.

In order to get a feeling for reward-bounded reachability properties the example given here can be utilised. It is equipped with two different reward functions (one for the consumed energy and one for the gained utility), and we can therefore compute the probability to receive at least some desired utility by investing not more than a specific energy budget. Rearranging the order of the bounds helps to study the impact of the given order on the counter-based transformation and the afterwards applied quantile-based computations.

Reachability quantiles over CTMCs

The presented implementation supports quantiles with upper or lower time bounds on simple path formulas over continuous-time Markov chains. The utilised algorithm consists of a combination of an exponential search with a succeeding binary search in order to find the demanded quantile value. The exponential search determines the smallest i ∈ Ν such that the probability for the given path formula is greater than the specified probability threshold for the first time. Afterwards, a binary search will be performed in the interval [2^i-1, 2ⁱ].

An example query is as follows:

quantile (min t, P>=0.5 [ F{time<=t} goal ])

This query asks for the minimal time such that we can finally reach the desired goal with a probability of at least 0.5.

The precision of the computed result is specified by the switch -quantileCtmcPrecision <x> over the command line. There exists the possibility to start the computation with a more coarse-grained precision and to dynamically refine the precision of the computation until the user-defined accuracy can be guaranteed for the resulting value. This allows to relax the precision when it is not necessary. In order to enable this option from the command line one needs to specify the switch -quantileCtmcStartPrecision <x>, where x corresponds to the desired starting precision. Setting x to 0 deactivates this dynamic adaptation-behaviour and all necessary computations use the precision specified for the final result.

For now the implemented algorithm only supports quantiles with upper or lower time bounds on simple path formulas.

Expectation quantiles

Expectation quantiles investigate the interplay of two reward functions. So, instead of handling just one reward function we take another one into account. We minimise the accumulation of one reward and try to increase the accumulation of the second reward. An expectation quantile can be specified using the following query:

expQuantile (Ex, Exp R{"utility"} > 5.5 [ R{"energy"} <= ? ])

Since we now consider expected values and not probabilities, the specified threshold can be greater than 1. This formula asks for the minimal energy that needs to be invested in order to achieve more than the specified expected utility of 5.5. The usage of multi-thresholds is supported as well. So, we can ask for:

 expQuantile (Ex, Exp R{"utility"} > {[0:10:1], [20:100:10], 200, 500} [ R{"energy"} <= ? ])

The usage of Ex again asks for the minimal energy accumulated by the best scheduler, while the minimal energy in the worst case can be computed using the following specification where Ex has been replaced by Un:

expQuantile (Un, Exp R{"utility"} > 5.5 [ R{"energy"} <= ? ])

Adapting the performance of the computation of quantiles

There are multiple possibilities to increase the performance of the computation of quantile queries. This allows to adapt the performance to different applications that have varying characteristics.

Using the command-line flag

prism -help

reveals multiple options that can be used in order to influence the performance of the quantile computations. The most important ones that have the highest impact on the computational performance are:

-valuesStorage <name> .......... Specify the method to store the values for the successors of positive reward states / transitions ([ALL_STATES, POS_REWARD_SUCCS_UNIFORM, POS_REWARD_SUCCS_INDIVIDUAL]) [default: ALL_STATES]

-lpSolverOnly <n> .............. Use the LP solver exclusively for all calculations (the number gives the bound for the calculations)

-multiStateMethod <name> ........ Specify the method to solve multi-state sets ([VALUE_ITERATION, INTERVAL_ITERATION, LP_SOLVER]) [default: VALUE_ITERATION]

-parallelPoolSize <n> .......... Specify the number of parallel threads for quantile-calculations

-parallelForPositiveRewards .... Exploit parallelism of J8 for parallel computations of positive-reward states. The degree of parallelity is controllable via -parallelPoolSize <n>

-parallelForZeroRewards ........ Exploit parallelism of J8 for parallel computations of zero-reward states. The degree of parallelity is controllable via -parallelPoolSize <n>

-quantileCtmcStartPrecision <x>  Set precision for quantile-calculations using CTMCs. Whenever a more precise computation is needed, the precision will adapt automatically. Setting to 0 will deactivate this behaviour and all calculations will be carried out using PRISMs standard-setting [default: 0]

-quantileCtmcPrecision <x> ..... Set value of epsilon for quantile-convergence in CTMCs [default: 1e-6]

Another possibility of adapting the performance of the quantile computations is by utilising the options dialog of the GUI. There exists the tab Quantile which provides the same possibilities as the flags for the command-line version.

Analysed protocols

In the following we list the material for the protocols that have been analysed within the dissertation ‘Formal Methods for Probabilistic Energy Models’. We start by giving the material for the selected protocols from the benchmark suite of PRISM:

Self-Stabilising Protocol: analysed models and properties (plot)
Asynchronous Leader-Election Protocol: analysed models and properties (plot)
Synchronous Leader-Election Protocol: analysed models and properties (plot)
Randomised Consensus Shared Coin Protocol: analysed models and properties (plot)

As well some protocols with an emphasis on their energy efficiency have been analysed:

Energy-Aware Job-Scheduling Protocol:
- reachability quantiles:
  - one shared resource:
    - minimal energy: analysed models and properties (plot)
    - maximal utility: analysed models and properties (plot)
    - under side conditions:
      - prohibit turbo mode: analysed models and properties (plot)
      - force turbo mode after first deadline-miss: analysed models and properties (plot)
      - round-robin scheduling: analysed models and properties (plot, zoomed)
  - two shared resources:
    - minimal energy: analysed models and properties (plot)
    - maximal utility: analysed models and properties (plot)
- expectation quantiles: analysed models and properties (plot)
Energy-Aware Bonding Network Device: analysed models and properties (plot)
HAECubie Demonstrator:
- reachability quantiles: analysed models and properties (plot)
- expectation quantiles: analysed models and properties (plot)

As an example for quantiles over CTMCs we analysed the minimal time that needs to pass before the Tandem Queueing Network becomes full with some specific probability:

Tandem Queueing Network: analysed models and properties