A Modest Approach to Modelling and Checking Markov Automata

Yuliya Butkova; Arnd Hartmanns; Holger Hermanns

doi:10.1007/978-3-030-30281-8_4

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 proceeding › Conference contribution › Academic › peer-review

5 Citations (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 language	English
Title of host publication	Proceedings of the 16th International Conference on Quantitative Evaluation of Systems (QEST 2019)
Editors	David Parker, Verena Wolf
Place of Publication	Cham
Publisher	Springer
Pages	52-69
Number of pages	18
ISBN (Electronic)	978-3-030-30281-8
ISBN (Print)	978-3-030-30280-1
DOIs	https://doi.org/10.1007/978-3-030-30281-8_4
Publication status	Published - 2019
Event	16th International Conference on Quantitative Evaluation of Systems, QEST 2019 - University of Glasgow, Glasgow, United Kingdom Duration: 10 Sept 2019 → 12 Sept 2019 Conference number: 16 http://www.qest.org/qest2019/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	11785
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Name	Theoretical Computer Science and General Issues
Publisher	Springer

Conference

Conference	16th International Conference on Quantitative Evaluation of Systems, QEST 2019
Abbreviated title	QEST 2019
Country/Territory	United Kingdom
City	Glasgow
Period	10/09/19 → 12/09/19
Internet address	http://www.qest.org/qest2019/

Access to Document

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

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). 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",

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)",

note = "16th International Conference on Quantitative Evaluation of Systems, QEST 2019, QEST 2019 ; Conference date: 10-09-2019 Through 12-09-2019",

url = "http://www.qest.org/qest2019/",

}

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, 16th International Conference on Quantitative Evaluation of Systems, QEST 2019, Glasgow, United Kingdom, 10/09/19. 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 proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A Modest Approach to Modelling and Checking Markov Automata

AU - Butkova, Yuliya

AU - Hartmanns, Arnd

AU - Hermanns, Holger

N1 - Conference code: 16

PY - 2019

Y1 - 2019

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

T2 - 16th International Conference on Quantitative Evaluation of Systems, QEST 2019

Y2 - 10 September 2019 through 12 September 2019

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). Epub 2019 Sept 4. doi: 10.1007/978-3-030-30281-8_4

A Modest Approach to Modelling and Checking Markov Automata

Abstract

Publication series

Conference

Access to Document

Other files and links