Submitted: January 2018
Abstract
Dependability of computer systems and software is a factor of steadily growing importance. In order to reason about a system’s reliability, a variety of formal models have been proposed with the goal of verifying different kinds of correctness properties.
Among the most expressive formalisms are Markov automata. They combine the continuous-time stochastic behavior of continuous-time Markov chains (CTMCs) with the probabilistic and nondeterministic branching of probabilistic automata without sacrificing compositionality.
This thesis first places the Markov automaton model within the tree spanned by different established formalisms and discusses how their features differ.
We then suggest a lifting of the Unif+ algorithm, an algorithm aiming at checking time-bounded reachability properties of continuous-time Markov decision processes (CTMDPs), to Markov automata and prove its correctness. As a proof of concept we additionally supply an implementation within Storm, a model checker for Markov automata and less expressive models, and evaluate its performance on a set of available benchmarks. Additionally, we provide a small improvement for a certain class of Markov automata that includes almost all of the known applications.