Promise: Symbolic Probabilistic Model Checking with Massive Design Spaces (NWO Veni)
In this project, we aim to combine symbolic probabilistic model checking methods with inductive synthesis to quickly analyze many different models. The novel methods in this project shall boost the PAYNT tool.
Summary for the general public
The design of safety-critical systems comes with many questions: What is the most cost-efficient hardware for lane assist in cars? What battery size suffices for a satellite? Will the robot safely unload the dishwasher? Although seemingly different, these questions can all be (partially) answered by analysing Markov models that describe how systems behave in uncertain circumstances. However, the complexity of modern computer systems leads to models that are too big to handle. This research project aims to develop novel algorithms that are able to analyse much bigger Markov models.
Funding Information
The project is funded by an NWO Veni Grant. These are parts of the NWO Talent Scheme. The funding amounts to 280k over 3 years (2023-2026).