Description

Many real-life phenomena can be abstractly modelled with continuous probability distributions: If you wait for the elevator, you can assume that the time remaining until it arrives follows an exponential distribution. If you measure some physical quantity, you should account for a measurement error that is normally distributed around the true, exact value.

The Modest language [1] allows formally modelling such phenomena and their interplay with e.g. hard deadlines or concurrent processes. Model-checking tools can then compute answers to questions like "what is the expected waiting time for the elevator" or "what is the probability that I will arrive at university before 08:45?"

Internally [2], our model checker deals with continuous distributions over real numbers by hacking them up into a finite number of intervals, computing the probability mass of the intervals, and then replacing the whole thing with a discrete probability distribution (e.g. "the elevator will arrive within 0 to 1 minutes with probability 0.5, 1 to 2 minutes with probability 0.3, and later than 2 minutes with probability 0.2"). The result is a finite-state system that our existing algorithms can handle. However, the current implementation is simple - it always creates intervals of length 1. This is inefficient: it doesn't scale well for complex models, and it is not precise enough in other cases.

The task in this project is to develop, implement and compare more intelligent methods of hacking continuous probability distributions into pieces - using the shape of the underlying pdf, or information collected from other places in the model.

Tasks:
- Think of better ways to hack probability distributions into pieces
- Implement them within the Modest Toolset [3] (website: http://www.modestchecker.net/)
- Use existing and new models to compare your approaches and evaluate the performance and precision improvements

Requirements:
- Basic understanding of probability theory
- Programming experience with an object-oriented language (our tools are written in C#)

References

1. Ernst Moritz Hahn, Arnd Hartmanns, Holger Hermanns, Joost-Pieter Katoen: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods in System Design 43(2): 191-232 (2013)
2. Ernst Moritz Hahn, Arnd Hartmanns, Holger Hermanns: Reachability and Reward Checking for Stochastic Timed Automata. ECEASST 70 (2014)
3. Arnd Hartmanns, Holger Hermanns: The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification. TACAS 2014: 593-598

Additional Resources

1. The paper