Theses

I offer supervision for Bachelor and Master theses. If you are interested in a bachelor or master thesis (on simulation or on any other topic), you are welcome to contact me.

LaTeX template for theses in Computer Science

Topics for Theses

Possible topics for theses:

Comparison of time-based and event-based simulation based on case studies (Bachelor)

Status quo: there are several formally defined case study models for stochastic hybrid systems with different properties from the ARCH Friendly Competition, which have been simulated and/or analyzed with different tools so far.
Objective of the thesis: development of time-based and event-based simulations for ARCH case studies, comparison of the speed and accuracy of the simulations.
Open questions: Which case studies are suitable for time-based and event-based simulation? What are the limits of practical feasibility? Which parameters influence performance?

Integration of Statistical Tests into an Existing Simulation Framework (Bachelor)

Status quo: In simulation, especially in Statistical Model Checking (SMC), it is typically assumed that a sufficient number of independent samples are generated. Whether the generated data are actually “random enough” or exhibit stationary behavior is often not explicitly verified. Classical statistical tests (e.g., runs test, chi-squared test, autocorrelation analysis) offer simple means to assess the randomness or uniformity of data.
Objective of the thesis: Integration of one or more basic statistical tests into an existing simulation framework. Use of these tests to analyze simulation outputs in order to detect stationary behavior, structural changes or trends, or undesired correlation between simulation runs. The goal is to gain a better understanding of when a simulation model produces stable and meaningful results.
Open questions: Which test is most appropriate for which type of simulation data? How large must the sample size be to draw reliable conclusions? How should the test results be interpreted in the context of SMC (e.g., with respect to confidence intervals or model validity)?

Integration of Empirical Distributions into an Existing Simulation Framework (Bachelor)

Status quo: Statistical Model Checking tools often rely on theoretical probability distributions (e.g., exponential, normal, uniform) as input for model parameters or event timings. In many practical applications, however, empirical data (e.g., time series, measurements) are available whose distribution does not match any standard theoretical form.
Objective of the thesis: Integration of empirically derived distributions into an existing statistical model checker – e.g., via histograms, interpolation functions, or kernel density estimation. The goal is to enable more realistic simulations based on real-world data. Compare the impact of empirical vs. theoretical distributions on selected verification results.
Open questions: Which representations of empirical distributions (e.g., histograms vs. KDE) are efficient and sufficiently accurate for use in Statistical Model Checking? How can such distributions be easily integrated into the tool (e.g., via configuration files or a simple API)? How does the choice of distribution affect the reliability and stability of statistical outcomes?

Development of a statistical model checker for rectangular autoata (Master)

Status quo: First approaches for statistical model checking of singular automata exist; rectangular automata additionally allow continuous non-determinism in the form of intervals in invariants, derivatives and jump conditions. This makes the analysis of rectangular automata difficult and inefficient for models with many random variables.
Objective of the thesis: Development of an event-based simulation approach for rectangular automata, including dealing with non-determinism (by resolution or by computing optimal schedulers) and the extension of the formalism with stochastic variables / random clocks, and addition of statistical model checking methods.
Open questions: What are the challenges of non-determinism in rectangular automata? How can we deal with non-determinism in simulation? How can previous simulation approaches be transferred? How easily can the formalism be extended to include stochastic variables, e.g. random clocks? How can statistical model checking methods be applied? How easy would an extension to linear hybrid automata (according to Henzinger) be?

Uncertainty Quantification (UQ) in Statistical Model Checking (Master)

Status quo: Classical Statistical Model Checking (SMC) verifies properties based on fixed model parameters. In real-world applications, these parameters are often uncertain or variable (e.g., due to measurement errors or incomplete knowledge). Initial approaches to combining SMC with Uncertainty Quantification (UQ) exist, such as nested Monte Carlo sampling. However, a complete integration into existing tools, application-oriented methodologies for complex models, and robust interpretations of combined uncertainties are still largely missing.
Objective of the thesis: Development and Evaluation of a concept for uncertainty quantification in the context of SMC, with a particular focus on: (1) Parametric uncertainty in probabilistic property evaluation, (2) Combining input uncertainty and sampling uncertainty from the SMC process, (3) Visualization and interpretation of the overall result (e.g., meta-confidence intervals). The approach will be applied to an existing stochastic model (e.g., hybrid Petri nets with stochastic variables). The goal is to produce a sound and practical methodology that fits realistic models and can be integrated into an existing simulation framework.
Open questions: How can uncertainty over parameter spaces (e.g., intervals or distributions) be systematically modeled? Which sampling techniques (grid, Latin Hypercube, adaptive) are most effective for UQ in the SMC context under limited computational budget? How can confidence intervals from SMC be meaningfully combined with input uncertainty? Can the results be summarized into a robust yet interpretable overall statement about the property under investigation?

Theoretical and Model-Specific Analysis of Convergence Rates in Statistical Model Checking (Master)

Status quo: Statistical Model Checking (SMC) uses Monte Carlo simulation to estimate the probability that a model satisfies a given property. The required number of simulations is typically derived from general statistical bounds (e.g., Hoeffding or Chernoff inequalities), independent of the model structure or property type. In practice, however, convergence behavior varies significantly depending on factors such as model complexity, property formulation, and event rarity. A systematic investigation of convergence behavior for specific model classes (e.g., hybrid Petri nets with random variables) is largely missing in the literature.
Objective of the Thesis: Analysis of how model characteristics (e.g., structure, synchronization, rare states) influence the convergence rate in SMC. Comparison of theoretical error bounds with empirically observed behavior on representative models. Development of simple criteria or heuristics to better estimate the remaining number of samples based on early results. Implementation of a prototype of an adaptive sampling strategy, either within an existing SMC tool.
Open Questions: Which structural properties of a model (e.g., conflicts, timing, state space size) systematically affect the variance and hence the convergence rate? How well do standard theoretical bounds reflect actual convergence behavior in practice? Where are they overly conservative? Can an adaptive sampling strategy be developed to balance efficiency and statistical confidence?