A Modest Approach to Modelling and Checking Markov AutomataMarkov 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.Read more
About model and code verificationI will use this colloquium to present what I have been doing and learning during these three initial months at FMT. You will see that there is more learning than doing, this may hopefully have to do with me jumping from my former topic: Stochastic Automata for model checking, to my current topic which is static verification of code using VerCors. I will start showing you a little bit about how VerCors works, thus we may look into separation logic for this. Afterwards, I plan to show you what we try to do with Vercors, and for this, I may go through some examples of application and talk to you about my future work directions.Read more
