Multi-objective Model Checking of Markov Automata

Markov automata (MAs) constitute a highly expressive formalism to model systems exhibiting nondeterminism, probabilistic branching, and continuously distributed random delays. Multi-objective model checking aims to analyze possible trade-offs between quantitative objectives of the modeled system, like the expected time for completing a job or the probability for an error-free behavior within a certain time interval. Previous works analyze MAs under schedulers that minimize (or maximize) a single objective. Known approaches do not generalize to multiple possibly conflicting objectives. For example, minimizing the expected time for completing a job might require taking higher risks, increasing the likelihood of an error. So far, the trade-off analysis between multiple objectives has only been studied for discrete-time models such as Markov decision processes (MDPs). In this thesis, we consider combinations of multiple (un)bounded probabilistic and expected value objectives for MAs. We lift the transformation from MAs to MDPs utilized in single-objective model checking to the multi-objective case. This requires new proofs as we need to consider a broader class of schedulers. Existing techniques for multi-objective MDPs are generalized to be compatible with the transformed models. Experiments on several case-studies are conducted to indicate the practical applicability of the presented results