University of Twente Student Theses
Data Structures and Heuristics for State Elimination in Markov Models
Boom, Mark (2023) Data Structures and Heuristics for State Elimination in Markov Models.
|
PDF
601kB |
| Abstract: | Model checking is a popular technique to verify (software) systems, where calculating properties of Markov Models is common practice. Many algo- rithms exist that achieve this, one of which is state elimination. Optimizing these algorithms provides more accurate results and more performance. In this paper we specifically address the underlying data structures for stor- ing models in memory. We develop a novel data structure, implement it within the framework of an existing model checker and benchmark it against a more traditional object-oriented data structure. Furthermore, we evalu- ate heuristics regarding the elimination order of states. We show that the data structure used may have a significant impact on performance. Within the realm of Markov Decision Processes, the problem of transition blowup emerges which renders a state elimination algorithm unfit without further optimizations. For Discrete-Time Markov Chains, elimination order has impact on memory usage. However, the effects of a heuristic are highly dependent on the characteristics of the model used. |
| Item Type: | Essay (Bachelor) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Computer Science BSc (56964) |
| Link to this item: | https://purl.utwente.nl/essays/95787 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page