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

    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 statusE-pub ahead of print/First online - 4 Sep 2019

    Publication series

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

    Fingerprint

    Automata
    Modeling
    High level languages
    Model checking
    Process Algebra
    Algebra
    Alternatives
    Scalability
    Reachability
    Long-run
    Reward
    Model
    Model Checking
    Discrete-time
    Roots
    Benchmark
    Evaluate
    Evaluation
    Language

    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
    Butkova, Yuliya ; Hartmanns, Arnd ; Hermanns, Holger. / A Modest Approach to Modelling and Checking Markov Automata. Proceedings of the 16th International Conference on Quantitative Evaluation of Systems (QEST 2019). editor / David Parker ; Verena Wolf. Cham : Springer, 2019. pp. 52-69 (Lecture Notes in Computer Science). (Theoretical Computer Science and General Issues).
    @inproceedings{f2759afa0cee49908a50d6cbfa51705e,
    title = "A Modest Approach to Modelling and Checking Markov Automata",
    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.",
    author = "Yuliya Butkova and Arnd Hartmanns and Holger Hermanns",
    year = "2019",
    month = "9",
    day = "4",
    doi = "10.1007/978-3-030-30281-8_4",
    language = "English",
    isbn = "978-3-030-30280-1",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    pages = "52--69",
    editor = "David Parker and Verena Wolf",
    booktitle = "Proceedings of the 16th International Conference on Quantitative Evaluation of Systems (QEST 2019)",

    }

    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). Lecture Notes in Computer Science, vol. 11785, Theoretical Computer Science and General Issues, Springer, Cham, pp. 52-69. https://doi.org/10.1007/978-3-030-30281-8_4

    A Modest Approach to Modelling and Checking Markov Automata. / Butkova, Yuliya; Hartmanns, Arnd; Hermanns, Holger.

    Proceedings of the 16th International Conference on Quantitative Evaluation of Systems (QEST 2019). ed. / David Parker; Verena Wolf. Cham : Springer, 2019. p. 52-69 (Lecture Notes in Computer Science; Vol. 11785), (Theoretical Computer Science and General Issues).

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

    TY - GEN

    T1 - A Modest Approach to Modelling and Checking Markov Automata

    AU - Butkova, Yuliya

    AU - Hartmanns, Arnd

    AU - Hermanns, Holger

    PY - 2019/9/4

    Y1 - 2019/9/4

    N2 - 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.

    AB - 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.

    UR - http://www.scopus.com/inward/record.url?scp=85072850457&partnerID=8YFLogxK

    U2 - 10.1007/978-3-030-30281-8_4

    DO - 10.1007/978-3-030-30281-8_4

    M3 - Conference contribution

    AN - SCOPUS:85072850457

    SN - 978-3-030-30280-1

    T3 - Lecture Notes in Computer Science

    SP - 52

    EP - 69

    BT - Proceedings of the 16th International Conference on Quantitative Evaluation of Systems (QEST 2019)

    A2 - Parker, David

    A2 - Wolf, Verena

    PB - Springer

    CY - Cham

    ER -

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