University of Twente Student Theses


Parallelising a probabilistic model checker

Sessink, Joost (2023) Parallelising a probabilistic model checker.

This is the latest version of this item.

[img] PDF
Abstract:Value iteration (VI) is an algorithm used for model checking probabilistic models. It is however known to perform inefficiently, especially when considering large models. In this thesis, we attempt to make value iteration more efficient by utilizing the multiple CPU cores that most computers nowadays possess. To realise this, we have implemented 3 parallel algorithms: parallel base value iteration (PBVI), topological parallel base value iteration (TPBVI) and parallel topological value iteration (PTVI). PBVI is a parallel algorithm with base value iteration (BVI), a traditional VI implementation, as its base. TPBVI and PTVI both are based on topological value iteration (TVI), a variant of VI that specifically takes into account the structure of the models. We benchmarked these parallel algorithms against their sequential counterparts as well as against each other, of which we present the results. All three parallel algorithms show overall speed-ups compared to their sequential counterparts, but also that their performance varies for the different models of the benchmark set.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page