A Modest Approach to Modelling and Checking Markov Automata

Markov automata are a compositional modelling formalism with continuous stochastic time, discrete probabilities, and nondeterministic choices. In this talk, based on joint work with Yuliya Butkova and Holger Hermanns, and recently presented at QEST'19, I will present extensions to the Modest language and the mcsta model checker to describe and analyse Markov automata models. Modest is an expressive high-level language with roots in process algebra that allows large models to be specified in a succinct, modular way. I will explain its use for Markov automata and illustrate the advantages over alternative languages. The verification of Markov automata models requires dedicated algorithms for time-bounded probabilistic reachability and long-run average rewards. I will describe several recently developed such algorithms as implemented in mcsta and showcase an experimental evaluation on a comprehensive set of benchmarks. The evaluation shows that mcsta improves the performance and scalability of Markov automata model checking compared to earlier and alternative tools.