title: Smarter sampling for optimaler decisions
topics: Algorithms and Data Structures , Dependability, security and performance
committee: Carlos Budde ,
Arnd Hartmanns


Formal models for verification and performance evaluation offer two ways to model decisions and uncertainty: via probabilistic choices, where each element of a set of alternatives is chosen with a certain probability, and nondeterministic choices, where we do not know at all which alternative will be chosen how often. Nondeterminism can flexibly represent either adversarial behaviour (i.e. we want to know what could happen in the worst case) or strategic choices (i.e. we want to find the best way to make these choices to achieve our goal, and presumably then implement this optimal schedule).

While traditional exhaustive model checking can naturally handle both types of choices, it is limited to small models by the state space explosion problem. More scalable approaches based on Monte Carlo simulation (often called statistical model checking) cannot natively deal with nondeterminism.

In this B.Sc. project, you will work with lightweight scheduler sampling, a recently developed method that makes it possible to combine simulation and nondeterminism to find near-optimal schedules. It is implemented in the Modest Toolset's modes simulator developed at FMT. However, the implementation performs scheduler sampling in a simple uniform manner. You will learn about a technique called smart sampling that iteratively refines a set of candidate schedulers and attempts to balance the precision (i.e. simulation effort) per scheduler versus the number of remaining schedulers. You will implement smart sampling for the computation of reachability probabilities, and develop a new smart sampling approach tailored to expected-cost properties. You will evaluate your implementation on existing case studies.

Prerequisites: Basic probability theory and statistics, some programming experience.
(The Modest Toolset is written in C#, but knowledge of a similar object-oriented language like Java or C++ usually suffices.)