University of Twente Student Theses
The State of Multi-Objective Model Checking
Wijk, M.G.W. van (2024) The State of Multi-Objective Model Checking.
|
PDF
1MB |
| Abstract: | Probabilistic model checkers can be used to formally verify the behaviour of a system. We can analyse a quantitative property like the chance of success, the expected costs, or uptime of a system. Although traditionally only one property is considered at the same time, in most real-life processes multiple properties influence each other. For example, the highest expected uptime of a system might be disproportionately expensive. Therefore, we focus on multi-objective probabilistic model checking, which allows us to consider the trade-offs between several properties. Since model checkers are used to analyse safety-critical processes such as space travel, it is important that they are reliable. Our research aims at assessing and improving the state of probabilistic model checkers. We show that there are several mistakes in state-of-the-arts model checkers. We then show the origins of these mistakes and solve most of them. We then replicate the most common multi-objective model checking papers using the Modest Toolset to investigate the validity of these algorithms. We found several mistakes and curiosities in the replicated papers. |
| 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: | https://purl.utwente.nl/essays/104622 |
| 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