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.
Thursday 26 September 2019 15:45 - 16:30
More events
- Mon 29 - Tue 30 Apr 2024Twente Water Weeks on campus
- Wed 8 - Wed 15 May 2024Erasmus+ Inspire Days
- Wed 8 May 2024 20:00 - 22:00Lecture in Twents, there's nothing wrong with that!
- Tue 21 May 2024 12:45 - 14:00Week of Inspiration / Lecture & concert: To the end of the world
- Tue 21 May 2024 19:30 - 21:00Week of inspiration / Wanted: climate optimists!