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

    1 Citation (Scopus)

    Abstract

    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
    PublisherSpringer
    Pages52-69
    Number of pages18
    ISBN (Electronic)978-3-030-30281-8
    ISBN (Print)978-3-030-30280-1
    DOIs
    Publication statusPublished - 2019
    Event16th International Conference on Quantitative Evaluation of Systems, QEST 2019 - University of Glasgow, Glasgow, United Kingdom
    Duration: 10 Sep 201912 Sep 2019
    Conference number: 16
    http://www.qest.org/qest2019/

    Publication series

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

    Conference

    Conference16th International Conference on Quantitative Evaluation of Systems, QEST 2019
    Abbreviated titleQEST 2019
    CountryUnited Kingdom
    CityGlasgow
    Period10/09/1912/09/19
    Internet address

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

  • Cite this

    Butkova, Y., Hartmanns, A., & Hermanns, H. (2019). A Modest Approach to Modelling and Checking Markov Automata. In D. Parker, & V. Wolf (Eds.), Proceedings of the 16th International Conference on Quantitative Evaluation of Systems (QEST 2019) (pp. 52-69). (Lecture Notes in Computer Science; Vol. 11785), (Theoretical Computer Science and General Issues). Cham: Springer. https://doi.org/10.1007/978-3-030-30281-8_4