The State of Multi-Objective Model Checking

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.