A Modest Approach to Modelling and Checking Markov Automata

Yuliya Butkova, Arnd Hartmanns*, Holger Hermanns

*Corresponding author for this work

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    6 Citations (Scopus)
    1 Downloads (Pure)


    Markov automata are a compositional modelling formalism with continuous stochastic time, discrete probabilities, and nondeterministic choices. In this paper, we 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. We 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. We describe several recently developed such algorithms as implemented in mcsta and evaluate them on a comprehensive set of benchmarks. Our evaluation shows that mcsta improves the performance and scalability of Markov automata model checking compared to earlier and alternative tools.

    Original languageEnglish
    Title of host publicationProceedings of the 16th International Conference on Quantitative Evaluation of Systems (QEST 2019)
    EditorsDavid Parker, Verena Wolf
    Place of PublicationCham
    Number of pages18
    ISBN (Electronic)978-3-030-30281-8
    ISBN (Print)978-3-030-30280-1
    Publication statusPublished - 2019
    Event16th International Conference on Quantitative Evaluation of Systems, QEST 2019 - University of Glasgow, Glasgow, United Kingdom
    Duration: 10 Sept 201912 Sept 2019
    Conference number: 16

    Publication series

    NameLecture Notes in Computer Science
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349
    NameTheoretical Computer Science and General Issues


    Conference16th International Conference on Quantitative Evaluation of Systems, QEST 2019
    Abbreviated titleQEST 2019
    Country/TerritoryUnited Kingdom
    Internet address


    Dive into the research topics of 'A Modest Approach to Modelling and Checking Markov Automata'. Together they form a unique fingerprint.

    Cite this